|
分散スナップショットアルゴリズム（DSA）を書換え論理に基づく計算機言語Maudeのメタプログラム（MP）として記述する方法と分散スナップショット到達可能性（DSR）を直接モデル検査する方法を考案し、実験により有効性を確認した。従来法では、分散システム（DS）ごとにDSAも含め毎回記述する必要があったのに対し、提案方法では、MPを１回記述しさえすれば、DSのみの記述で十分であるという利点がある。また、DSRを直接モデル検査可能になったため、より高速にモデル検査可能になり、性質を満たさない場合反例を提示できるようにもなった。提案方法は、DSを計算の対象とする分散アルゴリズムに適用可能である。
|
