首页 | 本学科首页   官方微博 | 高级检索  
     

变量极小不可满足在模型检测中的应用
引用本文:陈振宇,陶志红,KLEINE BüNING Hans,王立福. 变量极小不可满足在模型检测中的应用[J]. 软件学报, 2008, 19(1): 39-47. DOI: 10.3724/SP.J.1001.2008.00039
作者姓名:陈振宇  陶志红  KLEINE BüNING Hans  王立福
作者单位:东南大学
基金项目:Supported by the National Natural Science Foundation of Chinaunder GrantNos.60425206,60773104,60403016,60633010(国家自然科学基金),in Partby the Jiangsu Planned Projects for Postdoctoral Research Funds of Chinaunder GrantNo.0701003B(江苏省博士后科研资助计划)
摘    要:提出一个结合变量抽象和有界模型检测(BMC)的验证框架,用于证明反例不存在或输出存在反例.引入变量极小不可满足(VMU)的数学概念来驱动抽象精化的验证过程.一个VMU公式F的变量集合是保证其不可满足性的一个极小集合.严格证明了VMU驱动的精化满足抽象精化框架中的两个理想性质:有效性和极小性.虽然VMU的判定问题和极小不可满足(MU)一样难,即DP完全的,该案例研究表明,在变量抽象精化过程中,VMU比MU更为有效.

关 键 词:极小不可满足  抽象精化  模型检测
收稿时间:2006-05-25
修稿时间:2006-11-03

Applying Variable Minimal Unsatisfiability in Model Checking
CHEN Zhen-Yu,TAO Zhi-Hong,KLEINE BNING Hans,WANG Li-Fu. Applying Variable Minimal Unsatisfiability in Model Checking[J]. Journal of Software, 2008, 19(1): 39-47. DOI: 10.3724/SP.J.1001.2008.00039
Authors:CHEN Zhen-Yu  TAO Zhi-Hong  KLEINE BNING Hans  WANG Li-Fu
Affiliation:KLEINE B(U)NING Hans,CHEN Zhen-Yu,TAO Zhi-Hong,KLEINE B(U)NING Hans,WANG Li-Fu
Abstract:This paper presents a framework combining variable abstraction with bounded model checking, in order to prove the counterexamples' absence or establish the counterexamples' existence. A mathematical definition of variable minimal unsatisfiability (VMU) is introduced to drive this abstraction refinement process. The set of variables of VMU formula is a minimal one guaranteeing its unsatisfiability. Furthermore, the authors prove that VMU-driven refinement is valid and minimal by mathematical reasoning. Although the determining problem of VMU is as hard as the well-known problem called minimal unsatisfiability (MU), i.e. DP-complete, the case study has shown that VMU could be more effective than MU in variable abstraction refinement process.
Keywords:minimal unsatisfiability  abstraction refinement  model checking
本文献已被 CNKI 维普 万方数据 等数据库收录!
点击此处可从《软件学报》浏览原始摘要信息
点击此处可从《软件学报》下载全文
设为首页 | 免责声明 | 关于勤云 | 加入收藏

Copyright©北京勤云科技发展有限公司  京ICP备09084417号