| 研究概要 |
拡張有限状態機械でモデル化される通信プロトコルの安全性検証のための,不変式の記述支援に関し以下の研究を行なった.
(1)不変式の一部の自動導出手法の検討:二つのプロトコル機械の送信したメッセージのすれ違いがないという条件のもとで到達可能な状態に関する積項を順次生成する手続きを与えた.与えた手続きでは,一部人間の検証者との対話的処理を行なう.
(2)不変式の半自動生成システムの試作:前記手法の実現性を確認するため,報告者らが既に開発していた拡張有限状態機械モデルの通信プロトコルの検証システムの一部として,不変式の半自動生成システムを試作した.実現のために記述したプログラムは約6,000行であった.
(3)例プロトコルの検証実験:OSIセションプロトコルのデータ転送フェーズから抽出した例プロトコル(各プロトコル機械の状態数:10,整数値レジスタ数:2)の検証実験を行なった.上記の不変式半自動生成システムは例プロトコルに対し,632個の積項を出力した.それらの積項の和をとることにより得られた論理式が,例プロトコルの不変式であること及び安全でない状態では成立しないことが検証システムにより示された.以上より,例プロトコルの安全性がほぼ自動的に証明された.
|
