無限列時間付きステートチャートによる並行システムの仕様記述と検証の手法
スポンサーリンク
概要
- 論文の詳細を見る
タイミング制約記述を含む非同期型並行システムの仕様は時間グラフで表現されることが多い.並行システムの計算機化のアプローチとしては,仕様の制約式からモデル生成する自動生成アプローチと,仕様が性質記述を充足するかどうかを判定する検証アプローチに分類できる.時間厳密性を含む時相論理式から稠密的時間領域な時間グラフを生成するモデル生成アルゴリズムは知られていないが,検証は決定可能である.そこで,我々は,時間グラフを効率的に仕様記述して検証するために,無限列時間付きステートチャートを考案した.その主要な特徴は,(1)時間オートマトンを拡張したステートチャートにより形式的に仕様記述する,(2)ステートチャートの検証問題を形式言語理論の言語包合問題に帰着する,(3)時間グラフのタイミングシミュレーションにより検証コストを削減する,(4)インターフェースルールにより検証性質毎に時間グラフを縮少する,である.
- 1994-09-03
著者
関連論文
- 無限列時間付きステートチャートによる並行システムの仕様記述と検証の手法
- BDDによるSpeed-Independent回路の形式的検証
- ハードリアルタイムシステムの実時間記号モデル検査
- 実時間分散ソフトウェアの可能性と公平性の検証
- 拡張リアルタイム時相論理による分散ソフトウェアの形式的検証
- 分散ソフトウェアのタイミング検証
- 対称性に基づく並行システムの記号モデル検査
- 二分決定グラフと時間不等式手法に基づく近似解法による実時間シンボリックモデルチェッキング検証
- リージョングラフを用いた時間オートマトンのシンボリックモデルチェッキング検証