鉄道

ClearSy社 - シャルルドゴール空港の無人シャトル制御

ドメイン
    鉄道
開発対象
    無人シャトル制御システム
    フランス
開発組織
    ADP (Paris Airport)、Siemens Transportation Systems (STS)、ClearSy
形式手法(言語、ツール)
    B (EDiTh B, Bertille, Atelier B)
適用範囲・規模(形式手法)
  • ソフトウェア仕様ドキュメント: 228ページ(84の機能モジュール)
  • Bモデル: 183,897行
適用対象のソフト種別
    リアルタイム制御系
適用目的・工程
    要求仕様、設計、コード生成
実装言語
    Ada
実装規模
    Ada: 158,612行
効果
  • 限られた予算、納期内で、安全要求を全て満たし、バグがほとんど無いシステムの開発を行えた
  • 開発されたソフトウェアはIEC 61508: EN 50126, EN 50128, EN 50129に準拠。また、SIL4に分類された。

(出典: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

このページの先頭へ戻る