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

发布时间：2017-08-30 12:37

  本文关键词：基于逻辑的形式化验证方法:进展及应用

  更多相关文章： 形式化方法 逻辑系统 验证技术

【摘要】：近年来,形式化方法发展很快,一些技术已经产生工业应用。以逻辑系统为主线,分析几个影响力比较大的形式化验证技术和验证工具,以帮助应用工程师选择并使用形式化工具。主要包括命题演算和时态逻辑方面的SAT、BDD、模型检测和SMT,谓词逻辑方面的ACL2、VDM方法和B方法,以及高阶逻辑方面的HOL、PVS和COQ。还介绍形式化方法在学术界和工业界的应用情况,最后给出几个商业化的形式化验证工具。
【作者单位】： 北京京航计算通讯研究所;哈尔滨工业大学航天学院;北京大学数学学院信息科学系;
【关键词】： 形式化方法 逻辑系统 验证技术
【分类号】：TP301
【正文快照】： 近年来,形式化方法的研究与应用极其活跃。传统的定理证明器、模型检测器等形式化工具越来越成熟,新的高性能形式化系统层出不穷。在应用领域,一个重要趋势是出现越来越多较大规模的形式验证成果,形式化方法正在走进工业界。在硬件验证领域,形式化方法早已广泛采用。INTEL公司

【相似文献】

中国期刊全文数据库 前10条

1 古天龙;董荣胜;;欧洲高校计算机专业的形式化方法课程教学[J];计算机教育;2008年10期

2 柴振荣;《编程中的形式化方法及其应用》会议[J];管理科学文摘;1995年06期

3 郑士贵;智能服务网络形式化方法的模拟和实质[J];管理科学文摘;1997年01期

4 姜利;孙永强;;形式化方法的发展及展望[J];计算机科学;1998年02期

5 张广泉;关于软件形式化方法[J];重庆师范学院学报(自然科学版);2002年02期

6 崔霞,苗长芬;硬件设计中的形式化方法[J];新乡教育学院学报;2005年02期

7 鹿蕾;;形式化方法B的证明技术[J];现代电子技术;2005年23期

8 陈澎;设计模式形式化方法分析和初步比较[J];计算机工程;2005年02期

9 李建华;李红革;;形式化及其历史发展[J];自然辩证法研究;2008年08期

10 曹源;唐涛;徐田华;穆建成;;形式化方法在列车运行控制系统中的应用[J];交通运输工程学报;2010年01期

中国重要会议论文全文数据库 前7条

1 李文健;;形式化的涵义及其认识论本质[A];1993年逻辑研究专辑[C];1993年

2 吴允曾;;关于形式化的几个问题[A];金岳霖学术思想研究——金岳霖学术思想研讨会论文集[C];1985年

3 郑宇军;石海鹤;薛锦云;;Spec#语言中的形式化特性[A];2005年全国理论计算机科学学术年会论文集[C];2005年

4 雷敏;雷友殉;;一种UML到SDL转换方法的研究与应用[A];2006通信理论与技术新进展——第十一届全国青年通信学术会议论文集[C];2006年

5 苗洁君;王克;;密码模块的形式化设计和验证研究[A];第二十一次全国计算机安全学术交流会论文集[C];2006年

6 缪道期;;评审计算机安全等级[A];第二次计算机安全技术交流会论文集[C];1987年

7 赵晓峰;;城市轨道交通自主化信号系统全面创新实践[A];中国系统工程学会第十八届学术年会论文集——A12系统科学与系统工程理论在各个领域中的应用研究[C];2014年

中国重要报纸全文数据库 前1条

1 殷杰 安军 山西大学科学技术哲学研究中心;21世纪科学哲学的关键词:语境、科学理性与形式化[N];中国社会科学报;2011年

中国博士学位论文全文数据库 前8条

1 刘艳;互联网内容分级服务技术标准体系的形式化设计与验证[D];华中师范大学;2015年

2 钱振江;安全操作系统形式化设计与验证方法研究[D];南京大学;2013年

3 刘强;设计模式的形式化研究及其EMF实现[D];华东师范大学;2011年

4 张鹏;形式化方法在云计算中的应用研究[D];吉林大学;2014年

5 刘洋;网络式软件需求验证的形式化方法研究[D];电子科技大学;2013年

6 王迈;语言形式化原理[D];上海外国语大学;2011年

7 胡静;基于Pi-演算的Web服务形式化描述模型[D];天津大学;2013年

8 周宁;代数化符号模拟验证的应用研究[D];北京交通大学;2015年

中国硕士学位论文全文数据库 前10条

1 王春晓;MDF连续平压质量控制形式化建模及优化研究[D];东北林业大学;2015年

2 王亚丽;面向机器人规划的形式化研究[D];北京化工大学;2015年

3 Hamza I.Bangura;基于Z规格的软件缺陷形式化方法[D];天津大学;2010年

4 钟琪;软件分析模式的形式化研究[D];西南师范大学;2004年

5 王祥兵;形式化方法的理论及其影响[D];贵州大学;2009年

6 郭忠伟;神经内分泌复杂系统的形式化研究[D];扬州大学;2009年

7 王晓帆;基于模糊数学的形式化开发方法研究[D];西安理工大学;2003年

8 闵洪军;软件工程中形式化方法研究[D];浙江大学;2006年

9 张杨;UML模型形式化转换及验证的研究[D];太原理工大学;2013年

10 匡春临;并发系统的形式化技术研究[D];华侨大学;2008年

，

本文编号：759355