权益分类	功能权益	普通用户	{{item.name}}会员
{{category.name}}	{{benefitItem.name}}

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

研究通信协议验证方法并创建验证支持系统

基本信息

批准号：
03650303
负责人：
藤井護
金额：
$ 1.15万
依托单位：
Osaka University
依托单位国家：
日本
项目类别：
Grant-in-Aid for General Scientific Research (C)
财政年份：
1991
资助国家：
日本
起止时间：
1991 至无数据
项目状态：
已结题

项目摘要

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

The problem of communication system integrity is very important. The formal description technique (FDT) for this kind of verification is the sequential mechanical method, the description method of the possible series of actions of the plural machines (LOTOS), the temporal logic method, the selection method, etc. The finite state sequential mechanical method is the description method, and the pure method is the research method. The description of the finite state is very difficult, which means that the problem of automatic verification is very difficult to solve. The problem of obtaining the total synthesis state number of communication systems is discussed. In this paper, the following are discussed: (1) The state component of the infinite set contains two kinds of mechanical constraints and FIFO constraints.(2) The communication path is a communication system.(3) The proof method of the properties of the infinite set is investigated. 2. The basic test of this method is supported, and the test operation is carried out in the process of developing the test system automatically. 3. OSI test system is selected, and the safety is established. 4. Specific examples include the calculation time of the test system, the description of the test conditions, etc., and the effectiveness of this test method is verified.