自動車
ClearSy社 - コンポーネント仕様のモデル化
| ドメイン |
|
| 開発対象 |
|
| 国 |
|
| 開発組織 |
|
| 形式手法（言語、ツール） |
|
| 適用範囲・規模（形式手法） |
|
| 適用対象のソフト種別 |
|
| 適用目的・工程 |
|
| 実装言語 |
|
| 実装規模 |
|
| 効果 |
|
（出典: Peugeot）
詳細情報
検証内容
- 自動車の全てのコンポーネントについて、正しくて完全なEvent-Bモデルを作成した
- 実際の自動車のコンポーネントとその挙動と、Event-Bモデルとの明確な対応付けを行った
- コンポーネントの挙動を記録し、Event-Bモデルと整合しているかどうかの確認を行った
検証規模
期間
判断
形式手法を利用した動機
-
従来の不具合発見手法では、複雑化した自動車の不具合を見つけることが困難になってきた
手法・ツール選択理由
-
仕様の正確な記述を行う必要があった
障害と工夫
-
自動車の全てのコンポーネントについて実機の検証を行うのはコストが大きいため、重要なシナリオのみを対象とした
組織
体制
教育
その他
情報源
-
Guilhem Pouzancre, How to diagnose a modern car with a formal B model