拡張有限状態機械モデルの通信プロトコルのlivenessの検証法

概要

論文の詳細を見る
著者らは,プロトコル機械が拡張有限状態機械でモデル化され,通信路が非有界FIFOでモデル化された通信プロトコルの安全性の検証法を提案している.本稿では,同様にモデル化され,上記検証法により安全性が保証されているプロトコルのlivenessの検証法を提案する.まず,livenessを初期状態から到達可能な任意の状態からある性質Qを満たす状態に到達可能であるという性質(Q-live性)として定式化する.安全性の検証によりプロトコル∏の初期状態から到達可能な状態集合が部分集合GS_1,GS_2,・・・,GS_nに分割されているとする.このとき,各頂点v_1,v_2,・・・,v_nがそれぞれGS_1,GS_2,・・・,GS_nに対応し,v_iからv_jへの辺があるならば「∀gs ∈ GS_i∃ gs'∈ GS_j{gsからgs'に到達可能}」であるような有向グラフDRG_<∏>を作る.さらに,DRG_<∏>上を探索することにより,∏のQ-live性を示す.OSIセションプロトコルのデータ転送フェーズから抽出したプロトコルのQ-live性の検証を行った結果についても述べる.
一般社団法人情報処理学会の論文
1994-01-20