線形時相論理の為の効率的記号モデル検査方式
スポンサーリンク
概要
- 論文の詳細を見る
設計されたシステムが与えられた仕様どおりに動作するかどうかを確かめる設計検証はシステムの大規模化,複雑化により重要な役割を担うようになっている.一方,検証対象システムが大きくなると検証に要なる計算量が急激に増加するという,いわゆる状態爆発という問題がある.この問題を解決する一つの方法として二分決定木(Binary Desicion Diagram)を利用した論理関数処理に基づく記号モデル検査法が提案されている.本報告では,システムがペトリネットによって記述され,検証すべき性質が線形時相論理(Liner-time Temporal Logic)で表されている場合に,記号モデル検査法を効率的に行う方法を提案する.
- 1993-10-28
著者
関連論文
- 多値非同期式回路の形式的検証に関する研究
- プロセス代数に基づく非同期式論理回路の設計検証 (非同期式回路/システム設計論文小特集)
- 非同期式回路の検証におけるIivenessクラスに関する考察
- 非同期式回路の検証におけるlivenessクラスに関する考察
- ハードウェアによるZBDD処理の実現に関する研究
- ハードウェアによるZBDD処理の実現に関する研究
- ハードウェアによるZBDD処理の実現に関する研究
- Net Unfoldingによるタイムペトリネットの効率的解析
- 有限遅延幅モデルにおける非同期式回路の検証について (テストと設計検証論文特集)
- 時間トレース理論に基づく非同期式回路の検証について
- Failure trace解析に基づくGasP回路の形式的検証
- 星状抽象ペトリネットの解析に関する研究
- 星状抽象ペトリネットの解析に関する研究
- 星状抽象ペトリネットの解析に関する研究
- ZBDDとpartial order reductionに基づく非同期式回路検証方式について
- ゼロサプレスBDDによるペトリネットのCTL記号モデル検査
- 非同期式回路検証のためのレベル指向モデルとその効率的解析法について
- 非同期式回路検証のためのレベル指向モデルとその効率的解析法について
- データパスを含む非同期式回路の検証について
- ZBDDに基づく非同期式回路の検証方式
- ZBDDを用いた検証方式におけるpartial order reductionの適用について
- 高速タイミング検証方式の実現とその効率評価
- ZBDDに基づく非同期回路の検証方式
- 非同期式回路検証器における使用記憶域削減について
- 非同期式回路検証器における使用記憶域削減について
- 非同期式回路検証器における使用記憶域削減について
- Self-Timed Implementation of Boolean Functions
- Self-Timed Implementation of Boolean Functions
- Self-Timed Implementation of Boolean Functions
- Implementing Fast Boolean QDI Function Blocks
- Implementing Fast Boolean QDI Function Blocks
- Implementing Fast Boolean QDI Function Blocks
- Self-Timed Implementation of Boolean Functions
- Self-Timed Implementation of Boolean Functions
- Self-Timed Implementation of Boolean Functions
- n 安全タイムペトリネットの発火規則について
- n安全タイムペトリネットの発火規則について
- ステートチャートのシンボリックな検証方式について
- シミュレーションを利用した形式的検証システム
- シミュレーションを利用した形式的検証システム
- 論理シミュレーションに基づくプロセッサの自動検証
- タイムペトリネットにおけるCTL記号モデル検査法について
- タイムペトリネットにおけるCTL記号モデル検査法について
- 線形時相論理の為の効率的記号モデル検査方式
- 線形時相論理の為の効率的記号モデル検査方式
- 連立不等式に基づくタイムペトリネットのCTLモデル検査
- タイムペトリネットの拡張とスケジューラビリティーの検証への応用
- 対称性及び抽象化を利用した検証方式の効率化 (テストと設計検証論文特集)
- 正規表現を利用したスケーラブル環状回路の検証
- 正規表現を利用したスケーラブル環状回路の検証
- 対称性及び抽象化を利用した検証方式の効率化
- 有限幅遅延モデルに基づく非同期式回路検証方式とその効率化(ペトリネットの応用特集号)