形式化方法概貌  

Overview of Formal Methods

作　　者：王戟[1,2] 詹乃军[3,4] 冯新宇 刘志明 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)

机构地区：[1]国防科技大学计算机学院,湖南长沙410073 [2]高性能计算国家重点实验室(国防科技大学),湖南长沙410073 [3]中国科学院软件研究所,北京100190 [4]天基综合信息系统重点实验室(中国科学院软件研究所),北京100190 [5]南京大学计算机科学与技术系,江苏南京210023 [6]计算机软件新技术国家重点实验室(南京大学),江苏南京210023 [7]西南大学计算机与信息科学学院,重庆400715 [8]西南大学软件研究与创新中心,重庆400715

出　　处：《软件学报》2019年第1期33-61,共29页Journal of Software

基　　金：国家自然科学基金(61532007;61632005;61672435;61732019)~~

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

关 键 词：形式化方法 形式规约 形式验证 程序设计方法学 软件开发 

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]