CVS

center-name

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

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

Web版 トップ頁へ

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

  2. 概要一覧

▼ 話題別に探す
  1. 領域

  2. 形態

  3. 手法

  4. ツール

  5. 実施年度

事例 6: 遷移系抽象化アルゴリズムの検証


実施年度2003
概要 Lee-Yannakakisによる遷移系の分割縮小化アルゴリズムを形式化し、アルゴリ ズムの正当性と停止性の二つの性質を定理証明支援系PVSを用いて証明した。
担当者 高木理、武山誠、渡邊宏
班名
寄与 文科省科振費
関連する事例

題材

領域 アルゴリズム
題材の詳細
LeeとYannkakisによって与えられた遷移系の抽象化アルゴリズム。

Lee, D. and Yannakakis, M.: On-line Minimization of Transition
Sysmtems, in Proc. 24th Anuual ACM Symposium on Theory of Computing,
May 1992. pp. 264-274.
形態 擬似コード
言語 英語
規模 数ページ
題材の情報源 論文 Lee, D. and Yannakakis, M.: On-line Minimization of Transition Sysmtems, in Proc. 24th Anuual ACM Symposium on Theory of Computing, May 1992. pp. 264-274.

検証のデータ

目的
対話型検証事例を作る
検証内容
二つの性質を検証した。
アルゴリズムの正当性:出力される計算結果が正しい。
アルゴリズムの停止性:アルゴリズムは必ず停止する。
結果
正当性、停止性とも証明できた。停止性の証明では特殊な整礎集合を構成して、
証明の手間を省いた。
検証手法 定理証明・対話型検証
モデル化法 手動
使用ツール PVS
スケジュール、
労力、時間など
2ヶ月程度
備考

情報源

算譜科学研究速報
(テクニカルレポ-ト)
PS-2005-006, Verification of Transition System Reduction via PVS, O. Takaki, M. Takeyama, H. Watanabe, http://unit.aist.go.jp/cvs/tr-data/ps05-006.pdf
論文発表 Verification of Transition System Reduction via PVS, 高木 理(京都産業大学)、武山 誠、渡邊 宏, コンピュータソフトウェア,22-3,pp.134-145、2005/07
口頭発表 Kripke構造の模倣性に関する基本的性質および縮小化・抽象化に対する証明支 援系による形式化, 高木 理、武山 誠、渡邊 宏, システム検証の科学技術,梅田スカイビル、2004/02/05
知的財産
その他

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