プロダクションシステムを用いた通信ソフトウェア仕様の可到達解析に関する考察
スポンサーリンク
概要
- 論文の詳細を見る
通信ソフトウェア仕様の重要な検証項目の一つとして,状態の可到達性解析,即ち,特定の状態が,ある仕様によって与えられたシステムに出現するか否かの検査がある.本稿では,書き換え型のプロダクションシステムによって定義された通信ソフトウェア仕様の可到達集合についてその基本的な性質を考察する.可到達状態を複数のプロセスによって構成される到達可能な準広域状態として定義したとき,可到達状態集合の大きさは,初期状態として与えるプロセス数を増やすと単調増加することが予想される.このため可到達性を一般に保証するには,プロセス数を無限と仮定した解析を行なう必要がある.本論文では,システムを構成するプロセス数と可到達集合の大きさの関係を明らかにし,最大の可到達集合を得るのに必要な最小のプロセス数を求める方法を示した.これによって,無限プロセスの存在を仮定するシステムの可到達性を有限プロセスのそれに置き替えて議論することが可能になった.
- 社団法人電子情報通信学会の論文
- 1994-01-14
著者
関連論文
- ヒューリスティックなカットセット解析によるPSDLコンパイラの処理ネック解決
- 概念モデル上のカーディナリティに着目した仕様の洗練化
- E-Rモデルと制約に基づく仕様部品の合成と制約論理プログラムへの変換
- E-R モデルを用いた視覚的プログラミング言語 : PSDL-GR とその一実現法
- 広域状態遷移規則を用いた通信サービス仕様記述における可到達解析
- 通信システム仕様の高速検証方式
- 通信ソフトウェア仕様の検証に関する課題
- 広域状態遷移ルールの述語的解釈による可到達判定
- プロダクションシステムを用いた通信ソフトウェア仕様の可到達解析に関する考察
- 概念データモデルで記述された仕様の関数型言語への変換