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

doi:10.13209/j.0479-8023.2015.131

北京大学学报（自然科学版） ›› 2016, Vol. 52 ›› Issue (2): 363-373.DOI: 10.13209/j.0479-8023.2015.131

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

1. 北京京航计算通讯研究所, 北京 100074
2. 哈尔滨工业大学航天学院, 哈尔滨 150001
3. 北京大学数学学院信息科学系, 北京 100871

收稿日期:2014-06-20 出版日期:2016-03-20 发布日期:2016-03-20
通讯作者: 陈钢, E-mail: gangchensh(at)qq.com

Logic Based Formal Verification Methods: Progress and Applications

CHEN Gang¹, YU Linyu^1,2, QIU Zongyan³, WANG Ying¹

1. Beijing Jinghang Research Institute of Computing and Communication, Beijing 100074
2. School of Astronautics, Harbin Institute of Technology, Harbin 150001
3. Department of Information Science, School of Mathematical Science, Peking University, Beijing 100871

Received:2014-06-20 Online:2016-03-20 Published:2016-03-20
Contact: CHEN Gang, E-mail: gangchensh(at)qq.com

摘要/Abstract

摘要： 近年来, 形式化方法发展很快, 一些技术已经产生工业应用。以逻辑系统为主线, 分析几个影响力比较大的形式化验证技术和验证工具, 以帮助应用工程师选择并使用形式化工具。主要包括命题演算和时态逻辑方面的SAT、BDD、模型检测和SMT, 谓词逻辑方面的ACL2、VDM方法和B方法, 以及高阶逻辑方面的HOL、PVS 和COQ。还介绍形式化方法在学术界和工业界的应用情况, 最后给出几个商业化的形式化验证工具。

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

Abstract:

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.

Key words: formal methods, logic systems, verification techniques

中图分类号:

TP301

陈钢, 于林宇, 裘宗燕, 王颖. 基于逻辑的形式化验证方法: 进展及应用[J]. 北京大学学报（自然科学版）, 2016, 52(2): 363-373.

CHEN Gang, YU Linyu, QIU Zongyan, WANG Ying. Logic Based Formal Verification Methods: Progress and Applications[J]. Acta Scientiarum Naturalium Universitatis Pekinensis, 2016, 52(2): 363-373.

[1]	陈梅,张路,许进. 基于Riboswitch的细胞与门构建[J]. 北京大学学报（自然科学版）, 2014, 50(3): 411-415.
[2]	金?,王捍贫,朱梅霞. 基于时序可中断π演算的BPEL和BPEL4People建模[J]. 北京大学学报（自然科学版）, 2012, 48(2): 209-216.
[3]	高良才,汤帜,陶欣,房婧. 一种自动发现、分割与标注引文元数据的方法[J]. 北京大学学报（自然科学版）, 2010, 46(6): 893-900.
[4]	高良才,汤帜,林晓帆,俞银燕,房婧. 一种基于聚类技术的图书目录识别方法[J]. 北京大学学报（自然科学版）, 2010, 46(4): 531-538.
[5]	徐春香,屈婉玲,王捍贫,朱梅霞. 死路删除语义下的WS-BPEL流程的建模[J]. 北京大学学报（自然科学版）, 2010, 46(2): 162-170.
[6]	陈钢,宋晓宇, 顾明. COQ定理证明器辅助PLC 程序验证和分析[J]. 北京大学学报（自然科学版）, 2010, 46(1): 30-34.
[7]	李锌,张飞舟. 基于方向小波变换的分层多描述图像编码[J]. 北京大学学报（自然科学版）, 2008, 44(5): 793-798.
[8]	王宏鼎,谭少华,唐世渭,杨冬青,童云海. 基于模式元素语义关系的模式合并方法研究[J]. 北京大学学报（自然科学版）, 2007, 43(3): 405-411.
[9]	刘鹏,胡建斌,陈钟. 分布式计算环境下的语义安全策略语言[J]. 北京大学学报（自然科学版）, 2006, 42(5): 646-657.
[10]	陈鹏,霍金健,张立昂. 最小生成树问题在RMESH上的常数时间算法[J]. 北京大学学报（自然科学版）, 2006, 42(1): 83-88.
[11]	高韬, 谢昆青, 马修军, 陈冠华. SDML：基于空间数据库的空间数据挖掘语言[J]. 北京大学学报（自然科学版）, 2004, 40(3): 465-472.
[12]	蔡颖琨, 谢昆青, 马修军. 屏蔽了输入参数敏感性的DBSCAN改进算法[J]. 北京大学学报（自然科学版）, 2004, 40(3): 480-486.
[13]	崔鹏,张立昂,吉利久,高立. 两种平滑优化算法在一维情况下的比较研究[J]. 北京大学学报（自然科学版）, 2003, 39(5): 681-689.
[14]	邓志鸿,唐世渭,张铭,杨冬青,陈捷. Ontology研究综述[J]. 北京大学学报（自然科学版）, 2002, 38(5): 730-728.
[15]	刘田. 关于函数的验证复杂性、求值复杂性和输出值个数[J]. 北京大学学报（自然科学版）, 2000, 36(1): 109-116.

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

Logic Based Formal Verification Methods: Progress and Applications

RichHTML

PDF

PDF (翻译版)

可视化

摘要/Abstract

引用本文

使用本文

参考文献

相关文章 15

编辑推荐

Metrics

留言