SPARK Discovery

SPARK DiscoveryはGNAT Proユーザが形式手法を利用して、未実行での非初期化変数の確認、データと情報のフローの正しさ、コードにランタイムエラーがないことなどの検証ができます。

SPARK 言語はAda言語のサブセットで、形式手法に対応しているため、
データアーキテクチャの一貫性(変数とサブプログラムパラメータの適切な使用)から機能の正確性に至るまで、 プログラムのプロパティの検証に、数学を応用しています。

また、SPARK言語はAdaの契約(contract)ベースのプログラミング機能を使用しているため、動的(Adaセマンティクスsemantics)または静的(SPARK証明)にチェックされる契約(contract)と、テストならびに形式手法で検証されるコード両方を記述できます。

形式手法は、ソフトウェアアシュアランスのさまざまなレベルで適用できます。 SPARK Discoveryは、Stoneレベル(SPARKサブセットに準拠)、Bronzeレベル(Stoneレベルとデータフローの検証/非初期化変数の参照の確認)、およびSilverレベル(Bronzeレベル +ランタイムエラーが無いことの検証)の使用に適しています。

SPARK Pro製品は上位のGoldレベル(Silverレベル+整合性の証明)ならびにPlatinumレベル(Gold レベル+機能の正確さの証明)の検証に対応できます。 SPARK DiscoveryとSPARK Proの差異の詳細については、SPARKユーザーガイドを参照してください。