CVS

center-name

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

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

Web版 トップ頁へ

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

  2. 概要一覧

▼ 話題別に探す
  1. 領域

  2. 形態

  3. 手法

  4. ツール

  5. 実施年度

事例 14: 非自動はかりの重量データ処理プログラムのモデル検査適用事例


実施年度2002
概要 非自動はかりの重量データ処理プログラムの検証にモデル検査を適用した。 勧告OIML R76-1の中の条項 "4.5.7 Zero-tracking device: A zero-tracking shall operate only when the equilibrium is stable." をLTL論理式で記述し、SMV で検証を行った。
担当者 松岡聡、高橋孝一
班名
寄与 (株)イシダとの共同研究、内藤和文、小島章充(以上当時(株)イシダ)
関連する事例

題材

領域 組込み
題材の詳細
ロードセルに接続されたA/Dコンバーターから受け取ったデータを
さまざまなコマンドに応じて処理を行う、および、データのフィルター処理を
行うルーチンにモデル検査を適用した。
形態 仕様書
言語 フローチャート
規模 フローチャートで数10ページ
題材の情報源 (株)イシダ

検証のデータ

目的
モデル検査がどのようなものか共同研究相手先へデモする。
検証内容
非自動はかりOIML R76-1の中の条項 "4.5.7 Zero-tracking device:
A zero-tracking shall operate only when the equilibrium is stable."
をLTL論理式で記述し、SMV で検証を行った。
結果
単純な論理式については真偽値の結果が得られた。しかし、複雑な論理式では検
査器自体が停止しなかった。特別な不備も見つからなかった。
検証手法 モデル検査
モデル化法 フローチャートの意味に忠実にモデル化した。手動。
使用ツール SMV
スケジュール、
労力、時間など
実労時間はツールの使い方の勉強も含めて3ヶ月ほど
備考

情報源

算譜科学研究速報
(テクニカルレポ-ト)
論文発表
口頭発表 (ポスター発表) Yoshiki Kinoshita, Satoshi Matsuoka, Naoya Nitta and Koichi Takahashi: Model Checking a clause of OIML R 76-1, International Conference on Advanced Mathematical and Computational Tools in Metrology (AMCTM 2003)
知的財産
その他

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