CVS

center-name

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

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

Web版 トップ頁へ

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

  2. 概要一覧

▼ 話題別に探す
  1. 領域

  2. 形態

  3. 手法

  4. ツール

  5. 実施年度

事例 15: クルーズコントロールシステムの演繹的検証


実施年度2006
概要 オートクルーズコントローラのモデルをAgda上に構築し、基本的な性質の検証を 試みた。
担当者 湯浅 能史
班名 フィールドワーク4班
寄与 企業X,大学Yなど(非公開)
関連する事例 事例 26:制御系ECU調停器の演繹的検証

題材

領域 組み込み(車載ソフトウエア)
題材の詳細
一般的な(特定の製品ではない)クルーズコントローラのモデル。
形態 SCADEモデル、自然言語による仕様書、関連製品マニュアルなど
言語 SCADEの出力図、日本語。
規模 20頁前後
題材の情報源 企業Xの作成によるクルーズコントローラの公開版仕様書。

検証のデータ

目的
Agdaによるモデル化および検証の実験
検証内容
車速が設定速度に収束することを示す(活性の一種?)。
結果
モデルは作成できたが、検証の完成にはいたらなかった。
検証手法 定理証明(演繹手法)
モデル化法 ドキュメントから手動
使用ツール Agda
スケジュール、
労力、時間など
一人×3ヶ月程度
備考 2006年7月より中断。2007年度より再開。

情報源

算譜科学研究速報
(テクニカルレポ-ト)
論文発表
口頭発表 2006年度研究プロジェクト報告会(CVS) 「フィールドワーク4」
知的財産
その他 プロジェクト報告会資料 「フィールドワーク4」 PS-2007-007 システム検証研究センター 2006年度(平成18年度)研究報告集 http://unit.aist.go.jp/cvs/tr-data/PS2007-007.pdf

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