• Search Research Projects
  • Search Researchers
  • How to Use
  1. Back to previous page

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

Research Project

Project/Area Number 07750422
Research Category

Grant-in-Aid for Encouragement of Young Scientists (A)

Allocation TypeSingle-year Grants
Research Field 情報通信工学
Research InstitutionOsaka University

Principal Investigator

樋口 昌宏  大阪大学, 基礎工学部, 講師 (00238289)

Project Period (FY) 1995
Project Status Completed (Fiscal Year 1995)
Budget Amount *help
¥1,000,000 (Direct Cost: ¥1,000,000)
Fiscal Year 1995: ¥1,000,000 (Direct Cost: ¥1,000,000)
Keywords通信プロトコル / 論理検証 / 安全性 / 不変式 / 整数値レジスタ / 非有界FIFO
Research Abstract

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

Report

(1 results)
  • 1995 Annual Research Report
  • Research Products

    (2 results)

All Other

All Publications (2 results)

  • [Publications] 原圭吾,佐野順子,樋口昌宏,藤井護: "ECFSMモデルの通信プロトコル検証のための不変式の自動生成システムの開発" 情報処理学会第51回全国大会講演論文集. 1. 89-90 (1995)

    • Related Report
      1995 Annual Research Report
  • [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)

    • Related Report
      1995 Annual Research Report

URL: 

Published: 1995-04-01   Modified: 2016-04-21  

Information User Guide FAQ News Terms of Use Attribution of KAKENHI

Powered by NII kakenhi