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

Rodin Project - 航空情報表示システム

ドメイン	航空運輸
開発対象	CCF表示及び情報システム (CDIS)
国	イギリス
開発組織	Rodin Project
形式手法（言語、ツール）	Event-B (Rodin)
適用範囲・規模（形式手法）	既存のCDISシステム (1992年作成) の一部の再構築。 既存のCDISシステムは、VVSL (VDMの一種) で記述され、1200ページの仕様書、3000ページの設計ドキュメントが作成された。 再構築された部分における、Event-Bの抽象仕様は4ページ。
適用対象のソフト種別	エンタプライズ系
適用目的・工程	要求仕様、設計
実装言語
実装規模
効果	[仕様の理解] 抽象的な仕様記述から段階的に詳細化することにより、巨大なシステムの全容の理解を容易にした [バグ排除] 仕様と実際の設計との形式的なリンクを対応させることができた

詳細情報

検証内容

表示されるべきデータが必ず表示されていることを検証した。

検証規模

期間

判断

形式手法を利用した動機

既存のCDISシステムはVVSLを用いて作成されたが、形式的推論は行われていなかった

手法・ツール選択理由

分散システムモデリングに適しているという理由でEvent-Bを採用した

障害と工夫

• 理想的な仕様と現実的な設計との間の形式的なリンクの欠如
-> 理想的な仕様の拡張としてまず抽象仕様を作成した。理想的な仕様では、異なるユーザが異なる場所である変化するデータを見たとき、同じ時刻で見た場合は全く同じデータが見えるはずであるが、実際には遅延等によって異なるデータが見えることがある。これを現実的な抽象仕様として記述するために、履歴トラッキングシステムを導入した。システムは全てのデータ変更の履歴を保持し、ユーザは履歴のいずれかのデータを閲覧することとした。この抽象仕様を徐々に詳細化した。
まず基本的なディスプレイシステムの仕様記述を行い、航空に特化した部分を全て無視することによって、全体をうまく概観できるようにした。Rodinツールを利用してそれを徐々に詳細化していった。各ステップの証明責務はおおよそ20以下で済んだ。
• Event-Bにおいてレコード型をSETS、CONSTANTS、PROPERTIESを利用して表現した。

組織

体制

教育

その他

情報源

Rezazadeh, A. and Evans, N. and Butler, M., Redevelopment of an Industrial Case Study Using Event-B and Rodin, BCS-FACS Christmas 2007 Meeting-Formal Methods In Industry.(December 2007)

このページの先頭へ戻る