Fail-over clusters are utilized as a means to assure high-availability for services which require high reliability. If we need continuous communication during fail-over, it is required to synchronize internal states of a protocol stack of an active system and those of a stand-by system. It's, however, hard to verify the system because the number of machines which operate in parallel increases. In this paper, we have designed and verified some dual redundant communication protocols using the model checker SPIN for the purpose of a verifying synchronization mechanism at its design stage.%高い信頼性を求めるサービスに対して高可用性を確保するためにフェイルオーバークラスタが利用されている．フェイルオーバー時にクラスタと通信相辛が継続した通信を行うためにはプロトコルスタックの内部状態を同期する必要があるが，並行動作するマシンの数が増えるため，検証作業が困難になる問題がある．そこで，本研究ではクラスタの同期機構を設計段階で検証するために，SPINによるモデル検査を利用して通信プロトコルニ重化の設計と検証を行った．
展开▼
