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

• Project/Area Number: 12780221
• Research Category: Grant-in-Aid for Encouragement of Young Scientists (A)
• Allocation Type: Single-year Grants
• Research Field: 計算機科学
• Research Institution: Osaka Electro-Communication University (2001); Osaka University (2000)
• Principal Investigator: 北嶋 暁 大阪電気通信大学, 総合情報学部, 講師 (00304030)
• Project Period (FY): 2000 – 2001
• Project Status: Completed (Fiscal Year 2001)
• Budget Amount: ¥1,500,000 (Direct Cost: ¥1,500,000); Fiscal Year 2001: ¥700,000 (Direct Cost: ¥700,000); Fiscal Year 2000: ¥800,000 (Direct Cost: ¥800,000)
• Keywords: システムレベル検証 / インタフェース仕様 / 形式的検証 / コンポーネント間プロトコル

Research Abstract

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