复杂系统规约、分析与验证发展现状与展望  

Challenges and Trends for Specification,Analysis,and Verification of Complex Systems

作　　者：詹乃军[1,2] 王戟[3,4] ZHAN Naijun;WANG Ji(Science&Technology on Integrated Information System Laboratory,Institute of Software,Chinese Academy of Sciences,Beijing 100190,China;State Key Laboratory of Computer Science,Institute of Software,Chinese Academy of Sciences,Beijing 100190,China;College of Computer Science and Technology,National University of Defense Technology,Changsha 410073,China;State Key Laboratory of High-Performance Computing,National University of Defense Technology,Changsha 410073,China)

机构地区：[1]中国科学院软件研究所天基综合信息系统重点实验室,北京100190 [2]中国科学院软件研究所计算机科学国家重点实验室,北京100190 [3]国防科技大学计算机学院,长沙410073 [4]国防科技大学高性能计算国家重点实验室,长沙410073

出　　处：《前瞻科技》2023年第1期7-22,共16页Science and Technology Foresight

基　　金：国家重点研发计划(2022YFA1005101);国家自然科学基金(62192732,62032024,61732001);中国科学院稳定支持基础研究领域青年团队计划(YSBR-040)。

摘　　要：形式化方法包括计算系统(软硬件和网络)的规约、构造、分析与验证的数学基础、技术和工具。随着安全攸关系统在国民经济和国防等关键领域的应用越来越多,复杂系统可信性问题日益凸显。形式化方法已经成为开发安全可靠的安全攸关系统的关键技术之一,也是解决中国“缺芯少魂”的核心技术之一,同时也是国际学术前沿。文章回顾国内外形式化方法研究现状,分析国内外研究差距,并提出加强中国这方面基础研发的若干建议。Formal methods provide mathematical theories,techniques,and tools for the specification,construction,analysis,and verification of computing systems(including hardware,software,and networks).As safety-critical systems are more widely applied to key fields related to national economics and defense,the trustworthiness problem of complex systems becomes prominent and challenging.Formal methods have become a key technology for developing dependable safety-critical systems and solving China’s problem of deficient microchips and operating systems.They are also the frontiers of international academics.This paper reviews the current status of formal methods,analyzes the gap between China and other countries in this regard,and proposes some suggestions on ways of strengthening the basic research on formal methods in China.

关 键 词：形式化方法 安全攸关系统 形式规约 形式分析与验证 

分 类 号：TP30[自动化与计算机技术—计算机系统结构]