Accelerating the pace of engineering and science

Polyspace Code Prover

주요 특징

  • C 및 C++ 코드에서 특정 런타임 오류가 없음이 증명됨
  • 코드에 런타임 오류의 색상 코드 지정
  • 변수 및 함수 반환 값에 대한 범위 정보 계산
  • 지정된 범위 한도를 초과하는 변수 식별
  • 소프트웨어 품질 목표 준수를 추적하기 위한 품질 메트릭
  • 코드 메트릭과 품질 상태를 제공하는 웹 기반 대시보드
  • 결과 및 런타임 오류 상태 분류를 위한 가이드 기반 검토-확인 프로세스
  • 변수 읽기 및 쓰기에 대한 시각적인 표시
Run-time error results displayed by Polyspace Code Prover.
Polyspace Code Prover에서 표시된 런타임 오류 결과.

C 및 C++ 임베디드 소프트웨어 검증

Polyspace Code Prover는 반드시 최고 수준의 품질과 안전성을 요구하는 C 및 C++ 임베디드 소프트웨어 코드의 검증을 수행합니다. 이 툴은 추상적 해석(abstract interpretation)이라고 하는 정형 기법 기술을 사용하여 타당한 검증 결과를 도출합니다. Polyspace Code Prover는 런타임 오류가 발생할 수 있는 부분과 런타임 오류가 없음이 확인된 코드를 식별합니다. 고품질 보장 프로세스의 일부로서 Polyspace Code Prover를 사용하여 모든 입력, 경로 및 변수 값들을 철저하게 검증합니다. Polyspace Code Prover는 색상 코드를 사용하여 코드에서 각 요소의 상태를 나타냅니다. Simulink®와의 통합을 통해 코드 수준의 런타임 결과를 Simulink 모델까지 추적할 수 있습니다.

Polyspace Code Prover를 통해 다음을 수행할 수 있습니다.

  • 코드 증명 — 코드에 런타임 오류가 없는지 검증
  • 거짓 음성(false negative)가 없는 결과 확보 — 모든 런타임 오류 가능성을 철저히 파악
  • 코드의 품질에 대한 신뢰성 확보 — 검증된 코드와 검증되지 않은 코드를 측정

명령줄, 그래픽 사용자 인터페이스 또는 Visual Studio® 및 Eclipse™에 대한 플러그인을 통해 Polyspace Code Prover에 액세스할 수 있습니다. 이를 사용하여 다음을 포함한 소프트웨어 개발 작업 흐름의 모든 중요 활동을 지원할 수 있습니다.

  • 런타임 오류 검출
  • 특정 런타임 오류가 없음을 증명
  • 변수 범위를 결정하고 범위 한도가 위반되지 않았는지 확인
  • 적절한 소프트웨어 품질 목표 충족을 보장
  • Simulink 블록 또는 IBM® Rational® Rhapsody® 모델까지 런타임 오류를 추적
  • 인증을 위한 아티팩트 생성

Polyspace Code Prover는 Polyspace Bug Finder와 함께 작동하여 결함을 검출하고 코딩 표준 준수를 확인할 뿐만 아니라 소스코드에 특정 런타임 오류가 없음을 증명할 수 있습니다. 이러한 제품은 버그 찾기, 코드 규칙 검사 및 런타임 오류 증명에 이르는 초기 단계 개발에서부터 사용할 수 있는 엔드투엔드(end-to-end) 정적 분석 기능을 제공합니다. 이 기능은 최고 수준의 품질과 안전이 요구되는 임베디드 소프트웨어의 신뢰성을 보장합니다.

Parallel Computing Toolbox™MATLAB Distributed Computing Server™를 통해 검증 작업을 제출함으로써 해당 작업을 컴퓨터 클러스터로 전가하고 코드 검증 속도를 더 빠르게 할 수 있습니다.

런타임 오류 검출

Polyspace Code Prover는 정적 코드 분석(static analysis)과 추상적 해석(abstract interpretation)을 사용하여 오버플로우, 0으로 나누기 및 경계 밖 포인터와 같은 런타임 오류를 증명, 식별 및 진단할 수 있습니다. 이 기술은 모든 런타임 조건을 완벽하하게 포괄적으로 검증하며 자동으로 각 코드 연산에 대해 검증 여부, 실패 여부, 또는 도달 가능 여부 에 대한 진단을 제공합니다. Polyspace Code Prover가 생성한 검증 결과에서 각 C 또는 C++ 연산은 다음 색상 코드를 통해 상태를 나타냅니다.

녹색: 런타임 오류가 없는 것으로 증명됨
빨간색: 연산을 실행할 때마다 오류가 있음이 증명됨
회색: 도달할 수 없는 것으로 증명됨(기능 문제가 있을 수 있음)
오렌지색: 특정 조건에서 증명되지 않은 연산은 오류를 일으킬 수 있음

Color-coded run-time error attributes identified by Polyspace Code Prover.

Polyspace Code Prover에서 식별된 런타임 오류 속성

검출된 오류:

  • 오버플로우, 언더플로우, 0으로 나누기 및 기타 산술 오류
  • 경계 밖 배열 액세스 및 잘못 참조 해제된 포인터
  • 항상 true 또는 false인 구문
  • 초기화되지 않은 클래스 멤버(C++)
  • 초기화되지 않은 데이터에 대한 읽기 액세스
  • Null this포인터에 대한 액세스(C++)
  • 데드 코드(dead code)
  • 객체 프로그래밍, 상속 및 예외 처리(C++)와 관련된 동적 오류

