モデル検査を用いた通信プロトコル二重化の検証

摘要

高い信頼性を求めるサービスに対して高可用性を確保するために，フェイルオーバクラスタが利用rnされている．このようなシステムでは，フェイルオーバ時にクラスタと通信相手が継続した通信を行うために，プロトコルスタックの内部状態を同期する必要がある．しかし，並行動作するマシンの数が増えると，同期機構の検証作業が困難になるという問題が生じる．そこで，本論文ではクラスタの同期機構を設計段階で検証するため，モデル検査を利用した通信プロトコル二重化の検証手法を提案する．提案手法では，モデル検査を用いることにより，設計段階における不具合の早期発見が可能である．加えて，単体システムのモデルとその形式仕様をクラスタの検証に活用することにより，通信プロトコル二重化の検証を汎用的な手順で行うことができる．提案手法をTCPの二重化に対して適用し，提案手法の有効性を確認した．