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