◆ サブ メニュー ◆ Web版 システム検証の事例報告集
▼ Web版 トップ頁へ
▼ 一覧から探す
-
項目一覧
-
概要一覧
▼ 話題別に探す
-
領域
-
形態
-
手法
-
ツール
-
実施年度
|
実施年度 | 2006 |
概要 |
オートクルーズコントローラのモデルをAgda上に構築し、基本的な性質の検証を
試みた。
|
担当者 |
湯浅 能史
|
班名 |
フィールドワーク4班
|
寄与 |
企業X,大学Yなど(非公開)
|
関連する事例 |
事例 26:制御系ECU調停器の演繹的検証
|
題材
領域 |
組み込み(車載ソフトウエア)
|
題材の詳細 |
一般的な(特定の製品ではない)クルーズコントローラのモデル。
|
形態 |
SCADEモデル、自然言語による仕様書、関連製品マニュアルなど
|
言語 |
SCADEの出力図、日本語。
|
規模 |
20頁前後
|
題材の情報源 |
企業Xの作成によるクルーズコントローラの公開版仕様書。
|
検証のデータ
目的 |
Agdaによるモデル化および検証の実験
|
検証内容 |
車速が設定速度に収束することを示す(活性の一種?)。
|
結果 |
モデルは作成できたが、検証の完成にはいたらなかった。
|
検証手法 |
定理証明(演繹手法)
|
モデル化法 |
ドキュメントから手動
|
使用ツール |
Agda
|
スケジュール、 労力、時間など |
一人×3ヶ月程度
|
備考 |
2006年7月より中断。2007年度より再開。
|
情報源
|