주요 특징

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

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에 액세스할 수 있습니다. 이를 사용하여 다음을 포함한 소프트웨어 개발 작업 흐름의 모든 중요 활동을 지원할 수 있습니다.

  • 0으로 나누기와 같은 런타임 오류 검출
  • 버퍼 오버플로우와 같이 안전성이나 보안에 대한 중대한 런타임 오류가 없음을 증명
  • 변수 범위를 결정하고 범위 한도를 위반하지 않았는지 확인
  • 적절한 소프트웨어 품질 목표를 충족했는지 확인
  • Simulink 모델 또는 IBM® Rational® Rhapsody® 모델까지의 런타임 오류를 추적
  • 인증을 위한 아티팩트 생성

Polyspace Code Prover는 Polyspace Bug Finder와 함께 사용하여 소스 코드에서 0으로 나누기나 버퍼 오버플로우 등과 같이 안전성이나 보안에 악영향을 끼치는 결함을 검출하고 MISRA와 같은 코딩 표준의 준수 여부를 확인합니다. 이 두 제품으로 개발 초기 단계에서부터 버그 찾기, 코드 규칙 검사 및 런타임 오류 증명에 걸치는 엔드투엔드(end-to-end) 정적 분석 기능을 제공합니다. 이러한 기능을 통해 최고 수준의 품질과 안전성으로 동작해야 하는 임베디드 소프트웨어의 코드의 신뢰성을 확보할 수 있습니다.

Parallel Computing Toolbox™MATLAB Distributed Computing Server™를 사용하여 검증 작업을 컴퓨터 클러스터로 제출함으로써 속도를 향상시킬 수 있습니다.


런타임 오류 검출

Polyspace Code Prover는 정적 코드 분석과 함께 추상적 해석을 사용하여 산술 오버플로우, 0으로 나누기 및 버퍼 오버플로우 등의 런타임 오류를 증명, 식별 및 진단합니다. 이 기술은 가능성이 있는 모든 런타임 조건을 철저하고 완벽하게 확인하며 자동으로 각 코드 연산에 대해 증명 여부, 실패 여부, 또는 도달 가능 여부에 대한 진단 정보를 제공합니다. Polyspace Code Prover가 생성한 검증 결과에서 각 C 또는 C++ 연산은 코드에 색상을 입혀 다음과 같이 상태가 표시됩니다.

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

검출된 오류들:

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

Polyspace Code Prover에 의해 식별된 런타임 오류 속성들입니다.


범위 정보 보기

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

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

또한, 호출 계층 구조 및 호출 흐름 그래프를 사용하여 제어 흐름을 시각화하거나 전역 변수 데이터에 대한 액세스를 시각화하여 확인할 수 있습니다.

Explore gallery (3 images)


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

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

웹 브라우저에 표시된 소프트웨어 품질 메트릭


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

또한, Polyspace Code Prover는 런타임 에러 결과로부터 dSPACE® TargetLink® 블록 및 IBM Rational Rhapsody 모델까지의 추적 기능도 지원합니다.

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


코드 검증 프로세스 자동화

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

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


인증을 위한 아티팩트 생성

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

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

Certification 및 Qualification Kit가 판매 중입니다.