拡張有限状態機械でモデル化された通信プロトコルの生存性の検証法

概要

論文の詳細を見る
プロトコル機械が拡張有限状態機械でモデル化され,通信路が非有界FIFOでモデル化された通信プロトコルの生存性の検証法を提案する.生存性は初期状態から到達可能な任意の状態から興味のある性質Qを満たす状態に到達可能であるという性質(Q-live性)として定式化する.性質Qはプロトコル機械の状態および通信路上のメッセージ系列に関する条件を表す4種類の原子論理式を用いて指定する.それらの原子論理式を用いて,人間の検証者が初期状態から到達可能な状態の集合を部分集合RS_1,RS_2,...,RS_nに分割する.このとき,各頂点v_i(1≦i≦n)がRS_iに対応し,「∀gs∈RS_i∃gs′∈RS_j{gsからgs′に到達可能である}」ときに限りv_iからv_jへの辺があるようなグラフを縮退到達可能性グラフと呼ぶ.本論文では,与えられたRS_1,RS_2,...,RS_nに対して縮退到達可能性グラフを構成し,それを探索することによるQ-live性の検証法を提案する.また,提案する検証法に基づいて試作した検証システム,およびOSIセションプロトコルの一部を抽出したプロトコルのQ-live性の検証を行った結果についても述べる.
社団法人電子情報通信学会の論文
1995-01-25