分散アルゴリズムのCCSによる記述と形式的検証 --- ネットワークグラフ同定問題を例として

鍵本 聡 (9751028)

具体的にはTableau Proofと呼ばれる手法を用いる． この手法の主な手順は次の通りである．

まずプロセス代数を使って分散システムの仕様を記述．
仕様が満たすべき性質を様相μ計算などで記述．
プロセス代数式と様相μ計算式を横に並べた式を推論規則を 用いて書き換えていくことにより検証を進める．

しかし，例えばアルゴリズムの入力(ネットワークの形状)に応じて プロセス式の定義が変化するような場合， Tableau Proofを正当性の検証に直接適用するのは困難である． このような理由から，通常分散アルゴリズムの正当性の検証は 人手で行なわれる．

本研究では「ネットワークグラフ同定問題」を例にとり，それを解く 分散 アルゴリズムをCCSを用いて記述し，その正当性を帰納法とTableau Proofを 組み合わせて形式的かつより機械的に検証する手法について考察する． このことによりすべての状態を見落とさずに確実に検証でき， 分散アルゴリズムの正当性検証問題への自動化検証法の適用範囲が 広がったと言える．