CVS

center-name

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

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

Web版 トップ頁へ

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

  2. 概要一覧

▼ 話題別に探す
  1. 領域

  2. 形態

  3. 手法

  4. ツール

  5. 実施年度

事例 21: 環境ドライバを用いた組込みシステムのソースコードモデル検査


実施年度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
スケジュール、
労力、時間など


備考

情報源

算譜科学研究速報
(テクニカルレポ-ト)
PS-2007-010, 環境ドライバを用いたモデル検査による検証事例, Toshinori Takai, Takahiro Furuhashi, Hiroyuki Ozaki, Hitoshi Osaki, http://unit.aist.go.jp/cvs/tr-data/PS2007-010.pdf
論文発表
口頭発表
知的財産
その他

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