Polyspace Code Prover

소프트웨어에 런타임 오류가 없음을 증명

Polyspace Code Prover™는 C 및 C++ 소스 코드에 오버플로우, 0으로 나누기, 경계 밖 배열 액세스, 기타 특정 런타임 오류가 없음을 증명합니다. 프로그램 실행, 코드 수정 또는 테스트 케이스 없이 결과를 제공합니다. Polyspace Code Prover는 정적 분석과 정형 기법(formal method) 기반의 추상적 해석(abstract interpretation)을 사용합니다. 직접 작성한 코드, 생성된 코드 또는 이 두 가지가 조합된 코드에서 Polyspace Code Prover를 사용할 수 있습니다. 각 연산은 런타임 오류가 있는지, 실패가 검증되었는지, 도달할 수 없는지 또는 증명되지 않았는지 여부를 나타내는 색상 코드가 지정됩니다.

Polyspace Code Prover는 변수 및 함수 반환 값에 대한 범위 정보를 표시할 수 있고 변수가 지정된 범위 한도를 초과하는 조건을 증명할 수도 있습니다. 결과를 대시보드에 게시하여 품질 메트릭을 추적하고 소프트웨어 품질 목표를 준수할 수 있도록 합니다. 자동화된 검증을 위해 Polyspace Code Prover를 빌드 시스템에 통합할 수 있습니다.

업계 표준에 대한 지원은 IEC Certification Kit(IEC 61508 및 ISO 26262의 경우)와 DO Qualification Kit (DO‑178의 경우)를 통해 이용 가능합니다. Ada 언어 지원도 제공됩니다.

Comprehensive Static Analysis Using Polyspace Products

온라인 세미나 보기

평가판 사용 Polyspace Code Prover

평가판 신청
Jay Abraham

새로운 내용

출처: Jay Abraham, Polyspace Code Prover 기술 전문가