| 研究概要 |
今年度の研究の目的は,隠蔽代数を用いて分散システムの動的な性質と静的な構造を一括して定義することにより,システムの仕様を曖昧さなく記述し,同時に、その正しさを自動的に検証するための手法を確立することであった。まず仕様記述法に関しては,通信プロコトル,キャッシュ整合性プロトコル,相互排除アルゴリズム等の典型的な分散システムを例として取り上げ,システムの構成をデータ型を用いて抽象的に定義した上で,システムの振舞を記述することにより,直截で簡潔な形式仕様を得ることができることを示した。このことは検証の自動化を達成するためにも不可欠なことであったが,同時に,単なる形式系の定義に留まらない方法論の蓄積につながった点は,今後の応用に向けて重要な成果であった。仕様の正当性の自動検証については,隠蔽代数に基づいて記述された分散システムの振舞仕様を(無限)状態遷移機械の定義とみなし,システムの状態を隠蔽ソート上の述語として表現することで,モデル検査を不動点の繰り返し計算として自動化する方法を提案した。遷移述語間の包含関係を逐一検査していくことでモデル検査が自動化できるので,無限状態システムを有限状態システムに抽象化する必要がないという点がこの手法の大きな特徴である。本研究では本手法の有効性を確認するため,前述の述語間の包含を,等号を含む一階述語論理を対象とした導出法に基づく定理自動証明によって判定する試作システムをCafeOBJ処理系の上に作成した。結果として,前述の仕様記述例についての正当性が,数秒から数分で完全に自動検証された。このように,無限の状態やデータ型を持つ分散システム仕様の正当性をユーザの介入なしに自動的に検証することができるという点で,本研究の手法の有効性が明らかになった。
|
