航空運輸
Rockwell Collins社 - パイロット用のディスプレーを管理するシステム
| ドメイン |
|
| 開発対象 |
|
| 国 |
|
| 開発組織 |
|
| 形式手法（言語、ツール） |
|
| 適用範囲・規模（形式手法） |
|
| 適用対象のソフト種別 |
|
| 適用目的・工程 |
|
| 実装言語 |
|
| 実装規模 |
|
| 効果 |
|
（出典: NASA LaRC Formal Methods Program Research）
詳細情報
検証内容
-
異なるデータ表示アプリケーションから、適切なディスプレーにデータがルーティングする、ウィンドウマネージャの性質を検証する。
検証規模
期間
判断
形式手法を利用した動機
手法・ツール選択理由
障害と工夫
- 要求仕様を検証する性質に落とし込むこと
- Simulinkなどの商用モデリングツールのデータを異なる種類の形式手法を用いた分析ツールの入力とする、変換ツールを作ること
- 分析結果を分析者と製品エンジニアから分かりやすくするツールを作ること
- アプリケーションを個々に分析できるようなサブシステムに分解する手法を策定すること
- プロセスを改善できるように、検証プロセスを反復していくこと
- Rockwell Collins社とミネソタ大が共同開発した変換フレームワークを利用している。このフレームワークにより、商用モデリングツールの言語から、モデル検査器や定理証明器への変換ができるようになっている。
- 分析結果の妥当性
- ソフトウェア要求仕様からすべての形式的な検証性質が追跡可能であること
- すべての要求項目が少なくとも一つの形式的な検証性質により検証されること
次の3つの要件を満たす検証プロセスを策定すること
組織
体制
教育
-
開発者は１日程度の訓練と作業中の助言だけでモデル検査ツールの実践的な導入が可能
その他
情報源
- Steven P. Miller, Michael W. Whalen, Darren D. Cofer, Software Model Checking Takes Off, Communications of the ACM, February 1, 2010, pp.58-84.
- NASA LaRC Formal Methods Program Research