| 摘要: |
| 在过去的20年里，基于Kdpkc语义结构的模型检测技术在集成电路设计，网络协议分析，程序正确性验证及程序错误发现等方面证明了其有效性和能力．最近，在诸如使用SAT分析工具、有界模型检测等避免OBDDs的模型检测研究方面取得了相当大的进展提出的动态Knpke 语义结构是让原子命题集合AP可以改变．基于这个方法，提出了一个直接模型检测算法． |
| 关键词: 模型检测：动态Kripke语义结构 分支树逻辑 |
| DOI： |
| 分类号: |
| 基金项目:Supporsted by the National High-Tech Research and Development Plan of China under Grant No．2001 AA113171(国家高技术研究发展计划(863)); the National Grand Fundamental Research 973 Program of China under Grant No.2002CB312006(国家重点基础研究发展规划(973)). |
|
| Direct Model Checking Based on Dynamic Kripke Structure and Its Application Analysis |
|
TAO Zhi-Hong,Hans Kleine Büning,DING De-Cheng
|
| Abstract: |
| During the past two decades Model Checking based on Kripke Semantics Structure has proven its efficacy and powerful in circuit design，network protocol analysis，program verification and bug bunting．Recently there has been considerable research on Model Checking without OBDDs such as using SAT Solver or Bounded Model Checking (BMC). A Dynamic Kxipke Semantics Structure is introduced through allow the AP set changed．Based on this method．a new direct model checking algodthm is proposed． |
| Key words: model checking dynamic IG-ipke SCln~fiCS stnlcturei CTL logic |
