自動車

ClearSy社 - コンポーネント仕様のモデル化

ドメイン
    自動車
開発対象
    車載コンポーネントの機能
    フランス
開発組織
    ClearSy
形式手法(言語、ツール)
    Event B (Atelier B)
適用範囲・規模(形式手法)
  • 一部の機能
  • 50Bモデル
  • 7000イベント
  • 2000抽象変数
  • 1台目は14人年、2台目は5.6人年
適用対象のソフト種別
    制御系
適用目的・工程
    実機テスト
実装言語
実装規模
効果
    自動車の各コンポーネントが、仕様に基づいて正しく作成されているかどうかが確認された

(出典: Peugeot)


詳細情報

検証内容

  • 自動車の全てのコンポーネントについて、正しくて完全なEvent-Bモデルを作成した
  • 実際の自動車のコンポーネントとその挙動と、Event-Bモデルとの明確な対応付けを行った
  • コンポーネントの挙動を記録し、Event-Bモデルと整合しているかどうかの確認を行った

検証規模

期間

判断

形式手法を利用した動機

    従来の不具合発見手法では、複雑化した自動車の不具合を見つけることが困難になってきた

手法・ツール選択理由

    仕様の正確な記述を行う必要があった

障害と工夫

    自動車の全てのコンポーネントについて実機の検証を行うのはコストが大きいため、重要なシナリオのみを対象とした

組織

体制

教育

その他

情報源

    Guilhem Pouzancre, How to diagnose a modern car with a formal B model

このページの先頭へ戻る