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

STS - ニューヨーク地下鉄列車制御システムの最新化

ドメイン	鉄道
開発対象	地下鉄カナーシ線列車制御システム
国	米国
開発組織	STS (Siemens Transportation System)、ニューヨーク市都市交通
形式手法（言語、ツール）	B (Atelier B, Edith B)
適用範囲・規模（形式手法）	設計の早い段階で重要な部分とそうでない部分に分け、全ての重要な機能についてBを適用した。（ただし、低レイヤの入出力、設定ファイル、main関数の無限ループを除く。） Bの抽象モデルを125000行、具体モデルを38000行手動で作成し、EDiTh Bを利用することにより自動的に110000行を生成した。
適用対象のソフト種別	リアルタイム制御系
適用目的・工程	仕様設計、詳細設計
実装言語	Ada
実装規模
効果	簡潔で曖昧性の無い、高品質なソフトウェア仕様を作成することができた。 妥当性検証チームは詳細コードの開発ではなく、仕様の開発に集中することができた。

（出典: Daniel Dolle, B in Large-Scale Projects: The Canarsie Line CBTC Experience, Siemens Transportation Systems, http://www.clearsy.com/pdf/b2007_b_in_large_scale_projects_siemens.pdf）

詳細情報

検証内容

検証規模

証明責務は、抽象モデルが38500個、手動による具体モデルが19000個、自動生成による具体モデルが25000個であった。

期間

2001-2005

判断

形式手法を利用した動機

パリ地下鉄14号線で形式手法（B）を利用した経験があった。

手法・ツール選択理由

• Bを利用することにより、簡潔で曖昧性の無い、高品質なソフトウェア仕様を作成することができる。
• Bはコードが形式仕様のプロパティを維持していることを保証することができる。
• Atelier Bは数万の証明責務を取り扱うことができるほどロバストなツールである。

障害と工夫

STSで開発された半自動詳細化ツールであるEDiTh Bを利用することにより、パリ地下鉄14号線の開発時と比較して大幅に開発効率が向上した。

組織

体制

4人のチームが1年で車載ソフトウェアを開発した。4人のうち2人はパリ地下鉄14号線におけるBを利用した開発の経験者であった。その他1人はBの理論についての知識はあるが開発経験はなく、もう一人はBの知識もなかった。形式手法の専門家は必要としなかった。

教育

その他

情報源

• 形式手法適用調査　調査報告書、情報処理推進機構、2010
• Daniel Dolle, B in Large-Scale Projects: The Canarsie Line CBTC Experience, Siemens Transportation Systems, http://www.clearsy.com/pdf/b2007_b_in_large_scale_projects_siemens.pdf

このページの先頭へ戻る