基于逻辑的形式化验证方法:进展及应用  

Logic Based Formal Verification Methods: Progress and Applications

作　　者：陈钢[1] 于林宇[1,2] 裘宗燕[3] 王颖[1] 

机构地区：[1]北京京航计算通讯研究所,北京100074 [2]哈尔滨工业大学航天学院,哈尔滨150001 [3]北京大学数学学院信息科学系,北京100871

出　　处：《北京大学学报（自然科学版）》2016年第2期363-373,共11页Acta Scientiarum Naturalium Universitatis Pekinensis

摘　　要：近年来,形式化方法发展很快,一些技术已经产生工业应用。以逻辑系统为主线,分析几个影响力比较大的形式化验证技术和验证工具,以帮助应用工程师选择并使用形式化工具。主要包括命题演算和时态逻辑方面的SAT、BDD、模型检测和SMT,谓词逻辑方面的ACL2、VDM方法和B方法,以及高阶逻辑方面的HOL、PVS和COQ。还介绍形式化方法在学术界和工业界的应用情况,最后给出几个商业化的形式化验证工具。In recent years, formal methods have undergone a fast development. The authors give a brief review on the formal methods used in software and hardware verification. The main thread of the analysis consists of descriptions of logical systems and their related verification techniques and tools. The purpose is to help engineers to select formal tools and apply them to their work. This paper starts with a review of automated proving techniques based on propositional logic and temporal logic, including SAT, BDD, model checking, and SMT. For first order logic based theorem provers, the authors discuss ACL2, VDM method and B method. Among proof assistants which are based on higher order logics, the authors pick HOL, PVS and COQ. Advancements in commercial formal verification tools are discussed.

关 键 词：形式化方法 逻辑系统 验证技术 

分 类 号：TP301[自动化与计算机技术—计算机系统结构]