《表1 关于形式化方法图灵奖获得者研究清单》

  提示：宽带有限、当前游客访问压缩模式

本系列图表出处文件名：随高清版一同展现

《刍议面向航天器星载软件的形式化验证方法》

1. 获取 高清版本忘记账户？点击这里登录

1. 下载图表忘记账户？点击这里登录

形式化验证通过对系统进行穷尽搜索来进行验证，它以某个或某些形式的规范或属性为依据，使用数学的方法证明其正确性[2]。Robert W.Floyd于1967年提出的最早的形式化方法之一公理化方法验证程序的控制流，以及随后Tony Hoare在此基础上继续研究于1969年提出了程序验证的公理系统Hoare逻辑；陈钢博士在2016年3月的北京大学学报上发表了综述性的文章对基于逻辑的各种形式化验证方法和工具进行分析比较，可以帮助工程师从应用角度选择使用验证工具。清华大学贺飞博士等在软件学报上开辟了软件形式化验证和形式化方法理论基础专题，对最新录用的国内外研究论文进行评价分析；丁明等提出了业务流程上的形式化设计和验证方法；针对应答器报文编制规则黄旭等人给出了形式化建模与验证方法；赵正旭等在2016年进行的Z规格说明的推理与验证；查君鹏针对SPARCv8汇编程序进行了形式化验证；部分图灵奖获得者也在形式化方面进行了一些研究工作，如下表所示[3]。