| 基于动态Kripke语义直接模型检测及其应用分析 |
| |
| 引用本文： | 陶志红,Hans Kleine Büning,丁德成.基于动态Kripke语义直接模型检测及其应用分析[J].软件学报,2004,15(Z1):83-89. |
| |
| 作者姓名： | 陶志红 Hans Kleine Büning 丁德成 |
| |
| 作者单位： | 南京大学 数学系，江苏 南京 210093;Department ofComputer Science，Paderbom University,Germany;南京大学 数学系，江苏 南京 210093 |
| |
| 基金项目： | 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)). |
| |
| 摘 要： | 在过去的20年里，基于Kdpkc语义结构的模型检测技术在集成电路设计，网络协议分析，程序正确性验证及程序错误发现等方面证明了其有效性和能力．最近，在诸如使用SAT分析工具、有界模型检测等避免OBDDs的模型检测研究方面取得了相当大的进展提出的动态Knpke 语义结构是让原子命题集合AP可以改变．基于这个方法，提出了一个直接模型检测算法．
|
| 关 键 词： | 模型检测：动态Kripke语义结构 分支树逻辑 |
Direct Model Checking Based on Dynamic Kripke Structure and Its Application Analysis |
| |
| Abstract: | |
| |
| Keywords: | |
|
| 点击此处可从《软件学报》浏览原始摘要信息 |
|
点击此处可从《软件学报》下载全文 |
