CVS

center-name

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

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

Web版 トップ頁へ

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

  2. 概要一覧

▼ 話題別に探す
  1. 領域

  2. 形態

  3. 手法

  4. ツール

  5. 実施年度

事例 22: 検証期間の調査のための車載組込みシステムに対するモデル検査実験


実施年度2005
概要 モデル検査技術を現場導入するために,検証作業の主要な部分を企業側参加者 が担当し,検査日数を測定した.従来は仕様の検討から検査終了まで2,3ヶ月を 要していたモデル検査による検証が,全体を通じて9日間で終了することが出来 た.また,周期タスク駆動型組込みシステムに対して,抽象などを用いた効果 的なモデル検査プロセスを提案できた.
担当者 大崎人士,尾崎弘幸,小池憲史
班名 フィールドワーク1班
寄与 矢崎総業株式会社
関連する事例 事例 21:環境ドライバを用いた組込みシステムのソースコードモデル検査

題材

領域 組込みソフトウェア
題材の詳細
車載組込みシステムであり,あるセンサー情報をもとに,警報を発する装置.
形態 ソースコード
言語 C言語
規模 システム全体で数万行.検査対象は数千行.
題材の情報源

検証のデータ

目的
機能追加されたソースコードに対して,追加機能だけを検査する手法の確立
および検査期間の調査
検証内容
用意した検査項目32のうち,26でモデル検査による検査をを実施.
「あるセンサー情報が特定の値を示したら,直後に,警報を発する」などの
「直後」という制限がついた応答性など.
結果


検証手法 モデル検査
モデル化法 ソースコードから手作業で Promela でモデル化.
使用ツール Spin
スケジュール、
労力、時間など
モデル検査1
検査方針検討 1.5日×4人
モデル作成 1.5日×1人
検査 2日×1人
モデル検査2
仕様確認 1日×1人
検査方針検討 1.5日×4人
モデル作成 1.5日×1人
検査 3日×3人
備考

情報源

算譜科学研究速報
(テクニカルレポ-ト)
論文発表 河本孝久、小池憲史、古橋隆宏、鈴木伸一, 周期タスク型モデル検査法と車載組 込みシステムへの適用事例, 組込みシステムシンポジウム2007, 東京
口頭発表
知的財産
その他

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