범위 정보 보기

Polyspace Code Prover는 소프트웨어를 통해 제어와 데이터 흐름을 추적하고 변수 및 연산자와 연결된 범위 정보를 표시합니다. 커서를 연산자 또는 변수 위에 올려놓으면 툴팁 메시지가 범위 정보를 표시합니다. 추상적 해석(abstract interpretation)으로 알려진 정형 기법(formal method)은 정확한 범위 정보의 측정으로 소프트웨어에 특정 런타임 오류가 없음을 증명하기 위한 목적을 달성하도록 합니다. 범위 정보를 사용하여 소프트웨어를 디버깅하거나 특정 변수 또는 연산이 지정된 범위 한도를 위반하지 않았다는 것을 확실하게 알 수 있습니다.

아래 예제에서 Polyspace Code Prover는 나누기 연산의 왼쪽 피연산자가 -1701~3276의 범위이고 오른쪽 피연산자가 9임을 파악했습니다. 나누기 후 결과 범위는 -189~364입니다.

Tooltip displaying the possible ranges for all run time conditions.
모든 런타임 조건에 대한 가능한 범위를 표시하는 툴팁

호출 계층과 호출 흐름 그래프를 사용하여 제어 흐름을 추가적으로 시각화할 수 있습니다.

Call flow graph displaying the order of function calls in an interprocedural analysis.
절차적 분석에서 함수 호출 순서

소프트웨어 품질 메트릭 추적

중앙 집중식 품질 모델을 정의하여 런타임 오류, 코드 복잡성, 코딩 규칙 위반을 추적할 수 있습니다. 이러한 메트릭을 사용하여  개발의 시작 단계부터 최종 제공 버전까지 코드가 진화함에 따라 사전 정의된 소프트웨어 품질 목표에 대한 진행 상태를 추적할 수 있습니다. Polyspace Code Prover는 코드 품질의 개선 속도를 측정함으로써 개발자, 테스터 및 프로젝트 관리자가 고품질 코드를 목표로 설정하고 이를 제공할 수 있도록 합니다.

Software quality metrics displayed via web browser.
웹 브라우저를 통해 표시된 소프트웨어 품질 메트릭.

코드 검증 결과를 Simulink 모델까지 추적

Polyspace Code Prover는 생성된 코드 또는 생성된 코드와 직접 작성한 코드를 모두 포함하는 혼합 코드를 분석할 수 있습니다. 자동 생성된 코드내 코드 수준의 결함 결과는 Simulink의 모델까지 추적됩니다. 모델에서 믿을 수 있는 부분을 식별하고 코드에서 오류를 일으킬 수 있는 설계 문제를 수정할 수 있습니다. 또한 생성된 코드와 직접 작성한 코드의 인터페이스 사이에서 잠재적인 문제를 찾아낼 수 있습니다. 예를 들어 직접 작성한 S-Function 코드를 생성된 코드와 혼합하면, 인터페이스의 잘못된 신호 범위로 인해 런타임 오류가 발생하는 문제가 있을 수 있습니다.

Polyspace Code Prover는 또한 런타임 결과를 dSPACE® TargetLink® 블록과 IBM Rational Rhapsody 모델까지 추적하는 것도 지원합니다.

Tracing code verification results to the Simulink model.
코드 검증 결과를 Simulink 모델까지 추적.

코드 검증 프로세스 자동화

Polyspace를 빌드 프로세스에 포함시킴으로써 Polyspace Code Prover를 지속적인 통합 프로세스의 일부로 사용할 수 있습니다. 검증 작업 스케줄링을 자동화하고 이메일 알림을 설정할 수 있습니다. Polyspace Code Prover를 할당하여 검증 작업을 클러스터 컴퓨터(MATLAB Distributed Computing Server 사용)로 게시하는 일정을 정하고 결과가 나오면 이메일 알림을 받을 수 있습니다. 결과에는 서버가 자동으로 계산하는 이전 버전 코드와의 차이점이 포함되어 있습니다.

이러한 분석의 빈도도 정의 가능하며, 코드 기반의 특정 부분에 대해 적용하길 원하는 품질 모델을 정의할 수 있고, 결과가 나왔을 때 앞서 말한 사용자에게 보낼 이메일도 지정할 수 있습니다. 또한 자동화된 검증을 포함시키려는 빌드 프로세스의 특징도 정의할 수 있습니다.

인증용 아티팩트 생성

Polyspace Bug Finder 및 Polyspace Code Prover 는 IEC Certification Kit (IEC 61508 및 ISO 26262의 경우)DO Qualification Kit (DO-178의 경우)을 통해 업계 표준 기반의 프로젝트를 위한 인증 프로세스에서 사용할 수 있습니다.

보고서와 아티팩트는 코드의 최종 품질을 보여주고, 검토된 섹션을 강조 표시하며, 코드 메트릭을 생성하고, 코딩 규칙의 적용과 런타임 오류 상태를 문서화합니다. 이러한 보고서는 PDF, HTML, RTF 및 기타 형식으로 만들 수 있습니다.

DO Qualification Kit contents.
인증 및 검증 키트가 제공됩니다.

Polyspace를 활용한 C/C++ 코드 검증

웨비나 보기