ステートチャートのシンボリックな検証方式について
スポンサーリンク
概要
- 論文の詳細を見る
ステートチャートはグラフィカルなモデル化手法の一つで,商用のものも含めいろいろなツールが開発されている.しかし,その多くのは非常に簡単な意味モデルを用いているため,ステートチャートの記述が複雑になったり,状態遷移条件に否定イベントを含むステートチャートの振る舞いが曖昧になるという問題が生じている.そこで本稿では,まずステートチャートのより厳密な意味モデルを提案する.この意味モデルでは,一つの外部イベントに対するステートチャートの一動作(マクロステップ)をいくつかの状態遷移(マイクロステップ)の列で定義し,論理プログラミングにおけるnegation as failureの手法を用いて否定イベントを取り扱う.次に,その意味モデルを2分決定グラフ(BDD)を用いてシンボリックに解析する方法を示し,簡単な例において実験結果を示す.
- 社団法人電子情報通信学会の論文
- 1995-08-23
著者
関連論文
- 多値非同期式回路の形式的検証に関する研究
- プロセス代数に基づく非同期式論理回路の設計検証 (非同期式回路/システム設計論文小特集)
- 非同期式回路の検証における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モデル検査
- タイムペトリネットの拡張とスケジューラビリティーの検証への応用
- 対称性及び抽象化を利用した検証方式の効率化 (テストと設計検証論文特集)
- 正規表現を利用したスケーラブル環状回路の検証
- 正規表現を利用したスケーラブル環状回路の検証
- 対称性及び抽象化を利用した検証方式の効率化
- 有限幅遅延モデルに基づく非同期式回路検証方式とその効率化(ペトリネットの応用特集号)