BDDによるSpeed-Independent回路の形式的検証
スポンサーリンク
概要
- 論文の詳細を見る
従来, トレース理論によるSpeed-Independent回路の形式的検証が研究されている. しかし, この手法では検証コストが大きかったり, safetyやlivenessが検証できない. 本研究では, BDDによって検証コストを削減して, ω-オートマトンからKripke構造に変換する事によってhazard free, safetyやlivenessを検証する手法を提案する. また, 計算機実験により提案手法の有効性を示す.
- 社団法人電子情報通信学会の論文
- 1997-03-06
著者
-
中村 一博
名古屋大学情報メディア教育センター
-
高橋 健一
(財)九州システム情報技術研究所
-
高橋 健一
島根大学理学部情報科学科
-
中村 一博
島根大学理学部情報科学科
-
山根 智
島根大学理学部情報科学科
関連論文
- IT Forensicの研究開発動向 : アジア国際ワークショップ開催報告(セッション4-B:アクセスログ解析と報告)
- 第3者マシンとの連携による不正侵入検知モデルの提案
- 実時間システムのための近似手法に基づいた記号モデル検査器の開発と評価
- 第3者マシンとの連携による不正侵入検知モデルの提案
- IT Forensicの研究開発動向 : アジア国際ワークショップ開催報告(セッション4-B:アクセスログ解析と報告)
- A-7-11 第3者の助けによる不正侵入検知(A-7. 情報セキュリティ,一般セッション)
- メーリングリストへの投稿先アドレス無効化によるスパムメール防止
- メーリングリストへの投稿先アドレス無効化によるスパムメール防止
- 無限列時間付きステートチャートによる並行システムの仕様記述と検証の手法
- 仮想音響空間における音像定位と頭部形状の関連性についての一考察
- BDDによるSpeed-Independent回路の形式的検証
- ハードリアルタイムシステムの実時間記号モデル検査
- 実時間分散ソフトウェアの可能性と公平性の検証
- 拡張リアルタイム時相論理による分散ソフトウェアの形式的検証
- 分散ソフトウェアのタイミング検証
- 対称性に基づく並行システムの記号モデル検査
- 二分決定グラフによる実時間システムのモデルチェッキング検証
- 二分決定グラフと時間不等式手法に基づく近似解法による実時間シンボリックモデルチェッキング検証
- リージョングラフを用いた時間オートマトンのシンボリックモデルチェッキング検証