CVS

center-name

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

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

Web版 トップ頁へ

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

  2. 概要一覧

▼ 話題別に探す
  1. 領域

  2. 形態

  3. 手法

  4. ツール

  5. 実施年度

事例 1: 通信プロトコル設計へのモデル検査適用事例


実施年度2006
概要 プロトコルの設計過程の中でモデル検査をして設計を支援した。
担当者 高村博紀,渡邊宏
班名 フィールドワーク5班
寄与 古野電気株式会社との共同研究、吉川達(古野電気)、平岡康(古野電気)
関連する事例

題材

領域 プロトコル、組み込み
題材の詳細
専用線で結ばれた二つの通信機器の間のプロトコルの設計過程で作られる設計モデル。
プロトコルは次の四つの機能要求を満たすものに設定した。
1. 双方向にデータ送受信を行う、
2. 起動通知確認機能を持つ、
3. ウォッチドッグ機能を持つ、
4. スリープ機能を持つ
設計モデルは通信機器それぞれの振舞いを記述した状態遷移表。
形態 仕様書
言語 日本語
規模 通信機一つあたり、12状態で29種類のイベントからなる状態遷移表。
題材の情報源 古野電気株式会社

検証のデータ

目的
設計途中にモデル検査を導入する方法、
設計のバグ取りにモデル検査を使う方法を検討する。
検証内容
3段階の工程にわけて設計を行い、各段階で論理式を回帰的に検査した。検査
した性質は、状態遷移表の各状態への到達可能であること、デッドロックしな
いこと、エラー処理すること、4つの機能要求が満たされることなどである。
作成した論理式は全部で200個程度。
さらに、ラインが切れたり、データ化けしたりすることを想定したモデルを作り、
そこで不具合が生じないことも検査した。
結果
設計のバグ取りとして十分に使えた。
モデルを作成する段階で、設計の不備に気づくこともあった。
検証手法 モデル検査
モデル化法 手動
使用ツール UPPAAL
スケジュール、
労力、時間など
設計作業も含めて32人・日程度。
備考

情報源

算譜科学研究速報
(テクニカルレポ-ト)
計画中
論文発表 通信プロトコル設計におけるモデル検査法の適用事例, 高村 博紀 (CVS/AIST) 平岡 康 (古野電気) 吉川 達 (古野電気) 渡邊 宏 (CVS/AIST) , 第5回ディペンダブルシステムワークショップDSW2007論文集, 日本ソフトウェア科学会研究資料シリーズ No. 48, 31-34, 2007
口頭発表 第5回ディペンダブルシステムワークショップ(DSW07_summer), 通信プロトコル設計におけるモデル検査法の適用事例, 高村 博紀 (CVS/AIST) 平岡 康 (古野電気) 吉川 達 (古野電気) 渡邊 宏 (CVS/AIST) , 2007年7月3日
知的財産
その他

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