CVS

center-name

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

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

Web版 トップ頁へ

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

  2. 概要一覧

▼ 話題別に探す
  1. 領域

  2. 形態

  3. 手法

  4. ツール

  5. 実施年度

事例 29: 仕様処理システムの適用実験事例


実施年度2009
概要 仕様書の形式化の試験
担当者 矢田部俊介
班名 地域イノベーション班
寄与 CSKシステムズ西日本、CSKシステムズ、マックス(評価実施者)
関連する事例

題材

領域 組込(家電製品)
題材の詳細
電気ポットの仕様書(話題沸騰ポット要求仕様書 (GOMA-1015型) 第7版)
形態 自然言語でかかれた要求仕様書(抽象度の高い状態遷移図を含む)
言語 日本語
規模 15ページ
題材の情報源 組込みソフトウェア管理者・技術者育成研究会(SESSAME)作成

検証のデータ

目的
地域イノベーション創出研究開発事業で開発したツール「仕様処理システム」の
実用性の実証実験
検証内容
実際の仕様書から、統一仕様書式のプロトタイプを使用して用語集の作成し、
ツールが仕様書の形式化作業をどの程度有効に支援できるかを調べる。
また仕様書から抽出した用語が、正しく使われているか(型安全であるか)を
型検査によって判定する。
結果
話題沸騰ポット要求仕様書(第7版)の形式化作業を行った。この仕様書は
細かい設定が多いため、抽出はし易い。特に遷移関係が遷移図と遷移表で
表されていたため、抽出作業が確実に出来、また初期値についての記述も多く、
語彙抽出作業は進みやすかった。形式化作業については、おおむねツールで
サポートできるとの結論を得た。なお、型検査に合格した。
検証手法 型検査
モデル化法 仕様処理システムにより自動生成(モデルは統一仕様書式(XML)により記述、 Agda言語に自動翻訳し型検査を行う)
使用ツール 仕様処理システム(およびAgda)を使用
スケジュール、
労力、時間など
用語抽出と入力は 1人×3〜4日
状態遷移情報の抽出と入力も同じく 1人×3〜4日
データの改訂等もあわせ、全体として10日〜14日使用した。
備考 本作業は、マックスの研究員三名が行った。

情報源

算譜科学研究速報
(テクニカルレポ-ト)
論文発表
口頭発表
知的財産
その他

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