拡張リアルタイム時相論理による分散ソフトウェアの形式的検証
スポンサーリンク
概要
- 論文の詳細を見る
分散ソフトウェアは,多くのプロセスが並行動作してタイミング制約が厳しく,動作が正しいタイミングで行われるかどうかが非常に重要である.本稿では,リアルタイム時相論理の表現力を向上させた拡張TCTL(Timed CTL)を提案して,効率的なモデルチェッキング手法を提案する.本手法の主要な特徴は以下のとおりである.(1)稠密時間モデルかつ分岐時相論理においてfreeze quantificationとbounded temporal operatorの融合により,簡潔で表現力の高いタイミング制約表現が可能となる.(2)モデルチェッキングは不等式手法とラベリング手法の融合により実現する.
- 一般社団法人情報処理学会の論文
- 1995-07-13
著者
関連論文
- 無限列時間付きステートチャートによる並行システムの仕様記述と検証の手法
- BDDによるSpeed-Independent回路の形式的検証
- ハードリアルタイムシステムの実時間記号モデル検査
- 実時間分散ソフトウェアの可能性と公平性の検証
- 拡張リアルタイム時相論理による分散ソフトウェアの形式的検証
- 分散ソフトウェアのタイミング検証
- 対称性に基づく並行システムの記号モデル検査
- 二分決定グラフと時間不等式手法に基づく近似解法による実時間シンボリックモデルチェッキング検証
- リージョングラフを用いた時間オートマトンのシンボリックモデルチェッキング検証