ハードリアルタイムシステムの実時間記号モデル検査
スポンサーリンク
概要
- 論文の詳細を見る
以下のような特徴を持つ実時間記号モデル検査を開発した. 1. 実時間記号モデル検査のシステムは二分決定グラフによりシンポリンクに表現する. この手法において, 時間オートマトンから時間Kripke構造に変換して検証をおこなう. 2. 実時間システムにおいて, 近似解法を用いることにより検証コストを削減することができる. 3. 近似解法における実時間時相論理式のforwardとbackwardの不動点計算を行う.
- 社団法人電子情報通信学会の論文
- 1999-03-19
著者
関連論文
- 無限列時間付きステートチャートによる並行システムの仕様記述と検証の手法
- BDDによるSpeed-Independent回路の形式的検証
- ソフトウェアプロセスの時間オートマトンおよび時間モジュールによる記述法の比較
- ハードリアルタイムシステムの実時間記号モデル検査
- 実時間分散ソフトウェアの可能性と公平性の検証
- 拡張リアルタイム時相論理による分散ソフトウェアの形式的検証
- 分散ソフトウェアのタイミング検証
- 対称性に基づく並行システムの記号モデル検査
- 二分決定グラフと時間不等式手法に基づく近似解法による実時間シンボリックモデルチェッキング検証
- リージョングラフを用いた時間オートマトンのシンボリックモデルチェッキング検証