鉄道
ClearSy社 - シャルルドゴール空港の無人シャトル制御
| ドメイン |
|
| 開発対象 |
|
| 国 |
|
| 開発組織 |
|
| 形式手法（言語、ツール） |
|
| 適用範囲・規模（形式手法） |
|
| 適用対象のソフト種別 |
|
| 適用目的・工程 |
|
| 実装言語 |
|
| 実装規模 |
|
| 効果 |
|
（出典:Fersil ）
詳細情報
検証内容
-
制御ユニットが、コントロールセンターから無人シャトルの経路についての命令を受け取り、それに基づいて制御ユニットが無人シャトルを制御するシステムにおいて、全ての安全要求を満たしていることを検証した
検証規模
- Bモデルで記述した全ての要素間に矛盾が無いことを検証した
- リファインメントした際に矛盾が生じていないことを検証した
期間
判断
形式手法を利用した動機
-
限られた予算内で、初期リリースからほとんどバグの無い巨大なソフトウェア構築が求められた。特に安全要求への対応が求められた。
手法・ツール選択理由
-
ソフトウェア仕様書がとても精度が低いものであり、システムを理解するためには何らかの形式化が必要であった。
障害と工夫
- 自動リファインメントを行うには問題の規模が大きすぎたため、手動でBモデルを分割した
- 自動リファインメントを実施すると、実行速度が遅いアルゴリズムを採用してしまうことがあったため（本来であれば線形時間で解けるアルゴリズムを指数時間かかるアルゴリズムにしてしまった）、その場合は手動で新しいルールを作成し、適用した
- 仕様書の理解を助けるために、質問/回答データベースを作成し、ClearSyの質問とSiemensの回答の対応付けを行った
- 記述したBモデルが、自然言語で記述された仕様書を正しく表現していることを確認するために、全てのBモデルの要素について、Bモデルを記述していないメンバがチェックした
- Bモデルと自然言語のトレーサビリティを確保するために、Bモデルの各オペレーションにおいてコメントを記述した
組織
体制
教育
-
仕様書を理解するためのドメイン知識及びBの読解能力、記述能力の教育を行った。詳細化のモデルに関してはツールの導入により負荷の軽減を図った。
その他
情報源
-
ClearSy and Siemens Transportation Systems, Using B as a High Level Programming Language in an Industrial Project: Roissy VAL