アイティアクセス株式会社 形式検証ツール『SPARK Pro』
- 最終更新日：2021-10-29 15:05:23.0
- 印刷用ページ
形式検証と静的検証が統合されたツール・スイートでプログラムエラーを最小化
『SPARK Pro』は、形式検証可能なAda 2012サブセットの言語を使用し、ソフトウェア検証に数学ベースの信頼性をもたらすツールセットです。
当製品を使用して、ソフトウェア・アーキテクチャ要件を形式的に定義、自動検証。
実行時エラーを削減し、セーフティ・プロパティまたはセキュリティ・ポリシーの適用、機能の正確性 （形式的に定義された仕様への準拠） などの幅広いソフトウェア整合性に対するプロパティを保証する事ができます。
【機能】
■データフロー解析
■インフォメーションフロー解析
■実行時例外の検出
■プロパティチェック
■レベル別検証
※詳しくはPDF資料をご覧いただくか、お気軽にお問い合わせ下さい。
基本情報形式検証ツール『SPARK Pro』
【レベル別検証】
■ストーン（Stone）
・SPARK言語の制約事項により、安全なプログラムを記述
■ブロンズ（Bronze）
・データフロー解析とインフォメーションフロー解析を使用して、
非初期化変数の参照等の広範なエラーを排除
■シルバー（Silver）
・実行時エラーがないことを検証
■ゴールド（Gold）
・証明（Proof）を使用して、ソフトウェアの重要なプロパティを検証
■プラチナ（Platinum）
・クリティカルなコードが機能仕様を満たしていることを証明
※詳しくはPDF資料をご覧いただくか、お気軽にお問い合わせ下さい。
| 価格帯 | お問い合わせください |
|---|---|
| 納期 | お問い合わせください |
| 用途／実績例 | ※詳しくはPDF資料をご覧いただくか、お気軽にお問い合わせ下さい。 |
カタログ形式検証ツール『SPARK Pro』
取扱企業形式検証ツール『SPARK Pro』
-
-
■Trading Company Function ■System Integrator Function ■Manufacturer Function
形式検証ツール『SPARK Pro』へのお問い合わせ
お問い合わせ内容をご記入ください。
