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

イギリス国防省 - SHOLIS(ヘリコプタ着陸システム）

ドメイン	航空運輸
開発対象	艦載ヘリコプタ運行システム
国	イギリス
開発組織	PMES (Power Magnetics and Electronic Systems)、Praxis Critical Systems
形式手法（言語、ツール）	Z (CADiZ tool)、SPARK (Examiner, Simplifier, Proof Checker)
適用範囲・規模（形式手法）	要求ドキュメントは4000行以上。ソフトウェア要求仕様はZ、英語、数学的定義を含めて300ページ。
適用対象のソフト種別	リアルタイム制御系
適用目的・工程	要求仕様（Z）、設計（Z、SPARK）、コード記述（SPARK）
実装言語	SPARK
実装規模	133000行（Ada宣言13000行、Ada文14000行、SPARK flow アノテーション54000行、SPARK proof アノテーション20000行、空白行やコメント32000行）
効果	UK Interim Defense Standard (IDS) 00-55及び00-56への準拠

（出典: イギリス国防省ホームページ）

詳細情報

検証内容

• 最も重要なSafetyプロパティは「あるセンサの値が現在のSHOL (Ship Helicopter Operating Limits, 操作を行う際の許される値) の範囲を逸脱していた場合は警告が出され、センサの値がSHOLの範囲に収まっていた場合は警告が出されない」ということであり、これはZを用いて証明された。
• グローバル変数や定数の一貫性、初期状態の存在、事前条件の検査をZを用いて実施した。
• 障害発見比率は以下のとおりである。（障害発見比率/工数比率）を計算すると、Zによる証明の工程が、最も効率的に障害を発見していることがわかる。

工程	障害発見比率[%]	工数比率 [%]
仕様	3.25	5
Zによる証明	16	2.5
概念設計	1.5	2
詳細設計、実装、簡易テスト	26.25	17
単体テスト	15.75	25
統合テスト	1.25	1
コードの証明	5.25	4.5
システム妥当性テスト	21.5	9.5
受け入れテスト	1.25	1.5
その他（スタッフの教育、プロジェクト管理と計画、安全管理等）	8	32

検証規模

期間

1996年 - 1997年

判断

形式手法を利用した動機

• UK Interim Defense Standard (IDS) 00-55及び00-56に準拠する必要があった。これは、形式的な安全管理及び品質システム、システムの振る舞いの形式仕様、仕様及びコードレベルの両方における形式検証、プログラムプロパティ（インフォメーションフロー、タイミングやメモリ使用量等）の静的解析を要求する。
• テストを実施するよりも、形式手法による検証を実施するほうがコスト面で有利であった。

手法・ツール選択理由

SPARKを利用した理由は、論理的な健全性、簡潔な形式記述、表現力、セキュリティ、検証性、実行時の時間と使用リソース量である。

障害と工夫

組織

体制

• 検証は4人の技術者によって実施された。二人はZの検証を担当した。このうちの一人と残り二人は、Zの仕様に基づいてSPARK検証アノテーションを生成し、SPARKの検証を実施した。
• 全ての技術者は、ZやCSP等の形式手法に数年間関わっていた。しかし、SPARK SimplifierやProof Checkerを使ったことがあるのは一人だけであった。

教育

その他

情報源

Steve King, Jonathan Hammond, Rod Chapman, and Andy Pryor, Is Proof More Cost Effective than Testing?, IEEE Transactions on Software Engineering, Vol 26, No 8, August 2000

このページの先頭へ戻る