製品の高機能化に伴うシステムの複雑化、ソフトウェアの大規模化などに対応するため、世界中の先進的な組み込みシステムの開発現場では、網羅的・効率的な検証手法の採用が進んでいます。
実績豊富な形式手法である抽象解釈を用いた静的検証は、一般的な静的解析技術と、動的検証のギャップを埋めます。抽象解釈は、プログラムを実行せずに、プログラム内ですべての可能な振る舞いを検査し、ランタイムエラーの有無を数学的に証明します。その網羅的な解析により、ソフトウェアの高い信頼性を確保すると同時に、開発プロセスを効率化することができます。
抽象解釈を用いた静的解析のメリット、世界中で採用されている事例をご覧ください。
その他のリソース
Polyspace Bug Finder、Polyspace Code Proverの無料評価版で、静的解析によるバグの検出を試す
