Polyspace Code Prover

소프트웨어의 런타임 오류의 부재를 증명할 수 있습니다.

Polyspace Code Prover 는 C 및 C++ 소스 코드에서 오버플로, 0으로 나누기, 범위를 벗어난 배열 액세스 및 기타 런타임 오류의 부재를 증명할 수 있습니다. 프로그램 실행, 코드 계측 또는 테스트 케이스 없이도 결과를 생성할 수 있습니다. Polyspace Code Prover는 정형 기법을 기반으로 한 정적 분석과 추상 해석을 사용합니다. 수작업 코드, 생성된 코드 또는 둘이 조합된 코드에도 사용할 수 있습니다. 각 연산은 여러 색을 사용하여 런타임 오류가 없는지, 실패하는 것으로 증명되는지, 도달할 수 없거나 증명되지 않는지를 표시합니다.

Polyspace Code Prover는 변수 및 함수 반환 값에 대한 범위 정보를 표시하고, 어떤 변수가 지정된 범위 제한을 초과하는지 증명할 수 있습니다. 결과를 대시보드에 퍼블리시하여 품질 메트릭을 추적하고 소프트웨어 품질 목표를 준수할 수 있습니다.

IEC Certification Kit (for IEC 61508 and ISO 26262) 및 DO Qualification Kit (for DO-178)를 통해 산업 표준 지원이 가능합니다.

심각한 런타임 오류의 부재 증명

코드를 실행하지 않고 가능한 모든 입력값에 대해 모든 코드 경로를 분석할 수 있습니다. 런타임 조건과 무관하게 런타임 오류가 발생하지 않는 명령문을 식별하고 주의가 필요한 명령문을 찾을 수 있습니다.

문서

소프트웨어 설계 및 코드 이해도 개선

C/C++ 코드의 제어 및 데이터 흐름을 점검하고 변수 및 연산자와 관련된 범위 정보를 확인할 수 있습니다.

문서

소프트웨어 성능 최적화

안전성 및 보안성이 있는 연산을 식별하여 0으로 나누기나 오버플로와 같은 방어 코드를 제거할 수 있습니다. 실행 경로를 통해 도달할 수 없는 코드 분기를 검출할 수 있습니다. 논리 및 프로그램 구조에서 오류를 찾고 제거하여 메모리 사용량을 줄일 수 있습니다.

문서

전역 변수 사용 분석

작업 또는 스레드에 의해 공유되는 변수를 비롯하여 전역 변수에 대한 읽기/쓰기 연산을 디버그하는 데 소비되는 시간을 경감할 수 있습니다.
동시 액세스 그래프를 통해 데이터 경쟁 문제로 이어지는 제어 및 데이터 흐름을 이해할 수 있습니다. 코드 최적화를 위해 사용되지 않는 전역 변수를 식별할 수 있습니다.

문서

인증 지원

업계 표준에 대한 인증 과정을 완료하는 데 필요한 아티팩트를 생성할 수 있습니다. IEC 61508 및 ISO 26262 표준에 대한 사용 적합성을 TÜV SÜD에서 인증받았습니다. 리포트 및 아티팩트를 DO-178C 인증에 사용할 수 있습니다.

문서

Simulink 및 Stateflow 통합

생성된 코드에 대해 분석을 실행하고 그 결과를 소스 Simulink 모델 블록 및 Stateflow 차트로 추적할 수 있습니다. Simulink 환경 안에서 Polyspace^® 분석을 시작할 수 있습니다.

문서

데스크탑에서 대화형 방식 분석

소프트웨어 프로젝트 전체 또는 일부에 대해 정적 코드 분석을 실행할 수 있습니다. 데스크탑 툴을 사용하여 리포트를 생성하고 결과를 검토하며 분류할 수 있습니다.
디버거와 같은 보기를 통해 복잡한 버그의 근본 원인을 찾아 런타임 오류를 일으키는 각 명령문을 단계별로 탐색할 수 있습니다. 60개 이상의 C 및 C++ 컴파일러를 기본적으로 지원하며, 프로젝트의 빌드 시스템에서 추출하여 자동으로 Polyspace 분석을 설정함으로써 프로젝트를 조직하고 구성할 수 있습니다.

문서

정적 애플리케이션 보안 테스트

버퍼 오버플로, 메모리 액세스, 수치 오버플로 등의 심각한 보안 취약성의 부재를 증명할 수 있습니다. 코드 실행 없이 모든 코드 경로와 입력값에 대해 코드를 분석하여 퍼즈 테스트의 필요성을 줄일 수 있습니다.

영향 분석

지정된 전역 또는 지역 변수가 다른 변수나 특정 명령문에 미치는 영향을 정형적으로 추적하고 검증할 수 있습니다. 신호 분석을 수행하여 OBD 관련 소프트웨어에 대한 CARB의 요구사항을 충족하고 ISO 26262 맥락에서 간섭의 부재(freedom from interference)를 증명하며 보정 파라미터의 효과를 분석할 수 있습니다. 소프트웨어 보안의 맥락에서는 오염 분석과 민감 데이터 흐름 추적을 수행할 수 있습니다.