形式検証ツール『SPARK Pro』

『SPARK Pro』は、形式検証可能なAda 2012サブセットの言語を使用し、ソフトウェア検証に数学ベースの信頼性をもたらすツールセットです。
当製品を使用して、ソフトウェア・アーキテクチャ要件を形式的に定義、自動検証。

実行時エラーを削減し、セーフティ・プロパティまたはセキュリティ・ポリシーの適用、機能の正確性 （形式的に定義された仕様への準拠） などの幅広いソフトウェア整合性に対するプロパティを保証する事ができます。

【機能】
■データフロー解析
■インフォメーションフロー解析
■実行時例外の検出
■プロパティチェック
■レベル別検証

※詳しくはPDF資料をご覧いただくか、お気軽にお問い合わせ下さい。 （詳細を見る）