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

2000 Fiscal Year Annual Research Report

• Project/Area Number: 12780221
• Research Institution: Osaka University
• Principal Investigator: 北嶋 暁 大阪大学, 大学院・基礎工学研究科, 助手 (00304030)
• Keywords: システムレベル検証 / インタフェース仕様 / 形式的検証 / コンポーネント間プロトコル

Research Abstract

本年度は,まず,本研究で対象とするコンポーネント間のプロトコルのクラスについての検討を行った.コンポーネントのインタフェース仕様記述として,正規表現を用いる方法が提案されており,本研究でも同様のクラスについて検証を行うことを検討した.正規表現を用いてインタフェース仕様を記述することでコンポーネントの動作が抽象化されるため,形式的な検証が容易になる.
次に,検証内容とその方法について検討を行った.本研究では,二つのモジュール間のプロトコルを対象とする.この場合,重要な点は,いかなる場合でもプロトコルの不整合によるデッドロックが起こらないことである.検証方法としては,インタフェース仕様記述において,2者間のプロトコルでデッドロックが起こらないことを検証し,また,各モジュールについてインタフェース仕様を満たしていることを独立に調べるという方法を採ることにした.このようにすることで検証の切り分けができ,各検証時間を短くすることが可能である.
現在,検証アルゴリズムを考案し,検証システムを構築しつつ,例題を作成し,本手法の有効性の確認を行っている.
来年度は,現在行っている実験結果をまとめ,更に,三つ以上のモジュールを組み合わせた場合に対する検証方法について検討を行う予定である.