CVS

center-name

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

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

Web版 トップ頁へ

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

  2. 概要一覧

▼ 話題別に探す
  1. 領域

  2. 形態

  3. 手法

  4. ツール

  5. 実施年度

事例 25: Real-Time Maude によるモデル検査と検査式・ モデルの修正


実施年度2007年度
概要 本研究では, 実際のシステムに基づいて作成した架空の生産システムの仕様に モデル検査を適用し, その不具合の発見とその修正を行った. さらに, そのモデル検査のプロセスを考察し, 次の2つに関する提案を行った: 1. 見つけたい反例を選びたすための検査式の作成方法. 2. 対象システムに対する修正の効果と妥当性をモデル検査によって検討する 方法.
担当者 中野昌弘,高井利憲
班名 フィールドワーク1班
寄与 矢崎総業株式会社
関連する事例

題材

領域 組込みソフトウェア
題材の詳細
検証対象は実際の組込みシステムから作り出した, 架空の生産システムの仕様
である.
その生産システムは全体の電源スイッチ(F1)を持ち,
その電源スイッチがoffのときだけ, 観測対象である加工区画αに原料を追加し,
加工して排出する.

α内にはセンサーが設置されており, α内に残存する原料の量を計測する.
ただし, αの状態は加工始動スイッチ(F2)をonにしてからoffなるまでの一定時
間は安定しないことから,
センサーによって計測される値はα内の原料の残存量を必ずしも正確には示さない.
このため, この生産システムにはセンサーによって計測した値から安定した状
態のとき値を選択し出力する安定値出力システムを備えている.
このシステムは停止(v0), 初期化(v1), 稼働(v2), 終了(v3)という,
加工区画の振舞いを表現する4つののロケーションからなる状態遷移図で表現
される.
さらに, 安定値出力システムは安定値を出力するだけでなく,
それ以前に出力した安定値と最新の安定値を比較して値が増大していた場合は,
原料の増加があったということを検出する.
形態 仕様書
言語 日本語・その他
規模 13ページ(A4)
題材の情報源

検証のデータ

目的
仕様に対するモデル検査の適用を通して,
次の2つを考察する:
1. 見つけたい反例を選びたすための検査式の作成方法.
2. 対象システムに対する修正の効果と妥当性をモデル検査によって検討する
方法.
検証内容

前述「22.検証対象詳細」において述べた安定値出力システムに対して,
実際のシステムを使用する際に最も優先度が高い要求仕様として挙げられた
次の2つ検証項目として設定した:
a. 加工区画αに一定量の増加があった場合、安定値出力システムは
加工区画が稼働している状態(v2, 安定値出力システムのロケーション)にあ
るときその増加の検出を行う.
b. 加工区画が稼働している状態(v2)に入ってから停止状態(v0)に遷移す
るまでには, ある一定以上の時間を要する.

なお, aに関する検証については最初に与えられた仕様(i)と, その後与えられ
た(i)とは一部異なる仕様(ii)に対して行われた.
また, bについては, 仕様(ii)に対して行った.
結果
仕様(i)に対する検証.

まず, 自明な反例が検出される度に, それらの反例を検出しないよう,
検査式に修正を加えていき, 幾度目かの修正によって自明でない反例を検出した.
その後, (1)がvalidにならない原因を明らかにするため,
さらに様々な自明でない反例を検出することを目標に,
すでに検出した反例をさらに検出しないよう,
検査式に修正を加えながら検査を行った.
その結果, 実際に不具合の原因が明らかになった.

また, その際, 検査式の修正によって様々な反例を得るための方法も与えるこ
とができた.

さらに, 原因が明らかになったことから,
それに対するもとの仕様(i)の修正案を与えることができた.
そこで, その修正案に基づいてモデルを変更したのち,
そのモデルに対して同様の検査を行った.
その結果, 修正案が妥当であることが確認できた.

以上をまとめると,
(1)複数の反例導出による原因の明確化,
(2)仕様修正案を策定,
(3)修正案に基づくモデルの変更と, 修正案のの妥当性の確認を目的とした
変更後のモデルに対する検査,
という, モデル検査による不具合検出とその修正のプロセスを考案した.



仕様(ii)に対する検証.

仕様(ii)に対してモデル化を行い, まずaに関する検査を行い,
幾つかの反例が得られたものの, 概ねaを満たすことが明らかになった.
そして, bに関しては満たされることが分かった.

なお, Real-Time Maudeを用いた本研究の前に, SPINを用いてbに関する同様の
検査をで試みたところ, 検査が完了しなかった.
このことに関する詳細な考察は行っていない.
検証手法 モデル検査
モデル化法 仕様書から状態遷移図を抽出し、 状態遷移を書き換え規則として表現
使用ツール Real-Time Maude
スケジュール、
労力、時間など
1名で約3ヶ月

備考

情報源

算譜科学研究速報
(テクニカルレポ-ト)
Real-Time Maude によるモデル検査事例と検査式およびモデルの修正方法, 中野昌弘、高井利憲, 第四回システム検証の科学技術シンポジウム講演論文集, 算譜科学研究速報, PS-2008-002, pp. 57-68, http://unit.aist.go.jp/cvs/tr-data/PS2008-002-revise.pdf
論文発表
口頭発表 第4回システム検証の科学技術シンポジウム, 名古屋大学, 2007年11月
知的財産
その他

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