CVS

center-name

AIST
 センター長挨拶Policy Statement研究テーマ研究活動研究成果Technical Reports書籍共同研究集会支援English
 研修コースニュースレター ・CVS Staff ・アクセス 採用情報  ・お問い合わせ ・更新履歴 ・プレスリリース ・カレンダーHOME 

◆ サブ メニュー ◆
Web版 システム検証の事例報告集

Web版 トップ頁へ

▼ 一覧から探す
  1. 項目一覧

  2. 概要一覧

▼ 話題別に探す
  1. 領域

  2. 形態

  3. 手法

  4. ツール

  5. 実施年度

事例 26: 制御系ECU調停器の演繹的検証


実施年度2007
概要 車載ソフトウェアの検証。複数の制御系ECUが発するアクセル・ブレーキ印加 情報を調停し、矛盾のない出力へ統合するユニットを調停器と呼ぶ。ある単純 化された調停器の実装が、調停器としてふさわしい性質を持つことを、対話的 証明支援系を用いて、演繹的な方法で検証した。
担当者 湯浅能史
班名 フィールドワーク4班
寄与 (株)豊田中央研究所
関連する事例 事例 15:クルーズコントロールシステムの演繹的検証

題材

領域 組み込み(車載ソフトウエア)
題材の詳細
     制御系ECUの調停器(研究用に簡略化されたもの)。複数のECUが発するアクセ
     ル/ブレーキ印加情報を一つにまとめる機能を持つ。
形態 SCADEモデル
言語 データフロー図
規模 数頁
題材の情報源 小田 哲也, 潮 俊光, 富永 孝, 佐野 範佳「同期型言語を用いたリアルタイム システムにおける調停機構の検証」第51回システム制御情報学会研究発表講演会

検証のデータ

目的
演繹的ソフトウェア検証の実問題への適用実験。
検証内容
     調停器の基本的な性質として以下の3つを検証。
      (1) 出力において、アクセル印加とブレーキ印加は同時に生じない。
      (2) 出力は入力の最大値を越えない。
      (3) 入力において、アクセル印加とブレーキ印加の競合がなければ、
          入力の最大値をそのまま出力する。
結果
検証に成功した。
検証手法 演繹手法(定理証明による検証)
モデル化法 DFDを高階関数と解釈した数学モデル。手動で作成。
使用ツール 証明支援系 Agda
スケジュール、
労力、時間など
     モデル化と検証項目の設定に一人×2月程度(対象の理解に要した時間も
     含む)。検証に一人×1月程度。
備考

情報源

算譜科学研究速報
(テクニカルレポ-ト)
論文発表
口頭発表 2008/3/13 2007年度研究プロジェクト報告会(CVS) 「フィールドワーク4」
2008/3/19 事例セミナー(CVS) 「クルーズコントロールシステムの演繹的検証」
2008/6/19 情報処理学会、SIGSE-SIGEMB合同研究発表会「制御系ECU 調停器の検証における演繹的アプローチについて」
知的財産
その他

産総研ホーム >  組織 >  研究センター >  システム検証研究センター
Copyrights (C) 2005-2010 AIST Research Center for Verification and Semantics, All Rights Reserved.