形式化方法与系统软件:实践与发展建议  

Formal Methods and System Software:Practice and Suggestions

作　　者：丁浩然 王肇国 付明 陈海波[1] DING Haoran;WANG Zhaoguo;FU Ming;CHEN Haibo(School of Software,Shanghai Jiao Tong University,Shanghai 200240,China;Huawei Dresden Research Center,Dresden 01069,Germany)

机构地区：[1]上海交通大学软件学院,上海200240 [2]华为德累斯顿研究所,德国德累斯顿01069

出　　处：《前瞻科技》2023年第1期33-45,共13页Science and Technology Foresight

摘　　要：对高可靠系统软件需求的不断增加使得形式化方法在工业界引起了广泛的兴趣。文章概述了当前主流形式化方法,分析了国内外研究态势,并介绍了形式化方法在设计和实现操作系统、编译器、同步原语、文件系统、数据库系统和分布式共识协议等方面的实践。基于这些实践,进一步总结了形式化方法在系统软件中应用的经验,并从理论和工程两方面讨论其可能面临的挑战,最后针对这些挑战提出发展建议。The growing need for highly reliable system software has drawn widespread interest in formal methods in the industry.This paper presents an overview of the mainstream formal methods and analyzes the current research status in this regard.Then,it describes the application of formal methods in the design and implementation of operating systems,compilers,synchronization primitives,file systems,database systems,and distributed consensus protocols.On this basis,it summarizes the experience learned in applying formal methods to system software and discusses potential challenges from the theoretical and engineering aspects.Finally,it gives some suggestions on how to address these challenges.

关 键 词：形式化方法 操作系统 数据库 文件系统 分布式共识协议 

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