ホーム > 応用事例DB > 地域 > EU

EU

ClearSy - パリ地下鉄プラットフォームドアの制御

ドメイン
    鉄道
開発対象
    プラットフォームドアのコマンドコントローラ
国
    フランス
開発組織
    RATP、ClearSy
形式手法（言語、ツール）
    B (COMPOSYS, B4Free, Atelier B, Brama Animator)
適用範囲・規模（形式手法）
  • 1300ページのドキュメント
  • セーフティケースは15のドキュメントがあり、300ページ
  • Bモデルは3500行
適用対象のソフト種別
    リアルタイム制御系
適用目的・工程
    システム仕様設計、ソフトウェア仕様設計、コード検証
実装言語
    LADDAR
実装規模
効果
    テスト工程において、ソフトウェアの異常が一つも発見されなかった。

（出典: Guilhem Pouzancre, A Formal Approach in the Implementation of a Safety System for Automatic Control of "Platform Doors", 2006, http://www.composys.eu/resources/AFIS/Clearsy%20AFIS%202006%20Slides_03_05_2006_en.pdf）


詳細情報

検証内容

  • 列車とプラットフォームとの間に不適切な接続が確立されないこと
  • 列車と線路との間に不適切な接続が確立されないこと

検証規模

    1000の証明責務があり、90%を自動証明、残りを2日間でAtelier B interactive proverを用いて証明した。

期間


    2006（10か月）
  • システムアーキテクチャの定義　2か月
  • システム設計および安全性の実証　4か月
  • 3つのプラットフォームへの導入　4か月

判断

形式手法を利用した動機

    IEC 50126、50128、50129等に対応する必要があった。

手法・ツール選択理由

    信頼性の確保および、プロジェクト全体を通してのトレーサビリティの確保のため、プロジェクトのほとんどの工程で利用可能であるBを利用した。

障害と工夫

  • 列車の到着・出発をセンサを利用して検知するが、安全性の高いセンサは高価であった。そのため、比較的安価なセンサを利用し、それを多重化することでシステム全体の安全性を高めた。
  • PSDコントローラのアーキテクチャに依存しない過去の機能解析の結果を再利用した。
  • PLCとしてSIL3互換のSiemens7を利用しており、SIL3を維持するためにはSiemens7のGUIをとおしてのLADDER言語でのプログラミングが要求されていた。そのため、BをLADDARへ変換する際に時間制約などを検証するための最適化手法などを導入した。

組織

体制

    プロジェクトマネージャ、開発エンジニア、セーフティエンジニア、検証エンジニア

教育

その他

情報源

  • Thierry Lecomte, Thierry Servat, Guilhem Pouzancre, Formal Methods in Safety-Critical Railway Systems, 2007, http://deploy-eprints.ecs.soton.ac.uk/8/1/fm_sc_rs_v2.pdf
  • Guilhem Pouzancre, A Formal Approach in the Implementation of a Safety System for Automatic Control of ""Platform Doors"", 2006, http://www.composys.eu/resources/AFIS/Clearsy%20AFIS%202006%20Slides_03_05_2006_en.pdf
  • 形式手法適用調査　調査報告書、情報処理推進機構、2010

カテゴリ

, , ,

このページの先頭へ戻る