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