CVS

center-name

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

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

Web版 トップ頁へ

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

  2. 概要一覧

▼ 話題別に探す
  1. 領域

  2. 形態

  3. 手法

  4. ツール

  5. 実施年度

事例 5: 自動検針システム仕様書のモデル検査


実施年度2002
概要 自動検針システムの仕様書を題材にモデル検査を行った。仕様書を作成した時 に実施された査読では見つからなかった仕様書中の矛盾、記述不足の不具合を モデル検査で発見することができた。
担当者 早水公二、高橋孝一、渡邊宏
班名
寄与 関西電力との共同研究、篠崎孝一(関西電力)、文科省科振費
関連する事例

題材

領域 仕様書、通信プロトコル
題材の詳細
題材は自動検針システムの仕様書である。仕様書はこのモデル検査実験のため
に特徴的な機能に絞り来んで新たに作成した。題材の仕様書はテクニカルレポー
トの附属書として公開されている。

自動検針システム自体は企業で開発・試作された実験用のシステムで、「セン
タ」、「GW」、「WHM」の3つの設備から構成され、センタ〜GW間、G
W〜WHM間にそれぞれ双方向の通信路がある。センタからの遠隔操作によっ
て、GWを介してWHMのメータ値の読み取り、データの設定を行うシステム
である。センタはGWに対して要求を出力して、その要求に対する応答として
GWから処理結果の報告を入力する。GWはセンタからの要求に応じて、WH
Mに対して指令データを出力して、WHMの電力メータ値の読み込み、WHM
のパターンデータ設定を行う。WHMはGWからの指令データに応じて電力メー
タ値の返送、パターンデータ設定の処理を行い、指令データに対する応答とし
てGWに返送を出力する。
形態 仕様書
言語 日本語
規模 16ページ
題材の情報源 関西電力総合技術研究所にて開発・試作された実験用システムの動作を参考に、 検証担当者が仕様書を作成した。

検証のデータ

目的
仕様書へモデル検査を適用してみる。
検証内容
システム仕様書に書かれた文章から読み取れる各設備の動作仕様すべてとシス
テム全体の動作仕様を検査した。大雑把に数えるとCTL論理式 50個。

システム全体の動作仕様としては、次の二つを検査項目とした。
(a)パターン設定完了の確認
「センタから要求が出力されれば、最終的にWHM内でのパターン設定が完了す
ること」
(b)初期状態への再帰可能性
「いかなる状態からでも再び初期状態へ戻ることができること」
結果
次の二種類の仕様書の不具合を発見した。

二つの相矛盾する仕様
「メモリをデータで上書きする」仕様と「メモリを空データで上書きする」二
つの両立できない事象が同時に発生する可能性がある。発生した場合の優先度
を設定する必要があった。

仕様の記述不足によるフリーズ(ライブロック)
GWが電源異常の場合、センタがずっと待機状態におちいる可能性があった。タ
イムアウトを書き忘れていた。
検証手法 モデル検査
モデル化法 手動
使用ツール SMV
スケジュール、
労力、時間など
2ヶ月程度
備考

情報源

算譜科学研究速報
(テクニカルレポ-ト)
PS03-005, モデル検査器を用いた自動検針システムの仕様検証, 早水公二, 篠崎孝一, 高橋孝一, 渡邊宏, 本文 http://unit.aist.go.jp/cvs/tr-data/HONBUN.PDF,
付属書1 http://unit.aist.go.jp/cvs/tr-data/1.PDF,
付属書2 http://unit.aist.go.jp/cvs/tr-data/2.PDF,
付属書3 http://unit.aist.go.jp/cvs/tr-data/3.PDF
論文発表
口頭発表 モデル検査器を用いた自動検針システムの仕様検証, 早水 公二、篠崎 孝一(関西電力株式会社)、高橋 孝一、渡邊 宏, 情報処理学会 第43回プログラミング研究会,東京都港区芝浦、2003/03/18
知的財産
その他

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