Polyspace Client™ for Ada는 Ada83 및 Ada95 소스 코드에서 오버플로, 0으로 나누기, 범위를 벗어난 배열 액세스 및 기타 특정 런타임 오류의 부재를 증명합니다. 프로그램 실행, 코드 계측 또는 테스트 케이스 없이도 결과를 생성할 수 있습니다. Polyspace Client for Ada는 정형 기법에 기반한 추상 해석 기법을 사용하여 코드를 검증합니다. 분석 결과는 소스 코드 내에 표시됩니다. 각 코드 명령문은 여러 색을 사용하여 런타임 오류가 없는지, 실패하는 것으로 증명되는지, 도달할 수 없거나 증명되지 않는지를 표시합니다. Polyspace Client for Ada는 변수 및 함수 반환 값에 대한 범위 정보를 표시하고, 어떤 변수가 지정된 범위 제한을 초과하는지 증명할 수 있습니다.
사용자는 데스크탑에서 Polyspace Client for Ada를 사용하여 컴파일 및 테스트 전에 코드 분석을 실행하고 검토할 수 있습니다.
심각한 런타임 오류의 부재 증명
Ada83 또는 Ada95 코드 연산의 런타임 정확성을 검사할 수 있습니다. 런타임 조건에 무관하게 런타임 오류가 발생하지 않을 명령문을 식별할 수 있습니다. 발견된 사항과 관련된 이벤트 추적, 변수 값 범위 및 호출 트리의 지원을 통해 런타임 취약점을 분석할 수 있습니다. Polyspace Client for Ada는 정형 기법을 사용하여 다른 테스트 수단으로 찾을 수 없는 오류를 검출할 수 있습니다. 코드를 실행하지 않고 가능한 모든 입력값에 대해 모든 코드 경로를 분석할 수 있습니다.
데스크탑에서 대화형 방식 분석
프로젝트를 정리 및 구성하고 소프트웨어 프로젝트의 부분에 대해 정적 코드 분석을 실행하여 코드를 소스 코드 리포지토리에 제출하기 전에 코드 변경 사항의 적합성을 검사할 수 있습니다. Polyspace Client for Ada를 사용하면 리포트를 생성하고 결과를 검토 및 분류할 수 있습니다. 디버거와 같은 보기를 통해 복잡한 버그의 근본 원인을 찾아 런타임 오류를 일으키는 각 명령문을 단계별로 탐색할 수 있습니다.
소프트웨어 설계 및 코드 이해도 개선
소프트웨어의 제어 및 데이터 흐름을 점검하고 변수 및 연산자와 관련된 범위 정보를 확인할 수 있습니다.
소프트웨어 성능 최적화
안전성 및 보안성이 있는 연산을 식별하여 0으로 나누기와 같은 방어 코드를 제거할 수 있습니다. 어느 실행 경로를 통해서도 도달할 수 없는 코드 분기와 논리 및 프로그램 구조의 오류를 검출하고 이를 제거하여 메모리 사용량을 줄일 수 있습니다.
전역 변수 사용 분석
작업 또는 스레드에 의해 공유되는 변수를 비롯하여 전역 변수에 대한 읽기/쓰기 연산을 디버그하는 데 소비되는 시간을 경감할 수 있습니다. 동시 액세스 그래프를 통해 데이터 경쟁으로 이어지는 제어 및 데이터 흐름을 이해할 수 있습니다. 코드 최적화를 위해 사용되지 않는 전역 변수를 식별할 수 있습니다.
정적 애플리케이션 보안 테스트
잠재적으로 취약한 Ada 명령문에 메모리 액세스, 버퍼 오버플로, 수치 오버플로 등의 총체적인 스트레스를 가하여 응용 프로그램에 치명적인 보안 취약점이 없음을 증명할 수 있습니다. 20가지 CWE 약점 규칙을 지원합니다. Polyspace Client for Ada의 분석 결과를 활용하여 퍼즈 테스트를 보완 또는 대체하고, 취약한 연산에 집중할 수 있습니다.
강건성 및 기능 테스트 개선 및 보완
Polyspace Client for Ada를 사용하면 0으로 나누기 또는 오버플로 등 안전하지 않은 것으로 증명된 명령문을 집중적으로 테스트하여 강건성 테스트를 개선할 수 있습니다. 제어 및 데이터 흐름 분석과 함수 파라미터 및 전역 변수의 계산된 범위를 활용하고 Polyspace Client for Ada의 결과를 사용하여 경계 및 분할 테스트를 생성 및 유지 관리할 수 있습니다.
제품 관련 자료:
Polyspace 제품군
Polyspace 제품은 개발 라이프사이클 전반에 걸쳐 소프트웨어 품질을 테스트하고 모니터링함으로써 중요한 코드의 안정성과 보안성을 향상할 수 있습니다.
Polyspace Access
코딩 결함을 식별하고, 정적 분석 결과를 검토하고, 소프트웨어 품질 메트릭을 모니터링할 수 있습니다.
Polyspace Code Prover Server
소프트웨어에서 런타임 오류의 부재를 증명할 수 있습니다.
Polyspace Bug Finder
정적 분석을 사용하여 소프트웨어 버그를 식별할 수 있습니다.
Polyspace Test
임베디드 시스템 내 C 및 C++ 코드에 대한 테스트 개발, 관리, 실행
Polyspace Bug Finder Server
서버 컴퓨터에서 실행되는 정적 분석을 통해 소프트웨어 결함을 식별할 수 있습니다.
Polyspace Client for Ada
소스 코드에서 런타임 오류의 부재를 증명할 수 있습니다.
Polyspace Code Prover
소프트웨어의 런타임 오류의 부재를 증명할 수 있습니다.
Polyspace Server for Ada
컴퓨터 클러스터에서 검증을 수행하고 메트릭을 퍼블리시할 수 있습니다.
