主页期刊介绍编委会编辑部服务介绍道德声明在线审稿编委办公编辑办公English
2019-2020年专刊出版计划 微信服务介绍 最新一期:2019年第3期
     
在线出版
各期目录
纸质出版
分辑系列
论文检索
论文排行
综述文章
专刊文章
美文分享
各期封面
E-mail Alerts
RSS
旧版入口
中国科学院软件研究所
  
投稿指南 问题解答 下载区 收费标准 在线投稿
王戟,詹乃军,冯新宇,刘志明.形式化方法概貌.软件学报,2019,30(1):33-61
形式化方法概貌
Overview of Formal Methods
投稿时间:2018-10-23  修订日期:2018-10-30
DOI:10.13328/j.cnki.jos.005652
中文关键词:  形式化方法  形式规约  形式验证  程序设计方法学  软件开发
英文关键词:formal method  formal specification  formal verification  programming methodology  software development
基金项目:国家自然科学基金(61532007,61632005,61672435,61732019)
作者单位E-mail
王戟 国防科技大学 计算机学院, 湖南 长沙 410073
高性能计算国家重点实验室(国防科技大学), 湖南 长沙 410073 
 
詹乃军 中国科学院 软件研究所, 北京 100190
天基综合信息系统重点实验室(中国科学院 软件研究所), 北京 100190 
 
冯新宇 南京大学 计算机科学与技术系, 江苏 南京 210023
计算机软件新技术国家重点实验室(南京大学), 江苏 南京 210023 
 
刘志明 西南大学 计算机与信息科学学院, 重庆 400715
西南大学 软件研究与创新中心, 重庆 400715 
zhimingliu88@swu.edu.cn 
摘要点击次数: 1562
全文下载次数: 1243
中文摘要:
      形式化方法是基于严格数学基础,对计算机硬件和软件系统进行描述、开发和验证的技术.其数学基础建立在形式语言、语义和推理证明三位一体的形式逻辑系统之上.形式化方法已经以不同程度和不同方式愈来愈多地应用在计算系统生命周期的各个阶段.介绍了形式化方法的发展历程和基本方法体系;以形式规约和形式验证为主线,综述了形式化方法的理论、方法、工具和应用的现状,展示了形式化方法与软件学科其他领域的交叉和融合;分析了形式化方法的启示,并展望了其面临的发展机遇和未来趋势.形式化方法的发展和研究现状表明:其应用已经取得了长足的进步,在提高计算系统的可靠性和安全性方面发挥了重要作用.在当今软件日益成为社会基础设施的时代,形式化方法将与人工智能、网络空间安全、量子计算、生物计算等领域和方向交叉融合,得到更加广阔的应用.研究和建立这种交叉融合的理论和方法不仅重要,而且具有挑战性.
英文摘要:
      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.
HTML  下载PDF全文  查看/发表评论  下载PDF阅读器
 

京公网安备 11040202500064号

主办单位:中国科学院软件研究所 中国计算机学会
编辑部电话:+86-10-62562563 E-mail: jos@iscas.ac.cn
Copyright 中国科学院软件研究所《软件学报》版权所有 All Rights Reserved
本刊全文数据库版权所有,未经许可,不得转载,本刊保留追究法律责任的权利