形式化方法概貌
作者:
作者单位:

作者简介:

王戟(1969-),男,博士,教授,博士生导师, CCF高级会员,主要研究领域为软件方法学,软件分析与验证,并行与分布计算;詹乃军(1971-),男,博士,研究员,博士生导师,CCF杰出会员,主要研究领域为计算软件与理论;冯新宇(1978-),男,博士,教授,博士生导师,CCF专业会员,主要研究领域为程序设计语言理论,形式化程序验证;刘志明(1961-),男,博士,教授,博士生导师,CCF专业会员,主要研究领域为软件理论与方法.

通讯作者:

刘志明,E-mail:zhimingliu88@swu.edu.cn

基金项目:

国家自然科学基金(61532007,61632005,61672435,61732019)


Overview of Formal Methods
Author:
Affiliation:

Fund Project:

National Natural Science Foundation of China (61532007, 61632005, 61672435, 61732019)

  • 摘要
  • |
  • 图/表
  • |
  • 访问统计
  • |
  • 参考文献
  • |
  • 相似文献
  • |
  • 引证文献
  • |
  • 资源附件
    摘要:

    形式化方法是基于严格数学基础,对计算机硬件和软件系统进行描述、开发和验证的技术.其数学基础建立在形式语言、语义和推理证明三位一体的形式逻辑系统之上.形式化方法已经以不同程度和不同方式愈来愈多地应用在计算系统生命周期的各个阶段.介绍了形式化方法的发展历程和基本方法体系;以形式规约和形式验证为主线,综述了形式化方法的理论、方法、工具和应用的现状,展示了形式化方法与软件学科其他领域的交叉和融合;分析了形式化方法的启示,并展望了其面临的发展机遇和未来趋势.形式化方法的发展和研究现状表明:其应用已经取得了长足的进步,在提高计算系统的可靠性和安全性方面发挥了重要作用.在当今软件日益成为社会基础设施的时代,形式化方法将与人工智能、网络空间安全、量子计算、生物计算等领域和方向交叉融合,得到更加广阔的应用.研究和建立这种交叉融合的理论和方法不仅重要,而且具有挑战性.

    Abstract:

    Formal methods are techniques with mathematical foundations for specifying, developing, and verifying computer software and hardware systems. Their mathematical foundations lie in formal logic systems, consisting of formal languages, semantics, and proof systems. Formal methods have been increasingly applied in different stages of the lifecycle of a computing system with appropriate levels of rigor. This paper reviews the historic development of formal methods. Focusing on specification and verification, the paper discusses and introduces the state-of-the-art mainstream formal methods in details, including their theories, techniques, tools, and applications. It is also shown that the relation between formal methods and other fields of computer science. Finally, the opportunities, trends, and challenges of formal methods are forseen. Formal methods have made significant progresses and played crucial roles to guarantee the safety and security of computing systems. Now software is becoming a fundamental infrastructure, it is believed that formal methods will gain much wider applications, especially when they are used in combination with other theories and methods such as those in artificial intelligence, cyber security, quantum computing, and bioinformatics. Research to achieving such seamless combinations is, however, both challenging and important.

    参考文献
    相似文献
    引证文献
引用本文

王戟,詹乃军,冯新宇,刘志明.形式化方法概貌.软件学报,2019,30(1):33-61

复制
分享
文章指标
  • 点击次数:
  • 下载次数:
历史
  • 收稿日期:2018-10-23
  • 最后修改日期:2018-10-30
  • 录用日期:
  • 在线发布日期: 2018-11-23
您是第位访问者
版权所有:中国科学院软件研究所 京ICP备05046678号-3
地址:北京市海淀区中关村南四街4号,邮政编码:100190
电话:010-62562563 传真:010-62562533 Email:jos@iscas.ac.cn
技术支持:北京勤云科技发展有限公司

京公网安备 11040202500063号