1990 Fiscal Year Annual Research Report
動作系列集合による通信プロトコルの代数的仕様から状態遷移機械への変換
| Project/Area Number |
02650267
|
|---|
| Research Institution | Osaka University |
|---|
Principal Investigator |
藤井 護 大阪大学, 教養部, 教授 (00029464)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
関 浩之 大阪大学, 基礎工学部, 講師 (80196948)
伊藤 実 大阪大学, 基礎工学部, 助教授 (90127184)
|
|---|
| Keywords | 通信プロトコルの検証 / プロトコル機械 / 有限状態の順序機械 / 不変式 / Eventuality / (プロトコル機械の)分解,縮退 / OSIセションプロトコル |
|---|
| Research Abstract |
[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セションプロトコルへ適用し,その有効性を確かめた.
|
-
[Publications] 邵 蜂晶: "順序機械によってモデル化された通信プロトコルの一検証法ーOSIセションプロトコルを例にしてー" 電子情報通信学会技術研究報告. IN90ー52. (1990)
-
[Publications] 白川 理: "順序機械によってモデル化された通信プロトコルの検証システム" 電子情報通信学会全国大会. B-495 (1990)
-
[Publications] F.Shao: "A Verification System for Communication Protocols and lts Application to the OSI Session Protocol" Proc.Joint Conference on Communications,Networks,Switching Systems and Ssatellite Communications. 110-114 (1990)
-
[Publications] 邵 蜂晶: "順序機械によってモデル化された通信プロトコルの一検証法" 電子情報通信学会論文誌(DーI).
-
[Publications] F.Shao: "Protocol Verification via Decomposition and Degeneration and its Verification Example" 15th Annual International Computer Software and Applications Conference.
