• 研究課題をさがす
  • 研究者をさがす
  • KAKENの使い方
  1. 前のページに戻る

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

研究課題

研究課題/領域番号 12780221
研究種目

奨励研究(A)

配分区分補助金
研究分野 計算機科学
研究機関大阪電気通信大学 (2001)
大阪大学 (2000)

研究代表者

北嶋 暁  大阪電気通信大学, 総合情報学部, 講師 (00304030)

研究期間 (年度) 2000 – 2001
研究課題ステータス 完了 (2001年度)
配分額 *注記
1,500千円 (直接経費: 1,500千円)
2001年度: 700千円 (直接経費: 700千円)
2000年度: 800千円 (直接経費: 800千円)
キーワードシステムレベル検証 / インタフェース仕様 / 形式的検証 / コンポーネント間プロトコル
研究概要

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

報告書

(2件)
  • 2001 実績報告書
  • 2000 実績報告書

URL: 

公開日: 2000-04-01   更新日: 2016-04-21  

サービス概要 検索マニュアル よくある質問 お知らせ 利用規程 科研費による研究の帰属

Powered by NII kakenhi