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