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

池田　聡  地引　昌弘  久野　靖  西森　丈俊  

誌名
電子情報通信学会論文誌 D   Vol.J93-D   No.7   pp.1154-1164
発行日: 2010/07/01
Online ISSN: 1881-0225
DOI: 
Print ISSN: 1880-4535
論文種別: 特集論文 (インターネット技術とその応用論文特集)
専門分野: プロトコル
キーワード: 
モデル検査,  通信プロトコル,  冗長化,  

本文: PDF(320.3KB)
>>論文を購入

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