ディペンダブル・システムのための形式手法の実践ポータル

Lockheed Martin、Praxis - C130Jミッションコンピュータ

ドメイン	航空運輸
開発対象	航空制御システム
国	イギリス
開発組織	Lockheed Martin、Praxis
形式手法（言語、ツール）	CoRE、SPARK (SPARK Examiner, SPADE Automatic Simplifier, SPADE Proof Checker)
適用範囲・規模（形式手法）	ソフトウェアのコアとなる部分（全体の80%）
適用対象のソフト種別	リアルタイム制御系
適用目的・工程	要求仕様（CoRE）、コード記述・検証 (SPARK)
実装言語	SPARK
実装規模	200K行程度
効果	人手で行う場合は30日かかるようなバグの発見が、SPARK Examinerを利用することで1時間で発見できた。

（出典: Lockheed Martin社ウェブサイト）

詳細情報

検証内容

• CoREで記述された仕様とコードから、SPARKでProof Obligationを生成し、検証を行った。
• 多くの証明責務はSPADE Automatic Simplifierを用いて証明できた。残りはSPADE Proof Checkerを用いて対話的に証明した。

検証規模

期間

判断

形式手法を利用した動機

DO178BのレベルAへの準拠が要求されていた。ここでは、MC/DCテストカバレッジが要求されている。このテストは多大な時間を要するため、出来るだけ1回限りの実行で終わらせたいという動機があった。そのため、MC/DCテストを実行するまえに、全てのバグを発見しておく必要があった。

手法・ツール選択理由

• 本ドメインにおいて、SPARKは多くの導入事例があったため。
• ソフトウェアに多くの入力と出力がある場合は、CoREが適合しているため。

障害と工夫

• 効率よく検証を行うため、コードの構造をできるだけ単純化した。たとえば、事前定義のチェックなどをコードから削除した。
• プログラムユニットの実装及び検証を別々に実施した。

組織

体制

教育

その他

情報源

"Roderick Chapman, Industrial Experience with SPARK, ACM SIGAda Ada Letters - special issue on presentations from SIGAda 2000 Martin Croxford and James Sutton, Breaking Through the V and V Bottleneck, Lecture Notes in Computer Science, Vol 1031, 1996"

このページの先頭へ戻る