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