整備されたネットワークにおいて新たなプロトコルを導入した時，それに誤りがあった場合，その修正に要するコストは多大なものになり得る．本研究は分散相互排除アルゴリズムを仕様記述言語LNTで形式的に記述し，CADP toolboxを用いてモデル検査を行うことでそのような誤りを解消することを目的とする．分散相互排除アルゴリズムの参加ノードの故障モデルに対し，相互排除が正しく行われているかを確かめるため，参加ノード間を接続するネットワークプロセスと並列に共有資源を利用するノードを数えるカウンターを設置することで状態の監視を可能にする．また，ベクトル時計を用いた故障検知の一手法を提案する．