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

1999 Fiscal Year Annual Research Report

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

Research Abstract

研究開始から現在までに,分散システムの仕様記述言語と検証に関する理論が以下のように開発できた.
1.まず,分散システムの並行性やタイミング制約,機能の統合的な仕様記述を実現する時間ステートチャートを提案した.時間ステートチャートのタイミング制約と機能により,時間ステートチャートは無限な状態遷移システムであり,分散システムの汎用的な計算モデルに相当する.
2.次に,時間ステートチャートからPnueliらのクロック遷移システムに変換することにより,時間ステートチャートの操作的意味を定義した.この操作的意味により,時間ステートチャートのイベントによる動作と時間経過が形式化できた.
3.次に,クロック遷移システム上の演繹的証明により,時間ステートチャートが安全性や活性を充足することが検証できた.一般的に,分散システムは無限な状態遷移システムを構成するので,演繹的検証手法のみによって検証可能である.
4.最後に,クロック遷移システム上で詳細化検証の公理系を開発して,時間ステートチャートの詳細化の検証が実現できた.
現在,以下の検討項目を研究中である.
1.開放型分散システムの仕様記述を可能にするために,時間ステートチャートを拡張する.
2.時間ステートチャートのAssume-Guarantee style検証を実現する.
3.時間ステートチャートを有限化して,自動演繹的検証を実現する.

Research Products

• [Publications] 山根 智: "時間ステートチャートによる仕様記述と演繹的検証"電子情報通信学会技術研究報告(SS). 99・547. 33-40 (2000)
• [Publications] 山根 智,山ノ口崇: "時間ステートチャートの演繹的検証と自動演繹検証"情報処理学会九州支部研究会. 10. 150-157 (2000)