アジア

ClearSy - 北京地下鉄の自動列車停止システム

ドメイン
    鉄道
開発対象
    地下鉄の自動列車停止システム
    中国
開発組織
    ClearSy、ALSTOM
形式手法(言語、ツール)
    B (Atelier B)
適用範囲・規模(形式手法)
適用対象のソフト種別
    リアルタイム制御系
適用目的・工程
    仕様設計、詳細設計、自動コード生成
実装言語
    Ada
実装規模
効果
  • 仕様が満たされることが数学的に証明された。
  • リファインメントを繰り返し、最終的にAdaコードを生成した。

(出典: ClearSy社Webページ, http://www.fersil-railway.com/php/projet-urbalis-evolution-en.php)


詳細情報

検証内容

    安全が保証されない状態になったとき、緊急ブレーキがかかることを検証した。

検証規模

期間

    2006-2008

判断

形式手法を利用した動機

手法・ツール選択理由

障害と工夫

組織

体制

    Alstom社のチームが形式的に仕様設計を行った。この仕様を、ClearSy社のチームがAlstom社のチームと連携してBを用いて形式化した。

教育

その他

情報源

    ClearSy社Webページ, http://www.fersil-railway.com/php/projet-urbalis-evolution-en.php

このページの先頭へ戻る