アジア
ClearSy - 北京地下鉄の自動列車停止システム
| ドメイン |
|
| 開発対象 |
|
| 国 |
|
| 開発組織 |
|
| 形式手法（言語、ツール） |
|
| 適用範囲・規模（形式手法） |
|
| 適用対象のソフト種別 |
|
| 適用目的・工程 |
|
| 実装言語 |
|
| 実装規模 |
|
| 効果 |
|
（出典: 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