形式検証と静的検証が統合されたツール・スイートでプログラムエラーを最小化
『SPARK Pro』は、形式検証可能なAda 2012サブセットの言語を使用し、ソフトウェア検証に数学ベースの信頼性をもたらすツールセットです。
当製品を使用して、ソフトウェア・アーキテクチャ要件を形式的に定義、自動検証。
実行時エラーを削減し、セーフティ・プロパティまたはセキュリティ・ポリシーの適用、機能の正確性 （形式的に定義された仕様への準拠） などの幅広いソフトウェア整合性に対するプロパティを保証する事ができます。
【機能】
■データフロー解析
■インフォメーションフロー解析
■実行時例外の検出
■プロパティチェック
■レベル別検証
※詳しくはPDF資料をご覧いただくか、お気軽にお問い合わせ下さい。
このカタログについて
| ドキュメント名 | 形式検証ツール『SPARK Pro』 |
|---|---|
| ドキュメント種別 | 製品カタログ |
| ファイルサイズ | 94.2Kb |
| 登録カテゴリ | |
| 取り扱い企業 | アイティアクセス株式会社 (この企業の取り扱いカタログ一覧) |
この企業の関連カタログ
このカタログの内容
Page1
Formal Methods
形式検証ツール
形式検証 SPARK Pro
SPARK Proは形式検証と静的検証が統合されたツール・スイート
定理証明を用いて プログラムエラーを最小化
SPARKに備わっている機能
データフロー解析 レベル別検証
非初期化変数参照等、不確実性や不正な • ストーン（Stone）
動作の原因となるエラー検出 SPARK言語の制約事項により、安全なプ
ログラムを記述
インフォメーションフロー解析 • ブロンズ（Bronze）
プログラムを解析して指定されたデータの データフロー解析とインフォメーションフ
依存関係を検証 ロー解析を使用して、非初期化変数の参
照等の広範なエラーを排除
実行時例外の検出 • シルバー（Silver）
ゼロ除算、数値オーバーフロー、バッファ 実行時エラーがないことを検証
オーバーフロー、配列の範囲外インデック • ゴールド（Gold）
スなどの実行時例外を検出 証明（Proof）を使用して、ソフトウェアの重
要なプロパティを検証
プロパティチェック • プラチナ（Platinum）
セーフティやセキュリティプロパティを クリティカルなコードが機能仕様を満たし
contract（事前、事後条件）で記述し検証 ていることを証明
SPARK Proは形式検証後GNAT Proコンパイラでコード生成対応
SPARK Proは、MITREのCommon Weakness Enumeration（CWE）互換性および有効性プログ
ラムによりCWE互換として指定されており、CWEの上位25に含まれる非安全なソフトウェアエ
ラーやコードの弱点を検出
CWEの一例
CWE weakness Description
CWE 120, 123, 124, 125, 126, 127,
Buffer overflow/underflow
129, 130, 131
Variant record field violation, Use of incorrect
CWE 136, 137
type in inheritance hierarchy
AdaCore社の製品は、民間航空機の電子システム、軍事防衛システム、航空管制・制御、
鉄道システム、宇宙システム、自動車、医療機器、金融サービス分野の主要な民間企業や
政府機関を含む世界中のお客様が使用されています。各プロジェクトの概要に関しては、
www.adacore.com/ industries/をご覧ください。
2021.10
AdaCore www.adacore.com ✉ info@adacore.com
代理店：アイティアクセス株式会社 https://www.itaccess.co.jp/service/adv/adacore/ ✉ info@itaccess.co.jp