時相論理と並行計算、オートマトンの統合化による自律性のある分散システムの設計支援

2000 Fiscal Year Annual Research Report

• Project/Area Number: 11680360
• Research Institution: Kagoshima University
• Principal Investigator: 山根 智 鹿児島大学, 工学部, 助教授 (70263506)
• Keywords: 分散システム / 時相論理 / 演繹的検証 / リアルタイム性 / 詳細化検証 / Assume-Guarantee / receptive

Research Abstract

平成12年度では、前年度の成果の上に、以下のような成果を得た:
1.有限状態モデルにおいて、以下の提案及び開発を行った。
(1)分散システムを仕様記述可能とした拡張時間オートマトンを開発して、拡張時間オートマトンのAssume-Gurantee形式による自動詳細化検証手法を提案した。ここでの詳細化関係は、Milnerが提案した模倣関係を実時間制約で拡張した時間模倣関係である。
(2)拡張時間オートマトンで仕様記述した分散プロセスが物理的に実装可能であることを保証する条件、いわゆるreceptivenessの自動検証手法を実現した。Receptivenessは、環境と分散プロセスとの無限ゲームで形式化できる。
(3)自動詳細化検証器の実装を行って、計算機実験により、提案手法の有効性を示した。
2.無限状態モデルにおいて、時間ステートチャートのAssume-Gurantee形式による演繹的詳細化検証手法を開発した。さらに、receptivenessの演繹的検証手法を実現した。
現在、以下の検討項目を研究中である:
1.時間ステートチャートのAssume-Gurantee形式による演繹的詳細化検証手法の実装及び実問題への適用。
2.分散システムのより高度なモデル化として、ハイブリッドオートマトンへの拡張。

Research Products

• [Publications] 山根智,山ノ口崇: "実時間システムの演繹的検証と自動演繹的検証"情報処理学会研究報告MPS2000. 2000・29. 5-8 (2000)
• [Publications] 山根智,山ノ口崇: "実時間システムの演繹的検証"電子情報通信学会研究報告SS2000. 2000・6. 1-8 (2000)
• [Publications] 山根智,山ノ口崇: "AND構造とOR構造の分解による実時間ソフトウェアの安全性の演繹的検証"レクチャーノート(近代科学社). 25. 237-248 (2000)
• [Publications] 山根智: "Assume-Gurantee検証による実時間システムの階層的設計支援手法"情報処理学会論文誌. 41・12. 3352-3362 (2000)
• [Publications] 山根智,山ノ口崇: "Assume-Guarantee形式による実時間ソフトウェアの演繹的詳細化検証手法"電子情報通信学会研究報告SS2000. 2000・31. 1-8 (2001)