|
◆ サブ メニュー ◆
Web版 システム検証の事例報告集
▼ Web版 トップ頁へ
▼ 一覧から探す
-
項目一覧
-
概要一覧
▼ 話題別に探す
-
領域
-
形態
-
手法
-
ツール
-
実施年度
|
| 実施年度 | 2004 |
| 概要 |
モデル検査により，既知の不具合の発見可能であるかの調査が目的である．先
の実験で考案した環境ドライバというモデル検査法が適用可能であるかを調べ
た．結果として，既知の不具合をモデル検査で発見でき，先の実験で考案した
サイクリックエグゼクティブ型組込みソフトウェアに対する効果的なモデル化
法である環境ドライバを用いた方法が本実験でも適用可能であることも示すこ
とができた．
|
| 担当者 |
尾崎弘幸，大崎人士
|
| 班名 |
フィールドワーク1班
|
| 寄与 |
(非公開)
|
| 関連する事例 |
事例 22:検証期間の調査のための車載組込みシステムに対するモデル検査実験
|
題材
| 領域 |
組込みソフトウェア
|
| 題材の詳細 |
製品 A ，その後継製品Bおよびそのバグフィックス版 B'．製品 A のバグαは，
製品 B で修正されているが，その修正によりバグ βが製品 B には含まれている．
バグ βが修正された製品 B を B' と呼ぶ．
|
| 形態 |
ソースコードがメインで一部仕様書
|
| 言語 |
C言語
|
| 規模 |
対象システムはC言語で数万行規模．検査対象タスクを記述した関数は数百行程
|
| 題材の情報源 |
（非公開）
|
検証のデータ
| 目的 |
1. 既知の不具合がモデル検査で発見可能であるか，の調査
2. 修正した不具合が正しく修正されているか，の調査
3. 先の検証で考案した環境ドライバが適用可能であるか，の調査
|
| 検証内容 |
・製品 A に含まれるバグ α の検出
・製品 B に含まれるバグ β の検出
・製品 B ではバグ α は修正されていることの確認
・製品 B' ではバグ α およびバグ βは修正されていることの確認
|
| 結果 |
・製品 A に含まれるバグ α を表す反例を得る
・製品 B に含まれるバグ β を表す反例を得る
・製品 B ではバグ α に対応する検査式は反例無し
・製品 B' ではバグ α およびバグ βは対応する検査式は反例無し
|
| 検証手法 |
モデル検査
|
| モデル化法 |
プログラムから手動
|
| 使用ツール |
Spin
|
スケジュール、
労力、時間など |
|
| 備考 |
|
情報源
|
