動作系列集合による通信プロトコルの代数的仕様から状態遷移機械への変換

点击翻译按钮获取中文摘要

[1]研究の順序を一部変更し,通信プロトコルの検証法についての検討を先に行った.[2]通信ソフトウェアの信頼性を高めるためには,通信プロトコルの正しさを形式的に検証することが望ましい.本研究では互いにデ-タ単位を送受信する二つのプロトコル機械と通信路からなる通信系を検証の対象とし,プロトコル機械を有限状態の順序機械で,プロトコル機械間の通信路を長さに制限のないFIFOキュ-でモデル化した.このようなモデルでは,通信路の有界性が保証されているならば多くの検証の問題は判定可能となる.しかし,この有界性は一般に判定不能であり,実用的プロトコルでは有界性が成り立たない場合も多い.また,仮に有界性が保証されていても,検証時に生成される通信系の合成状態の個数が膨大となり,検証が困難となる.[3]本検証法では与えられたプロトコルПにおける検証すべき性質を,(a)プロトコル機械の指定された状態成分が指定された値をもつことを表す式と,(b)通信路上のデ-タ単位の系列が指定された正規集合に属することを表す式とを原子式とする命題論理式として簡潔に記述した.また,П上の論理式F,Gと正整数kに対して,(F,G,k)ーeventuality(Fを満たす任意の合成状態からどのような遷移を行っても高々k回の遷移でGを満たす合成状態に必ず到達するという性質)が判定可能であることを示した.さらに,Пにおいて,次の(1)ー(3)がそれぞれ成り立つための判定可能な十分条件を与えた.(1)与えられた論理式Fが不変式であること,(2)デッドロック状態に到達不能であること,(3)与えられたデ-タ単位の部分集合Σcについて,通信路上に存在するΣcに属するデ-タ単位の総個数が有界であること.[4]検証の効率を向上させるため,プロトコル機械の分解と縮退という二つの技法を導入した.[5]本検証法をOSIセションプロトコルへ適用し,その有効性を確かめた.