Journal of Software:2019.30(1):33-61

(国防科技大学 计算机学院, 湖南 长沙 410073;高性能计算国家重点实验室(国防科技大学), 湖南 长沙 410073;中国科学院 软件研究所, 北京 100190;天基综合信息系统重点实验室(中国科学院 软件研究所), 北京 100190;南京大学 计算机科学与技术系, 江苏 南京 210023;计算机软件新技术国家重点实验室(南京大学), 江苏 南京 210023;西南大学 计算机与信息科学学院, 重庆 400715;西南大学 软件研究与创新中心, 重庆 400715)
Overview of Formal Methods
WANG Ji,ZHAN Nai-Jun,FENG Xin-Yu,LIU Zhi-Ming
(School of Computer, National Univerisity of Defense Technology, Changsha 410073, China;State Key Laboratory for High Performance Computing(National Univerisity of Defense Technology), Changsha 410073, China;Institute of Software, Chinese Academy of Science, Beijing 100190, China;Science & Technology on Integrated Information System Laboratory(Institute of Software, Chinese Academy of Science), Beijing 100190, China;Department of Computer Science and Technology, Nanjing University, Nanjing 210023, China;State Key Laboratory for Novel Software Technology(Nanjing University), Nanjing 210023, China;School of Computer and Information Science, Southwest University, Chongqing 400715, China;Software Research and Innovation Center, Southwest University, Chongqing 400715, China)
Chart / table
Similar Articles
Article :Browse 985   Download 726
Received:October 23, 2018    Revised:October 30, 2018
> 中文摘要: 形式化方法是基于严格数学基础,对计算机硬件和软件系统进行描述、开发和验证的技术.其数学基础建立在形式语言、语义和推理证明三位一体的形式逻辑系统之上.形式化方法已经以不同程度和不同方式愈来愈多地应用在计算系统生命周期的各个阶段.介绍了形式化方法的发展历程和基本方法体系;以形式规约和形式验证为主线,综述了形式化方法的理论、方法、工具和应用的现状,展示了形式化方法与软件学科其他领域的交叉和融合;分析了形式化方法的启示,并展望了其面临的发展机遇和未来趋势.形式化方法的发展和研究现状表明:其应用已经取得了长足的进步,在提高计算系统的可靠性和安全性方面发挥了重要作用.在当今软件日益成为社会基础设施的时代,形式化方法将与人工智能、网络空间安全、量子计算、生物计算等领域和方向交叉融合,得到更加广阔的应用.研究和建立这种交叉融合的理论和方法不仅重要,而且具有挑战性.
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.
文章编号:     中图分类号:    文献标志码:
基金项目:国家自然科学基金(61532007,61632005,61672435,61732019) 国家自然科学基金(61532007,61632005,61672435,61732019)
Foundation items:National Natural Science Foundation of China (61532007, 61632005, 61672435, 61732019)
Reference text:


WANG Ji,ZHAN Nai-Jun,FENG Xin-Yu,LIU Zhi-Ming.Overview of Formal Methods.Journal of Software,2019,30(1):33-61