リージョングラフを用いた時間オートマトンのシンボリックモデルチェッキング検証
スポンサーリンク
概要
- 論文の詳細を見る
実時間システムの形式的検証は重要な研究テーマである.しかし,従来の検証手法では,検証コストが大きいために実用化が困難である.本論文では,時間オートマトンで仕様記述して実時間時相論理で検証仕様記述した場合に,検証コストを削減する手法を以下のように提案する.(1)時間オートマトンから時間Kripke構造を生成して,時間Kripke構造からリージョングラフを生成する.(2)仕様と検証仕様を二分決定グラフ(BDD)にエンコードして,シンボリックモデルチェッキング手法により形式的検証を実現する.検証システムを実現して計算機実験により,状態空間の組み合わせ爆発を抑制できることが確認できた.
- 一般社団法人電子情報通信学会の論文
- 1996-06-11
著者
関連論文
- 実時間システムのための近似手法に基づいた記号モデル検査器の開発と評価
- 無限列時間付きステートチャートによる並行システムの仕様記述と検証の手法
- BDDによるSpeed-Independent回路の形式的検証
- ハードリアルタイムシステムの実時間記号モデル検査
- 実時間分散ソフトウェアの可能性と公平性の検証
- 拡張リアルタイム時相論理による分散ソフトウェアの形式的検証
- 分散ソフトウェアのタイミング検証
- 対称性に基づく並行システムの記号モデル検査
- 二分決定グラフによる実時間システムのモデルチェッキング検証
- 二分決定グラフと時間不等式手法に基づく近似解法による実時間シンボリックモデルチェッキング検証
- リージョングラフを用いた時間オートマトンのシンボリックモデルチェッキング検証