Polyspace Code Prover

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

Polyspace Code Prover™는 C 및 C++ 소스 코드에서 오버플로, 0으로 나누기, 범위를 벗어난 배열 접근 및 기타 런타임 오류가 없음을 증명하는 견고한 정적 분석 툴입니다. 프로그램 실행이나 탐침 코드 삽입, 테스트 케이스 작성없이 결과물을 만들어 냅니다. Polyspace Code Prover는 소프트웨어 프로시저 간, 제어 및 데이터 흐름 동작을 검증하기 위한 정형기법을 기반으로 의미 분석과 추상 해석을 사용합니다. 이 도구를 통해 손으로 작성한 코드, 생성된 코드 또는 이 둘의 조합을 검증할 수 있습니다. 각 코드 구문은 런타임 오류가 없는지, 실패하거나 도달할 수 없다고 증명되었는지, 증명되지 않았는지를 나타내기 위해 코드에 색상을 입혀 표현됩니다.

Polyspace Code Prover는 변수와 함수 반환 값에 대한 범위 정보를 표시하고 어떤 변수가 지정된 범위 제한을 초과하는지를 증명할 수 있습니다. 코드 검증 결과를 사용하여 품질 지표를 추적하고 소프트웨어 품질 목표를 준수하는지 확인할 수 있습니다. Polyspace Code Prover는 Eclipse™ IDE와 연동하여코드를 검증할 수 있습니다.

IEC Certification Kit(IEC 61508 및 ISO 26262용)와 DO Qualification Kit(DO-178용)를 통해 업계 표준을 지원합니다.

정형 기법 기반의 코드 검증

부정 오류 없이 높은 수준의 품질과 안전성을 확보합니다.

심각한 런타임 오류가 없음을 증명하기

실행 환경과 상관없이 런타임 오류가 발생하지 않는 C/C++ 및 Ada 코드의 연산들을 파악합니다.

런타임 오류 검출

다른 테스팅 방식이 발견 못 한 오류 감지

코드 실행 없이 가능한 모든 입력에 대해 모든 코드 경로를 분석합니다.

호출 계층 구조.

인증용 산출물 생성

업계 표준에 따라 프로젝트의 을 따르는로세스를 완료할 수 있습니다.

DO Qualification Kit.

코드 이해 및 개선

코드 리뷰, 디버깅 및 견고성 테스트에 소요되는 시간을 줄입니다.

문제의 근본 원인 이해와 디자인 개선

소프트웨어의 제어와 데이터 흐름을 검사하고 변수와 연산자에 관련된 범위 정보를 확인합니다.

모든 런타임 조건에 대해 가능한 범위를 표시하는 툴팁.

의도하지 않은 소프트웨어 동작 방지

로직과 프로그램 구조에 있는 에러나 어떤 실행 경로로도 도달할 수 없는 코드 영역을 찾습니다.

데드 코드 찾기.

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

생성된 코드에 대한 검증을 실행하고 검증 결과물에서 Simulink의 소스 모델 블록으로 추적합니다.

코드 검증 결과물에서 Simulink 모델로 추적하기

Polyspace Code Prover Server로 코드 검증 자동화

코드 변경 마다 조기에 자주 분석함으로써 지속적인 통합을 용이하게 합니다.

코드 검증 절차 자동화

Polyspace Code Prover Server™를 사용하여 Jenkins 및 Bamboo와 같은 빌드 자동화 도구로 서버급 시스템에서 Polyspace Code Prover 정적 분석 엔진을 실행합니다.

코드 검증 절차 자동화.

협업 리뷰를 위한 결과 업로드 및 알림

자동으로 결함을 구성 요소 소유자에게 할당하고, 이메일 알림을 보내고, 결과를 Polyspace Code Prover Access에 업로드하여 문제를 분류하고 해결할 수 있습니다.

Polyspace Code Prover 결과와 함께 이메일 알림을 보냅니다.

Polyspace Code Prover Access로 협업 리뷰

검증 결과와 품질 메트릭을 소프트웨어 개발 팀과 공유합니다.

Polyspace Code Prover 결과물을 리뷰하여 문제 분류 및 해결

Polyspace Code Prover Access™는 중앙 저장소에 있는 Polyspace 코드 검증 결과와 품질 메트릭에 대한 웹 브라우저 인터페이스를 제공합니다. 웹 브라우저에서 여러 탐색 도구들을 사용하여 코드가 함께 표시되는 코드 검증 결과를 조사합니다.

런타임 오류 검출

프로젝트 품질 및 소프트웨어 품질 목표

대시보드에는 소프트웨어 품질, 프로젝트 상태, 결함 수, 코드 메트릭 및 소프트웨어 품질 목표를 모니터링하는 데 사용할 수 있는 정보가 표시됩니다.

프로젝트 개요 대시보드.

이미 사용하고 있는 버그 추적 툴과 통합

웹 브라우저 인터페이스를 사용하여 Jira와 같은 버그 추적 툴에서 티켓을 생성하고 할당합니다.

티켓 생성.

최신 기능

공유 변수 분석 모드

전역 변수 공유 및 사용 내용들에 대해서만 계산하기 위해 전체 어플리케이션에 대해 덜 광범위한 방식으로 Code Prover 분석 실행

컴파일러 지원

Cosmic 컴파일러로 컴파일하는 코드를 손쉽게 Polyspace 분석 환경 구성

Simulink 지원

Simulink 편집기 툴스트립에서 상황에 알맞게 나오는 버튼을 사용해 생성된 코드를 분석

Simulink 지원

C Caller 블록 및 Stateflow 차트에서 호출하는 사용자 정의 코드를 모델의 문맥에서 검증

이 기능과 그에 상응하는 함수에 대한 세부 정보는 릴리스 정보를 참조하십시오.

무료 평가판 받기

30일 동안 사용해 보세요.

다운로드

구매하기

제품별 가격을 확인하세요.

학생이세요?

학생용 MATLAB 및 Simulink를 확인하세요.

자세히 보기