拡張有限状態モデルの通信プロトコルの検証における不変式の記述支援

1995 Fiscal Year Annual Research Report

• Project/Area Number: 07750422
• Research Institution: Osaka University
• Principal Investigator: 樋口 昌宏 大阪大学, 基礎工学部, 講師 (00238289)
• Keywords: 通信プロトコル / 論理検証 / 安全性 / 不変式 / 整数値レジスタ / 非有界FIFO

Research Abstract

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

Research Products

• [Publications] 原圭吾,佐野順子,樋口昌宏,藤井護: "ECFSMモデルの通信プロトコル検証のための不変式の自動生成システムの開発" 情報処理学会第51回全国大会講演論文集. 1. 89-90 (1995)
• [Publications] M.Higuchi,J.Sano,K.Hara,M.Fujii: "A Semi-automated Verification Methed for Communication Prctocols Modeled as 2-ECFSMS" Proc of 16th Int′l Conference on Distributed Computing Systems. (未定). (1996)