著者

吉岡 信和 田辺 良則 田原 康之 長谷川 哲夫 磯部 祥尚

出版者

日本ソフトウェア科学会

雑誌

コンピュータ ソフトウェア (ISSN:02896540)

巻号頁・発行日

vol.31, no.4, pp.4_40-4_65, 2014-10-24 (Released:2014-12-24)

---

機器の高速化やネットワークの発展に伴い,多数の機器やコンポーネントを連携させ,高度な機能を提供する並行分散システムが一般的になってきている.そのようなシステムでは,振舞いの可能性が膨大であり,従来のレビューやシミュレーションで設計の振舞いの正しさを保証することは困難である.それに対して,網羅的にかつ自動的に振舞いに関する性質を調べるモデル検査技術が注目されている.本稿では,モデル検査技術の背景と5つの代表的なモデル検査ツールを紹介し,その応用事例や最新の研究動向を解説する.

著者

磯部 祥尚 ローゲンバッハ マーカス

出版者

日本ソフトウェア科学会

雑誌

コンピュータ ソフトウェア (ISSN:02896540)

巻号頁・発行日

vol.25, no.4, pp.85-92, 2008

著者

磯部 祥尚 ローゲンバッハ マーカス Markus Roggenbach 産業技術総合研究所:マーカス・ローゲンバッハ スウォンジー大学 産業技術総合研究所:マーカス・ローゲンバッハ スウォンジー大学 National Institute of Advanced Industrial Science and Technology:Swansea University National Institute of Advanced Industrial Science and Technology:Swansea University

出版者

日本ソフトウェア科学会

雑誌

コンピュータソフトウェア = Computer software (ISSN:02896540)

巻号頁・発行日

vol.25, no.4, pp.85-92, 2008-10-28

参考文献数

17

著者

磯部 祥尚

出版者

独立行政法人産業技術総合研究所

雑誌

基盤研究(C)

巻号頁・発行日

2008

---

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