通信プロトコルの検証法の検討とその検証支援システムの製作

1991 Fiscal Year Annual Research Report

• Project/Area Number: 03650303
• Research Institution: Osaka University
• Principal Investigator: 藤井 護 大阪大学, 教養部, 教授 (00029464)
• Co-Investigator(Kenkyū-buntansha): 関 浩之 大阪大学, 基礎工学部, 講師 (80196948)
• Keywords: 通信プロトコルの検証 / プロトコル機械 / 拡張有限状態機械 / 不変式 / プロトコルの安全性 / OSIセションプロトコル

Research Abstract

通信プロトコルの正しさを形式的に検証する問題は,通信ソフトウェアの信頼性を高めるためにも重要である.この種の検証を可能にするための形式記述技法(FDT)には,順序機械を用いてプロトコル機械をモデル化する方法,複数プロセスの可能な動作系列を記述する方法(LOTOS),時間論理,ペトリネットを用いる方法等があるが,有限状態の順序機械モデルによる記述・検証法は,モデルが単純であることからよく研究されてきた.しかし,有限状態モデルは実用的なプロトコルの記述は十分でない,意味検証の自動化のための検証法についてあまり検討がなされていない等の問題点があった.また,この種の問題では,とり得る通信系の全合成状態数が膨大になることから効率のよい検証法を開発することが実用上の課題であった。本研究では,
1.レジスタ(とり得る値の集合が可算無限集合であるような状態成分)を含む二つのプロトコル機械と長さに制限のないFIFOキュ-でモデル化された通信路からなる通信系を対象し,そのプロトコルが満たすべき性質の検証法について考察した.また,
2.この方法に基づく検証を支援し,検証作業を一部自動化するためのシステムの開発を行い,さらに,
3.OSIセションプロトコルについて,安全性が成り立つことをこの方法を用いて消検し,
4.具体例において検証に要した計算時間,検証条件の記述のし易さ等の観点から,本検証法の有効性を確かめた.

Research Products

• [Publications] 邵 峰晶: "順序機械によってモデル化された通信プロトコルの一検証法ーOSIセションプロトコルを例にしてー" 電子情報通信学会論文誌. J74ーDー1. 846-857 (1991)
• [Publications] Masahiro Higuchi: "A Verification Procedure via Invariant for Extended Communicating FiniteーState Machines" Submitted to Fourth Workshop on ComputerーAided Verification.
• [Publications] 樋口 昌宏: "優先サ-ビスを含む通信プロトコルの可達性解析について" 電子情報通信学会技術研究報告. IN91ー108. (1991)
• [Publications] 白川 理: "拡張有限状態機械でモデル化された通信プロトコルの一検証法とそれに基づく検証システム" 情報処理学会研究報告. SEー82ー12. (1991)
• [Publications] 玉井 順子: "優先サ-ビスを含む通信プロトコルの安全性の検証" 情報処理学会第44回全国大会. 7Lー5. (1992)