システムレベル設計におけるコンポーネント間プロトコルの形式的検証法

系统级设计中组件间协议的形式化验证

• 批准号: 12780221
• 负责人: 北嶋 暁
• 金额: $ 0.96万
• 依托单位: Osaka Electro-Communication University (2001)Osaka University (2000)
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for Encouragement of Young Scientists (A)
• 财政年份: 2000
• 资助国家: 日本
• 起止时间: 2000 至 2001
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/en/grant/KAKENHI-PROJECT-12780221/
• 关键词: システムレベル検証; インタフェース仕様; 形式的検証; コンポーネント間プロトコル

本年度は,まず,昨年度の検討結果をまとめ,二つのモジュール間のプロトコルの正しさを形式的に検証するアルゴリズムを考案した.具体的には,二つのモジュール間のプロトコルについて,インタフェース記述方法と,その記述のもとでの,インタフェースが正しいことの十分条件およびその検証手法を考案し,簡単な例題に対して,提案手法の有効性を確認した.次に,モジュールの数が三つ以上からなる場合の検証法について検討し,検証アルゴリズムを考案した.提案手法では,インタフェース仕様として各モジュールの機能を明確に分けて定義し,さらに機能の優先度や並列可能な機能の情報を用いることにより,モジュール間のプロトコルが正しいことを比較的容易に示すことができる.一般には三つ以上のモジュールからなる場合のプロトコルの正しさの検証は,起こり得る組み合わせの数が膨大となり,検証が困難であるが,提案手法では,帰納的な議論が可能なプロトコルのクラスを定め,検証においては,プロトコルの正しさを保証するための十分条件を確かめることにより,検証を容易にすることができる.また,簡単な例題に対して,本手法の有効性を確認した.最後に,検証系をはじめとするシステムの作成の際に必要となるインタフェース仕様記述言語を定めた.提案手法は,本言語に含まれるモデルの上で議論されているため,提案アルゴリズムを実装することにより,検証の自動化が可能となる.これにより,検証の自動化の見通しを得た.

This year, the results of the previous year's review were reviewed, and the results of the second review were reviewed. Specifically, the description method of the two sets of information between the two sets of information, the description method, the description method, the description method, In addition, the number of detection groups is more than three times, and the number of detection groups is more than three. The proposed method is to clearly define the functions of each group, prioritize the functions, and use the information of the possible functions. In general, the number of combinations obtained is increased, the verification is difficult, the proposal method is changed, the discussion of inclusion is possible, the verification is changed, the verification is guaranteed, the verification is accurate, and the verification is easy. The effectiveness of this method is confirmed by simple examples. Finally, the identification system is necessary for the creation of the system. The proposal method is that this language contains the following comments: This is the first time that we've seen this.