| 研究概要 |
ネットワークに接続されたコンピュータや端末の間で, 確実に通信を行うための一連の取り決めをプロトコル(通信規約)と呼ぶ. ネットワークを確実に運用するためには, プロトコルを厳密に定め, ネットワークの構成要素がすべてそのプロトコルに従って動作していることを確認する必要がある. このためにネットワークに接続される機器(プロトコル製品と呼ぶ)をネットワークに接続する場合には, 必ず所定のプロトコルとの整合性の検証を行う. これを適合性試験もしくは製品検証と呼ぶ.
プロトコルの製品検証においては, プロトコルをいかに記述し, それにもとずいてテスト手順をどのように決めるかが問題である. プロトコルは従来から自然言語を用いて記述されて来たが, あいまいさがあり, 製品検証に適していない.
本研究においてはまずプロトコルを系統的に機械可続な方法で表現するイベント順序記述方式を定式化した. これは理論的には時相論理にもとずくものであり, プロトコルを構造に関する記述と動作に関する記述に分けて表現する. 次にこの表現を有限オートマトンの理論によって状態遷移表に変換する方式を提案した. 状態遷移表からテストシーケンスを生成する方法はすでに研究者等によって明らかにされており, これによってプロトコルの形式表現からテストシーケンス発生に到る一貫した手法が得られたことになる.
この方法は簡単なデータリング層のプロトコル, HDLCちらにはトラシスポート層のプロトコルに適応する実験を通して, 充分実用的であると考えられる. なおイベント順序記述, 状態遷移表表現は国際標準LOTOS, ESTELLEに対応しており, この間の変換も本方式の拡張によって可能になることが明らかにされた. この際のLOTOS表現には追加の情報が必要になる.
|
