EU

ボンバルディア - 鉄道制御システム

ドメイン
    鉄道
開発対象
    Deutsche Bahn社の無線鉄道制御システム
    ドイツ
開発組織
    ボンバルディア
形式手法(言語、ツール)
    Rational Statemate/LSC (Live Sequence Chart)
適用範囲・規模(形式手法)
適用対象のソフト種別
    リアルタイム制御系
適用目的・工程
    要件定義、システム設計、ソフトウェア設計
実装言語
実装規模
効果
    形式的に要求を記述することにより、仕様の厳密さが高まり、再利用性も向上した。

(出典: Brill, M. and Buschermohle, R. and Damm, W. and Klose, J. and Westphal, B. and Wittke, H., Formal verification of LSCs in the development process, Integration of Software Specification Techniques forApplications in Engineering, pp.494--516, 2004)


詳細情報

検証内容

  • 列車が地上子などのアクティベーションポイントに近づいたら必ず通信チャネルがセットアップされる。

検証規模

期間

判断

形式手法を利用した動機

  • 開発するコンポーネントが安全要求を満たしていることを保証するため。
  • モデル検査はテストと異なり全ての入力および入力の組合せについて検査することができるため。

手法・ツール選択理由

    Statemateに組み込まれているLive Sequence Chartsはよく知られているMSC2000のMessage Sequence ChartやUMLのシーケンス図を基にしており、クリティカルな通信プロトコルの記述および検証に向いているため。

障害と工夫

    モデル検査はモデルを解析するのみであり、ハードウェアやソフトウェアの実装に関して検証するものではない。そのため、作成したモデルから自動的にテストを作成し、実装に適用した。

組織

体制

教育

その他

情報源

  • Bohn, J. and Damm, W. and Klose, J. and Moik, A. and Wittke, H. and Ehrig, H. and Kramer, B. and Ertas, A., Modeling and validating train system applications using statemate and live sequence charts, IDPT, 2002
  • Brill, M. and Buschermohle, R. and Damm, W. and Klose, J. and Westphal, B. and Wittke, H., Formal verification of LSCs in the development process, Integration of Software Specification Techniques forApplications in Engineering, pp.494--516, 2004

このページの先頭へ戻る