软件学报

作者：王戟,詹乃军,冯新宇,刘志明

单位：王戟，国防科技大学 计算机学院, 湖南 长沙 410073;高性能计算国家重点实验室(国防科技大学), 湖南 长沙 41007311,詹乃军，中国科学院 软件研究所, 北京 100190;天基综合信息系统重点实验室(中国科学院 软件研究所), 北京 10019002,冯新宇，南京大学 计算机科学与技术系, 江苏 南京 210023;计算机软件新技术国家重点实验室(南京大学), 江苏 南京 21002303,刘志明，西南大学 计算机与信息科学学院, 重庆 400715;西南大学 软件研究与创新中心, 重庆 40071504

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

基金：国家自然科学基金（61532007，61632005，61672435，61732019）

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

来源：2019年第1期

《软件学报》期刊编辑部

查看软件学报杂志2019年第1期