並行システムの高信頼自動検証ツールに関する研究

2010 年度 研究成果報告書

• 研究課題/領域番号: 20500023
• 研究種目: 基盤研究(C)
• 配分区分: 補助金
• 応募区分: 一般
• 研究分野: 情報学基礎
• 研究機関: 独立行政法人産業技術総合研究所
• 研究代表者: 磯部 祥尚 独立行政法人産業技術総合研究所, 情報技術研究部門, 主任研究員 (50356458)
• 研究期間 (年度): 2008 – 2010
• キーワード: 並行システム / プロセス代数 / 自動解析ツール / 記号処理 / 状態数削減 / 無限状態システム / 定理証明器 / モデル検査器

研究概要

本研究では、並行システムの設計を支援するため、モデル検査器のように自動的に、かつ定理証明器のように記号的にそのシステムの動作を解析するツールの開発を目標として、(1)定理証明器の証明自動化と(2)モデル検査器の記号処理化の二つの側面から研究を行った。前者の(1)については、並行動作の理論CSPに基づく定理証明器CSP-Proverにモデル検査の自動検査アルゴリズムを実装し、証明自動化の可能性を示した。後者の(2)については、並行システムの構造や各プロセスの動作から、そのシステム全体の動作を記号処理によって自動解析する方法を提案し、その方法を解析ツールCONPASUとして実装した。例えばCONPASUは、無限状態の並行システムから、その動作を理解するために有益な記号ラベル付き状態遷移図を自動生成することができる。

研究成果

• [雑誌論文] CONPASU-tool: A Concurrent Process Analysis Support Tool based on Symbolic Computation (2011)
  • 著者名/発表者名: 磯部祥尚
  • 雑誌名: Communicating, Process Architectures 2011(WoTUG-33, IOS Press) (掲載確定) ページ: 22
  • 査読あり
• [雑誌論文] CONPASU-tool : 記号処理に基づく並行プロセス解析支援ツールの試作 (2010)
  • 著者名/発表者名: 磯部祥尚
  • 雑誌名: レクチャーノート/ソフトウェア学 ソフトウェア工学の基礎XVII(近代科学社) 36巻 ページ: 65-74
  • 査読あり
• [雑誌論文] 並行システムを解析するための逐次化と状態削減機能の実装～仕様の自動生成を目指して～ (2010)
  • 著者名/発表者名: 磯部祥尚
  • 雑誌名: 電子情報通信学会技術研究報告CST(コンカレント工学) 110巻89号 ページ: 139-144
• [雑誌論文] The Stable Revivals Model in CSP-Prover (2009)
  • 著者名/発表者名: Gift Samuel, Markus Roggenbach, 磯部祥尚
  • 雑誌名: Electronic Notes in Theoretical Computer Science (ENTCS) Vol.250, No.2 ページ: 119-134
  • 査読あり
• [雑誌論文] CSP-CASL-Prover -- A generic tool for process and data refinement (2009)
  • 著者名/発表者名: Liam O'reilly, Markus Roggenbach, 磯部祥尚
  • 雑誌名: Electronic Notes in Theoretical Computer Science (ENTCS) Vol.250, No.2 ページ: 69-84
  • 査読あり
• [雑誌論文] CSP-Prover -- a Proof Tool for the Verification of Scalable Concurrent Systems (2008)
  • 著者名/発表者名: 磯部祥尚
  • 雑誌名: 日本ソフトウェア科学会コンピュータソフトウェア(JSSST) 25巻4号 ページ: 85-92
  • 査読あり
• [学会発表] CONPASU-tool : A Concurrent Process Analysis Support Tool based on Symbolic Computation (2011)
  • 著者名/発表者名: 磯部祥尚
  • 学会等名: Communicating Process Architectures 2011, (CPA 2011, the 33rd WoTUG conference)
  • 発表場所: リムリック大学(アイルランド)
  • 年月日: 2011-06-21
• [学会発表] CONPASU : CSPモデルの解析支援ツール (2011)
  • 著者名/発表者名: 磯部祥尚
  • 学会等名: 第7回CSP研究会
  • 発表場所: 東洋大学(東京都)
  • 年月日: 2011-05-21
• [学会発表] CONPASU : 記号処理に基づく並行プロセスの状態数削減ツール (2011)
  • 著者名/発表者名: 磯部祥尚
  • 学会等名: 第13回プログラミングおよびプログラミング言語ワークショップ(PPL2011)
  • 発表場所: 定山渓ビューホテル(北海道)
  • 年月日: 2011-03-10
• [学会発表] CONPASU-tool : 記号処理に基づく並行プロセス解析支援ツールの試作 (2010)
  • 著者名/発表者名: 磯部祥尚
  • 学会等名: 第17回ソフトウェア工学の基礎ワークショップ(FOSE2010)
  • 発表場所: いなもと旅館(新潟県)
  • 年月日: 2010-11-19
• [学会発表] 並行システムを解析するための逐次化と状態削減機能の実装 ～仕様の自動生成を目指して～ (2010)
  • 著者名/発表者名: 磯部祥尚
  • 学会等名: 電子情報通信学会コンカレント工学研究会(CST)
  • 発表場所: 北見工業大学(北海道)
  • 年月日: 2010-06-22
• [学会発表] A Prototype Tool for Analyzing Concurrent Processes -- Towards Automatic Generation of Specifications (2010)
  • 著者名/発表者名: 磯部祥尚
  • 学会等名: Workshop on Symbolic Computation and Software Verification
  • 発表場所: 筑波大学(茨城県)
  • 年月日: 2010-04-06
• [学会発表] CSPプロセスの解析支援ツールの試作～仕様の自動生成を目指して～ (2010)
  • 著者名/発表者名: 磯部祥尚
  • 学会等名: 第4回CSP研究会
  • 発表場所: 東洋大学(東京都)
  • 年月日: 2010-03-10
• [学会発表] プロセス代数に基づく並行システムの動作解析のための逐次化ツール (2010)
  • 著者名/発表者名: 磯部祥尚
  • 学会等名: 第12回プログラミングおよびプログラミング言語ワークショップ(PPL2010)
  • 発表場所: 琴参閣(香川県)
  • 年月日: 2010-03-04
• [学会発表] 定理証明器による双模倣等価性の自動証明 (2009)
  • 著者名/発表者名: 磯部祥尚
  • 学会等名: 第11回プログラミングおよびプログラミング言語ワークショップ(PPL2009)
  • 発表場所: 高山グリーンホテル(岐阜)
  • 年月日: 2009-03-10
• [学会発表] The First Step for Implementing a Model Checker in a Theorem Prover -- Toward Automatic Verification in CSP-Prover (2008)
  • 著者名/発表者名: 磯部祥尚
  • 学会等名: Theorem Proving and Provers (TPP2008) Meeting
  • 発表場所: 東北大学電気通信研究所(宮城県)
  • 年月日: 2008-11-26
• [学会発表] The Stable Revivals Model in CSP-Prover (2008)
  • 著者名/発表者名: Gift Samuel, Markus Roggenbach, 磯部祥尚
  • 学会等名: 8th International Workshop on Automated Verification of Critical Systems (AVoCS2008)
  • 発表場所: グラスゴー大学(スコットランド)
  • 年月日: 2008-10-01
• [学会発表] CSP-CASL-Prover -- A generic tool for process and data refinement (2008)
  • 著者名/発表者名: Liam O'reilly, Markus Roggenbach, 磯部祥尚
  • 学会等名: 8th International Workshop on Automated Verification of Critical Systems (AVoCS 2008)
  • 発表場所: グラスゴー大学(スコットランド)
  • 年月日: 2008-09-30
• [備考] CONPASUのホームページ
  • URL: http://staff.aist.go.jp/y-isobe/conpasu
• [備考] CSP-Proverのホームページ
  • URL: http://staff.aist.go.jp/y-isobe/CSP-Prover/CSP-Prover.html