全文刊载于《前瞻科技》2023年第1期"形式化方法与复杂计算系统可信保障专刊”。

文章摘要

形式化方法包括计算系统（软硬件和网络）的规约、构造、分析与验证的数学基础、技术和工具。随着安全攸关系统在国民经济和国防等关键领域的应用越来越多，复杂系统可信性问题日益凸显。形式化方法已经成为开发安全可靠的安全攸关系统的关键技术之一，也是解决中国“缺芯少魂”的核心技术之一，同时也是国际学术前沿。文章回顾国内外形式化方法研究现状，分析国内外研究差距，并提出加强中国这方面基础研发的若干建议。

文章速览

现代计算科学诞生于“什么是计算”“如何计算”“计算的代价”和“计算正确性”等计算本质问题的探索。20世纪30年代，Turing的图灵机，Gödel、Herbrand和Kleene的递归函数，Church的λ演算等计算模型的相继提出标志着可计算性理论的创立，建立了现代存储程序计算机理论模型，奠定了第一台现代计算机诞生的基础。20世纪50年代，Rabin和Scott提出的自动机理论和Chomsky建立的形式语言理论实质性地促进了程序设计和线路设计技术的发展；20世纪60年代，McCarthy提倡使用数学方法研究程序语义，促进了形式化方法研究的活跃，包括操作语义、代数语义、指称语义和公理语义等在内的各种形式语义相继提出。同时，为了解决软件正确性问题，Floyd和Hoare等提出了基于逻辑和自动机的形式验证技术，这标志着形式化方法作为一个独立研究方向的诞生。受其工作影响，各种规约语言及开发方法相继被提出，如Floy-Hoare逻辑、动态逻辑、VDM（Vienna Development Method）和Z开发方法等。

20世纪70年代初，Dijkstra提出如何设计正确的并发和分布式计算系统的科学问题，激发了并发和分布式系统设计理论研究的高潮。程序设计语言理论方面，Dijkstra提出了P-V操作机制，Hoare提出了管程（Monitor）机制等；并发和分布式模型方面，Hoare提出了CSP理论，Milner提出了CCS理论等；规约逻辑方面，Pnueli提出了线性时序逻辑，Clarke和Emerson提出了计算树逻辑，Lamport提出了动作时序逻辑等；验证技术方面，Clarke和Emerson、Sifakis和Queille建立了模型检验技术等。20世纪80—90年代，模型检验技术快速发展，各种状态符号表示和约减技术及高效搜索算法相继提出，如二叉决策图（Binary Decision Diagram, BDD）、偏序约减、符号模型检验、限界模型检验等。因为模型检验完全自动，效率和能力的提升使其在工业界获得巨大成功，实际上已经成为硬件设计和验证的一个标准技术。

与此同时，随着软件社会基础设施越来越重要，如何保证复杂软件正确性和可靠性的需求日益突出，特别是航天器、飞机、高速列车、核反应堆等复杂且安全攸关系统控制软件。对这些软件进行完全功能和信息安全验证超出了模型检验的能力，同时也源于定理证明的基础性地位和工具的发展，自动和交互式定理证明技术再次成为研究热点。一方面，人们提出了各种表达能力强的元逻辑作为交互式定理证明器的逻辑基础，并实现了各种交互式定理证明器，如Coq、Isabelle/HOL、PVS等；另一方面，研究了各种定理证明自动化程度提高技术，如消解原理、Horn子句求解、叠置等。同时，人们提出了SMT求解技术，并开发了许多高效求解器，如Z3、CVC5等。特别是SMT求解器不仅成功应用于软硬件和网络设计，而且在软件测试、系统仿真、监测等其他方向和领域有着广泛应用。

理论上，形式化方法是为建立计算系统的基础理论而诞生，并随着计算机科学进步而发展，是计算系统的规约、构造、分析与验证的数学基础、技术和工具。实践上，形式化方法已经成功应用于各种硬件设计，成为芯片设计和验证的必备技术；同时，形式化方法已经成为提高软件可信性的关键技术，为工业软件和基础软件开发提供理论基础和平台工具支撑。事实上，形式化方法在微软（Microsoft）、华为、新思科技（Synopsis）、脸书（Facebook）、亚马逊（Amazon）、中国航天科技集团、中国航空工业集团、中国铁路总公司等公司产品开发过程中得到重要应用，提高了其商业软件的可信性。国际上已经出现了一批以形式化方法为核心竞争力的高科技公司，如Galois、Praxis等。形式化方法已经成为安全攸关系统安全设计的重要方法，并在工业界各种标准和规范中得到明确推荐使用。例如，铁路行业的EN 50126、EN 50128、EN 50129、EN 50159，航空行业的ARP4754、DO-178b、DO3333，核电行业的EN-60880，军工行业的MIL-STD-883，面向安全相关工业控制系统的IEC-61508等。

总之，形式化方法正在向复杂系统领域渗透迈进，特别是复杂系统规约、分析与验证技术及工具是国际学术前沿，也是解决中国信息基础“缺芯少魂”的核心关键技术。突破相关技术问题迫在眉睫。国家需要加强形式化方法基础研究，解决复杂系统规约、分析与验证技术等一系列前沿问题，突破国家芯片设计、基础软件和工业软件等复杂关键软件的供给能力瓶颈。

1国外研究进展

根据文献[1]的定义，形式化方法是基于严格数学基础，对计算系统包括软硬件和网络进行形式规约、开发和验证的技术。其中，形式规约是使用形式语言构建所开发的软件系统的规约，它们对应于软件生命周期不同阶段的制品，刻画系统不同抽象层次的模型和性质，如需求模型、设计模型甚至代码和代码的执行模型等。分析与验证是证明不同形式规约之间的逻辑关系，这些逻辑关系反映了软件制品之间的软件开发不同阶段需要满足的各类正确性需求。例如，分析与验证给出“系统设计模型满足若干特定性质”的反例或者证明构造。在形式规约和分析与验证的基础之上，形式化开发主要是构造、证明形式规约之间的等价转换或者满足精化关系，以系统的形式模型为指导，逐步精化，开发出满足需要的系统，也称为构造即正确（Correct by Construction）的开发。下面将分别介绍形式规约、分析与验证等方面的国外研究进展。

1.1 形式规约

形式规约是由形式规约语言严格描述的系统模型或者系统需要满足的性质。前者称为模型规约，后者称为性质规约。根据形式规约语言的不同，常用复杂系统的规约可以分为图形规约、迁移系统规约、代数规约、进程代数规约、逻辑规约，以及上述形式的集成规约等。

（1）图形规约。该规约就是使用不同含义的图形表示复杂系统的不同构件，而这些图形构件连接组合成完整系统。图形规约的优点是直观、理解容易、使用方便、高效。它们已经在工业界广泛使用，如UML、Simulink/Stateflow、Modelica、SCADE等。特别是很多图形规约支持仿真和代码自动生成，是模型驱动开发方法的主要途径。但是图形规约往往缺乏严格性，其安全性和可靠性保证主要依赖仿真，对安全攸关系统开发支持不够。

（2）迁移系统规约。该规约主要使用一些具有严格数学含义的各种数学图形描述系统行为，如Kriple结构、Petri网、Statecharts、有穷状态机等及其扩充。这些模型能够描述系统的整体行为，非常直观，因而可以在此基础上设计基于状态空间搜索的自动验证技术，如模型检验等。为了对具有复杂特征的系统行为建模，人们对迁移系统进行了各种扩充。以自动机为例，其后续扩展包括时间自动机、混成自动机、概率时间自动机、随机混成自动机等。而且这些模型不再局限于计算机领域，已经广泛应用于控制、生物、物理、化学等诸多领域。

（3）代数规约。该规约就是使用一个代数结构描述一个复杂系统，其中每个系统状态变量对应一个类子，系统状态变量上的各种操作对应类子间的运算符，而这些操作的含义以及约束关系描述成一组多类等式逻辑的公理。代数规约的优点是具有非常好的数学基础，任意操作序列的计算结果可以自动得到、自动执行，如第四代语言（Fourth Generation Language, 4GL）。但是等式逻辑的表述能力有较大局限性，不能表达一般的程序结构和行为。目前常用的代数规约语言包括Maude、OBJ、Larch等。代数规约对程序设计理论和软件工程影响非常广泛，例如早期的抽象数据类型，后来的面向对象程序设计及ML等函数式程序设计语言等。

（4）进程代数规约。为了研究并发和分布式系统，人们相继提出了CSP、CCS、ACP等各种进程代数（演算）。CCS和CSP都最大限度地将并发通信系统的数据状态和数据计算功能抽象掉，重点关注通信、同步、异步等，是基于事件的规约语言。基于进程代数的规约具有非常好的结构特征，适合对复杂系统，特别是并发和分布式系统进行建模。为了处理并发系统的其他特征，如信息安全、移动、实时、混成、概率和随机，这些并发模型均进行了各种扩充。例如，为了处理实时系统，Reed和Roscoe扩充CSP到实时系统，建立了Timed CSP；为了处理混成系统，何积丰和周巢尘等将CSP扩充到混成系统，建立了HCSP；为了处理移动计算，Milner提出了π-演算，后被Cardelli和Gordon进一步扩充为Ambient-calculus；为了处理信息安全，Abadi等将π-演算改进成Spi-演算等。

（5）逻辑规约。性质规约语言基于程序逻辑，通过逻辑公式来描述一组性质以定义所期望的系统行为（指系统的每个执行）。性质规约不直接定义系统的具体行为。基于性质的形式规约偏向于说明性的，逻辑约束往往是最小必要的，以给出较大的实现空间。Lamport指出，系统需要满足的性质可以分成两类：安全性，即不好的事情从不发生；活性，即好的事情一定能够发生。Alpern和Schneider证明任何性质均可以表示成这两种性质的交。表达系统性质的逻辑非常多，大概可以分为如下几个大类。①Floyd-Hoare逻辑及其后续发展。Floyd-Hoare逻辑的公式形如{Pre} P {Post}，其中，Pre和Post是一阶逻辑公式，分别称为前、后置断言，P是程序。Floyd-Hoare逻辑是现在程序验证的理论基础，目前主要程序验证方法基于Floyd-Hoare-Naur归纳断言方法，其核心是程序不变式生成和终止性分析。Floyd-Hoare逻辑后续发展包括Dijkstra的WP演算、各种并发Hoare逻辑、分离逻辑、混成Hoare逻辑、关系Hoare逻辑、量子Hoare逻辑等。②模态和时序逻辑及其后续发展，又可分为线性时序逻辑、分支时序逻辑和动态逻辑等，如LTL、CTL、μ-演算等。这些逻辑是将传统模态逻辑在程序上进行重新解释获得的，一般具有最小模型性质，从而永真性、可满足性和模型检验都是可判定的，可以实现对性质的自动验证。这些逻辑的模型检验工具如Spin、SMV、UPPAAL等已被广泛应用。③各种一阶逻辑、高阶逻辑或者类型系统，其表达能力强，一般作为交互式定理证明的元逻辑，例如基于高阶逻辑的Isabelle/HOL、基于依赖类型论的Coq、基于一阶逻辑的RODIN等。

近年，人们发现信息流安全策略、信息物理融合系统敏感性等不再是针对单独一个系统运行的性质，而是运行集合上的性质，称为超性质（Hyperproperty）。为了处理超性质，已经有许多工作将传统规约逻辑扩充到超性质。

（6）集成规约。上述各种规约的优缺点均非常明显，一种规约很难描述系统在不同抽象层模型及它们之间的精化关系，并最终生成代码。为此，人们结合上述各种规约技术以及程序设计语言特点，设计了各种集成规约语言，如早期的VDM、Z等。例如，VDM包括数据类型的规约和程序结构（即模块）的规约；数据类型的规约定义具有该类型的数据以及数据上的操作，由一阶谓词逻辑描述数据的范围约束以及操作需要满足的约束；一个模块的规约说明程序变量及其类型以及一组过程或函数；过程和函数的功能约束由Floyd-Hoare逻辑来定义；VDM同时定义了模块的组合机制以及不同抽象层模型间精化机制等。为了提供面向对象的软件规约和精化，VDM扩展到VDM++，Z扩展为Object-Z等。另外，目前比较流行的集成规约语言还有B、Event-B、Alloy、JML等。

1.2 分析与验证

形式化方法最显著的作用是能够对形式规约进行分析与验证。分析与验证的常见方法有静态分析、定理证明、模型检验等。

1.2.1 静态分析

静态分析是指基于程序语法结构，不依赖程序执行，静态地分析程序性质及执行效果，主要用于编译优化、程序理解、调试和测试、性能分析（如实时性分析和资源消耗等）、信息安全等。常用静态分析技术包括基于类型和效果系统分析（Analysis based on Type and Effect System）、控制流分析、基于约束求解的分析和抽象解释等。

基于类型和效果系统分析的基本思想是在编译时，利用类型与效果系统检测，分析程序执行效果，验证程序性质，如内存安全分析、数据竞争检测、性能分析、正确性验证等。相较于其他分析技术，静态分析具有简单、高效和可靠等优点。这项技术已被广泛应用于编译器的设计。

控制流分析是指不需要执行程序而根据其控制流图分析其执行时信息的技术。它包含两个基本步骤：①gen/kill算法遍历程序收集相关信息；②根据步骤①所收集的信息推导出方程组（可以前向或者后向）并分析。目前，控制流分析主要应用于可达性、实时性分析、资源消耗等，如可用表达式分析、可达定义分析、变量依赖关系分析、最坏执行时间分析等。

基于约束求解的分析技术主要根据程序语法，符号化执行程序，根据执行路径产生各种约束。它可以用于性质验证、性能分析等，也可以应用于测试用例生成等。这与后面基于自动定理证明的程序验证非常类似，严重依赖约束求解器能力和效率。

抽象解释是根据定义的抽象域对程序语义进行近似的技术，它不需要实际执行，可以静态地分析程序性质。它的核心组成是程序的抽象域以及程序在抽象域上的抽象执行，一般需要保证抽象执行必须终止。为了保证抽象执行能够快速收敛，需要加宽操作；同时，为了避免加宽操作过度，从而导致分析结果没有意义，需要考虑变窄操作。相较于上述几种静态分析技术，抽象解释的主要优点是尽管代价变高，但是可以分析和验证更复杂性质的大规模的程序，并且非常高效（相较于验证技术）。例如，ASTREE成功应用于AIR BUS 380上千万行程序，检查数组越界、除法为零等运行时错误。

1.2.2 定理证明

基于定理证明的形式验证将“系统满足其规约”这一论断作为逻辑命题。它要么通过规约逻辑的证明系统，以演绎推理的方式自动地或者交互式地对该命题开展证明；要么基于规约逻辑可满足性和永真性判定过程，自动证实或者证伪逻辑命题。自动演绎推理可以基于消解原理、叠置方法、Horn子句求解、人工智能的证明策略推荐。基于自动演绎推理和判定过程的定理证明称为自动定理证明，而基于交互式演绎推理的定理证明称为交互式定理证明。交互式定理证明能力更强，可以适用各种复杂问题的验证，但是往往验证效率低、掌握难度大。如何提高自动化程度是其面临的挑战。目前，提高交互式定理自动化程度的途径有以下几种。

（1）证明策略。交互式定理证明的自动化传统上依靠在交互式定理证明器里实现证明策略（Tactics），几乎所有的常用交互式定理证明器都提供实现证明策略的语言，如OCaml或ML。对于Coq，Czajka等提供了一个更高层次的证明策略语言。如何改善这些语言，让用户能够更直观地实现证明策略是一个长久的问题。近年，如何利用人工智能技术自动合成证明策略成为研究热点。

（2）调用自动定理证明器。很多交互式定理证明器都在使用或尝试使用这种自动化方法。其中，Isabelle里的Sledgehammer最具代表性，现在已成为Isabelle大多数应用中必不可少的工具。但是，使用外部自动定理证明器的一个弱点是无法处理涉及高阶逻辑的命题。虽然存在一些从高阶逻辑的命题转换到一阶逻辑的算法，但转换的过程可能会让命题变得非常烦琐。

（3）构件证明库。类似开源软件，把一个常用定理及特定领域理论实现放到证明库中，这样在实际验证中遇到相同定理或者定理依赖的理论时，直接调用，可以大大提高验证效率。近年，针对各种特定领域的定理证明库不断完善。但如何搜索和推荐定理证明库中已有定理变得日益重要，而人工智能技术正好可以在其中发挥巨大作用。

另外，逻辑基础是交互式定理证明器设计的另外一个关键问题。逻辑基础除了保证可靠性以外，应当能够有效地表达需要证明的理论，并且让实际的证明过程尽可能地方便。例如，Isabelle/HOL等使用一种简单的（不包含依赖类型的）类型论（Simple Type Theory，或者称为Higher-order Logic）；Coq和Lean的使用依赖类型论（Dependent Type Theory）。逻辑基础的一个最新的进展是同伦类型论（Homotopy Type Theory），它是一种基于依赖类型的更复杂的类型论。

相较而言，自动定理证明是完全自动的，如果不满足甚至可以给出反例，因而容易使用，但是能够验证的问题受限，必须是可判定的，其中推理和判定算法效率是一个瓶颈。特别是设计各种复杂约束高效求解和近似算法，以及如何将这些针对不同理论的判定算法组合起来，验证组合性质是一个巨大挑战。

目前有许多成熟交互式定理证明工具，如Coq、Isabelle、Lean、PVS等。这些工具已被成功应用于大型软件系统的验证，如操作系统微内核（如seL4）、程序语言编译器（如CompCert）等。也有许多成熟的自动定理证明工具，如基于自动演绎的定理证明器Vampire、Auto2等；基于判定算法的，特别是SAT/SMT约束求解器，如MaxSAT、Z3、CVC5等。这些工具已被广泛应用于计算系统的设计、分析和验证，以及其他领域。

1.2.3 模型检验

模型检验分别由Clarke和Emerson、Queille和Sifakis在20世纪80年代初各自独立提出，其基本思想是通过自动遍历系统模型的有穷状态空间来检验系统的语义模型是否满足其性质规约。通常，在模型检验中，使用有穷状态机表示系统模型，使用时序逻辑公式表示性质规约。如果系统模型（模型规约）不满足性质（性质规约），模型检验算法会给出系统行为不满足性质规约的反例，用户可以根据反例进行分析和调试；如果模型检验未发现反例，则系统一定满足所检验的性质。如何对模型状态空间进行搜索，依赖规约逻辑，例如CTL模型检验通常用深度优先或者宽度优先算法，搜索模型中每个状态满足给定CTL公式的子公式集合；而LTL的模型检验算法通常将待验证公式取反，然后转换成一个Büchi自动机，并和系统模型（通常表示成另外一个Büchi自动机）做乘积，从而将模型检验问题归结为乘积自动机的可达性问题。

模型检验的核心是有穷状态空间上的遍历策略和算法。因而模型检验的关键问题是如何在可表示的状态空间和有效的时间内完成状态搜索，主要挑战是如何应对系统状态爆炸。目前主要有如下几种方法。

（1）结构化方法。结构化方法利用定义系统的语法表达（模型）结构来缓解状态空间爆炸问题。典型的方法有对称模型检验、on-the-fly的状态空间搜索、偏序模型检验、参数化模型检验等。

（2）符号化方法。符号化方法将模型迁移结构的状态和迁移编码为逻辑公式。这种符号化编码能够有效压缩表示状态集合的数据结构，状态变迁的操作也相应高效。符号化的编码方法常常基于BDD、命题公式或者无量词的一阶约束等。

（3）抽象方法。抽象方法将复杂系统的状态空间结构归约为较小的同态映像。后者是前者的一个上近似（Over-approximation），从而把原系统的验证转化成模型检验可以处理的问题，如谓词抽象方法等。而作为更一般化的方法，抽象解释是一种基于序集合上单调函数对程序形式语义进行可靠近似的理论，为程序自动分析提供了一个通用的框架。

（4）限界方法。限界方法的基本思想非常简单，仅仅搜索给定长度路径上的所有状态，这样搜索空间可以根据实际需要设定。这主要用于系统找错，特别是和测试结合较多。与路径分析方法相结合，例如与基于插值的不动点计算相结合，限界模型检验也可以做无界验证，如著名工具IC3。

利用符号化方法或数据抽象的方法将无穷状态系统转换为一个“性质等价”的有穷状态表示系统的抽象，从而可以对一些无穷状态系统进行模型检验。例如，实时系统模型（时间自动机）的状态空间是无穷的，模型检验时用Region或者差分有界矩阵（Difference Bounded Matrix, DBM）来表示系统抽象状态，从而可以将时间自动机模型检验问题归结为有穷图的可达性问题而高效求解。典型的实时模型检验工具有UPPAAL等。

另外，实际系统中存在不确定性，这在信息物理融合系统中是固有的，例如系统中物理部件的信息感知不准确、传输丢失等。为此，在这些系统模型的描述中，通过引入概率或者随机元素来表达系统的不确定性，并在设计策略中，通过容错、容变机制来获得期望的量化性质。这类系统量化性质的模型检验可以通过概率模型检验和统计模型检验来实现，概率模型检验工具有PRISM和IscasMC等。

1.3 工业应用

形式规约、分析与验证计算机硬件系统设计应用十分成功。1992年，Clarke等利用SMV验证了IEEE Futurebus+标准896.1—1991中高速缓存（Cache）一致性协议，发现了一些过去未发现的潜在错误。国际斯坦福研究所（SRI）和洛克威尔自动化公司（Rockwell Automation）合作使用PVS系统，规约和验证了AAMP5微处理器，发现了设计中若干微码的错误。1994年出现的Intel Pentium浮点单元中的缺陷对后来的芯片设计产生了巨大的影响。随后，形式分析与验证技术已经成为硬件设计标配技术，各大硬件制造商都有一个非常强大的形式化方法团队为保障系统的可靠性提供技术支持，如国际商业机器公司（IBM）、英特尔公司（Intel）、超威半导体公司（AMD）等。特别是近年SAT/SMT求解器的能力和效率的大幅提升，使采用形式分析与验证技术进行工业级别硬件验证成为可能。例如，20世纪80年代，SAT求解器能够求解含有几十个布尔变量的公式已经是极限，现在的SAT求解器可以求解上千万布尔变量的公式，基本可以应对尺寸较小的芯片设计需求。

形式化方法在软件领域的应用比硬件要早，但在工业界的影响相对要小，主要因为软件系统的复杂性远高于硬件，相应的软件系统形式化工具水平也远低于硬件形式化工具。即使如此，形式化方法在工业界也得到了一些成功应用。例如，早在20世纪80年代，Moore等就开展了对CLI软件栈（CLI Stack）的形式验证；20世纪90年代，人们成功应用B方法开发了巴黎地铁的14号线控制系统和巴黎Roissy机场无人驾驶控制系统的关键软件，大约占整个软件系统的1/3；2000年前后，德国在“复杂系统自动验证分析”（Automated Verification and Analysis for Complex Systems, AVACS）项目支持下，验证了欧洲列车控制系统（European Train Control System, ECTS）的正确性，主要理论工具是中国计算机科学家提出的时段演算理论。近年，随着以SMT为代表的自动定理证明技术以及以高阶逻辑和依赖类型理论为理论基础的交互式定理证明技术的快速发展，形式分析与验证在系统软件验证方面取得突破性进展。例如，在编译器方面，CompCert项目始于2005年，一直持续至今，形式验证了一个基本上符合ISO-C-90和ANSI-C标准的工业级的C语言编译器；操作系统形式验证方面的工作较多，比较有代表性的操作系统内核验证包括澳大利亚NICTA对seL4的验证、美国耶鲁大学团队对CertiKOS的验证、中国科学技术大学团队对μC/OS-II的验证等。seL4在美国国防部高级研究计划局（Defense Advanced Research Projects Agency, DARPA）HACMS项目实验中，作为无人机操作系统抵御了信息安全攻击。此外，还有对分布式系统的验证、安全系统的验证、文件系统的验证等。

当然，形式化方法更多的应用来自安全攸关的工业和国防等领域。例如在航天领域，美国航空航天局（National Aeronautics and Space Administration, NASA）有大批全球顶级形式化方法专家，其中喷气推动实验室（Jet Propulsion Laboratory, JPL）飞行软件团队使用SPIN模型检验器分析了火星科学实验室（Mars Science Laboratory, MSL）任务中多线程代码的竞争条件；在航空领域，人们通过形式验证发现了ARINC653 P1-3的6个功能安全问题；微软将SLAM作为微软驱动程序质量保证的常规工具；亚马逊已经将形式化方法大量应用于日常业务安全保证；谷歌也使用静态分析技术分析了其代码库等。

2国内研究进展

中国开展形式化方法研究工作较晚，基本是从1978年改革开放开始的。当时国内一批优秀学者被选派出国交流学习，他们迅速进入国际学术前沿，取得了一些具有重要国际影响的成果。例如，中国科学院院士唐稚松访问美国斯坦福大学后，在国际上首次提出可执行时序逻辑想法，并实现由性质规约自动生成代码的开发环境XYZ/E。中国科学院院士周巢尘访问英国牛津大学期间，同Tony Hoare一起解决了CSP的公理语义问题；20世纪90年代初，周巢尘院士和国际同行提出了时段演算理论，首次将连续数学概念引入计算机科学，开辟了实时系统形式设计新途径，成为实时系统形式设计的两个主流方法之一（另一个是时间自动机）。中国科学院院士李未为结构化操作语义建立作出了杰出贡献。中国科学院院士何积丰与Tony Hoare合作，提出统一程序理论（UTP），解决了不同程序模型和不同程序设计风范比较难题。中国科学院院士林惠民和国外同行合作，提出符号互模拟理论，解决了进程代数中一个重要公开难题，并实现工具。

进入21世纪后，国家对软件可信，特别是安全可靠的需求日益突出。以国家自然科学基金委员会“可信软件基础研究”重大研究计划为代表，给予复杂系统建模和验证研发大力支持，带动了中国形式化方法的快速发展，正在逐步缩小与国际同行的差距。在形式规约方面，中国科学院软件研究所团队在时段演算前期工作基础上，开发出结合AADL和Simulink/Stateflow组合图形建模，并与混成CSP构成图形与形式模型相互自动转换的层次建模；同时扩充传统霍尔逻辑到混成系统，建立混成霍尔逻辑作为信息物理融合系统性质规约逻辑，并建立基于交互式定理证明和可达集计算的验证技术，解决了安全攸关系统设计中的若干难题；开发的MARS工具已经在航空航天和高速铁路等系统得到应用。南京大学团队针对线性混成系统可达集开展了系统和深入的工作，开发的可达集分析工具BACH在国际上具有重要影响。国防科技大学团队长期从事抽象解释和符号执行等静态分析技术研究，取得了多项国际领先成果，开发的模型检验工具在国际程序验证竞赛中多次获得冠军。在程序验证方面，南京大学团队设计了针对并发系统的分离逻辑，并应用于并发操作系统验证，具有重要国际影响。北京航空航天大学团队也长期将形式化方法应用于航空嵌入式软件形式验证，发现了航空嵌入式软件标准ARIC 653中的许多错误，并确认。上海交通大学团队长期从事基于定理证明的C语言验证及相关编译器验证，在国际上具有重要影响。清华大学团队开发了针对C程序的模型检验工具，并成功应用于一些操作系统驱动的验证。中国科学院软件研究所团队也长期从事SAT/SMT及交互式定理证明工作，开发的SAT求解器，多次在国际SAT比赛各个赛道中获得冠军；开发的基于演绎的自动定理证明工具和交互式定理证明工具具有重要国际影响。北京大学团队在非线性约束求解方面取得了国际领先的成果，并和中国科学院软件研究所合作，解决了程序验证中的若干公开难题。另外，中国科学院软件研究所和上海交通大学在概率系统和概率程序验证方面的工作在国际上也具有重要影响。在面向国家需求的应用层面，中国航天部门和科研院所合作建立了结合形式化方法、覆盖软件研制全周期、以可信要素为核心的航天嵌入式软件可信保障技术体系以及相应的可信保障集成环境，并在“嫦娥”探月等重大工程软件的可信性保障中发挥了重要作用。

但是，整体看，中国形式化方法和国际同行相比落后明显。首先，目前形式规约、分析与验证的大研究方向基本是国际同行创立的，中国科研人员虽然在其中解决了一些理论和技术问题，但开创性工作仍然缺乏；其次，在形式化方法核心推理技术和工具引擎，例如以自动推理证明、高阶定理证明、高性能数学规划求解器等方面表现薄弱，也存在着被“卡脖子”风险，在一些重要的方向，例如函数式程序设计范型和语言环境方面工作较少；第三，有影响的工具不多，虽然国内近年开发了许多形式规约、分析与验证工具，但是缺乏系统性和引领性，没有形成合力，亟须实实在在解决国民经济和国防建设中的问题，核心关键技术对中国“缺芯少魂”基础支持远不能满足需求。此外，形式化方法作为一种渗透型的方法学领域方法，虽然在各领域的应用场景和应用空间丰富，但是在资助层面与国际上同类资助对比有不小差距。

3关键技术挑战

随着信息技术的高速发展，人类社会即将进入人机物融合时代，其基本特征就是软件定义一切、万物互联、人机物自然交互。在人机物融合时代，过去在封闭环境下运行的孤立系统通过网络连接，在开放环境下协同完成指定的任务。另外，人工智能技术的快速发展和广泛应用，使得系统更加智能，特别是人在回路的新型控制模式，使得系统可信性保证更加困难。同时，量子计算、生物计算、类脑计算等可能颠覆传统计算产业的新型计算模型不断涌现，这些模型能够成为现实仍旧需要突破各种理论和技术挑战，需要针对这些新型计算模型的形式规约、分析与验证理论和技术进行研究。

3.1 开放环境挑战

人机物融合时代，安全攸关系统的形态发生了显著的变化。传统的安全攸关系统是在封闭固定环境下工作的，其环境是确定的，设计环境与运行环境往往假设一致；而人机物融合的安全攸关系统是在开放多变环境下工作的，其环境具有非确定（Uncertainty）、难以完全刻画、设计环境与运行环境不完全一致等特点，甚至环境本身就是多变的。这使得人机物融合的安全攸关系统的安全保证成为了一个巨大的挑战。如何有效对开放环境下的安全攸关系统进行规约、分析与验证，以确保系统安全可靠，是计算机科学的一个重大挑战，需要新的系统设计理论和工程方法。

3.2 控制软件复杂性挑战

安全攸关系统的设计必须考虑环境与系统的紧耦合，并且包含了并发、分布和实时等特征，规约复杂度高。环境的开放性使安全攸关系统变得愈加复杂。首先，开放环境的不确定性和多变性要求安全攸关软件系统必须是开放的自适应系统。对自适应系统，“感知—判断—决策—动作”（Observation-Orientation-Decision-Action, OODA）是其适应环境的基本结构，并形成了多层次抽象的嵌套交叠，行为非常复杂；其次，由于一些场景难以显式建立规约，数据驱动的学习赋能部件成为系统的一部分，而学习赋能部件固有的不确定性和难解释性使得整个系统的规约成为了挑战；第三，安全规约必然是建立在环境和软件系统的模型上，环境的开放性和系统的复杂性也往往使安全性质的描述变得困难，需要研究在合适的抽象层次和恰当的角度上的性质规约方法。

3.3 新型计算模型挑战

后摩尔时代对计算极限的探索促使各种新型计算模型相继提出，如量子计算、生物计算和类脑计算等，这些全新研究领域给计算机理论带来新的挑战。例如，针对新型计算模型，显然过去针对Turing机模型，基于有穷自动机理论发展的各种程序设计语言和开发方法不再适用，需要新的程序设计语言及开发方法。同时，新型计算模型上如何保证安全攸关系统正确性和可靠性也是一个巨大挑战。例如，量子计算内在的不确定性使得量子程序验证比经典程序验证困难得多等。

4发展趋势与建议

4.1 发展趋势

1）仿真、测试、分析与验证等多种技术集成

仿真和测试技术目前仍旧是安全攸关系统设计实践中的主流技术，因为它们成本低、效率高、掌握容易。分析技术主要用于与系统运行相关度不高的性质验证，而形式验证主要用于对安全性要求高，可以承担高成本的系统或者子系统。即使是形式验证，如上所述，针对不同性质和需求，也可能需要运用不同验证技术。而对于复杂安全攸关系统的设计，必须综合运用各种技术。如何将这些技术集成，形成合力保证复杂系统可信性是一个挑战，也是发展趋势。

2）符号计算和数值计算融合

传统分析和验证主要基于符号计算。符号计算的优点是精确，没有误差，但缺点是效率太低，求解能力有限；相对而言，数值计算效率高，能够对很多理论不可解问题给出近似解，但是缺点是有误差，正确性难以保证。近年，如何建立基于数值与符号混合计算之上的形式分析与验证技术，从而克服符号计算和数值计算的各自缺点，发挥各自优点，是计算机科学和数学共同关注的挑战性问题，已经成为一种趋势。

3）定性和定量相结合

传统上，形式分析与验证基本上是针对定性性质，因而效率和规模一直是个瓶颈。而近年，随着系统功能变得越来越复杂，系统规模越来越庞大，特别是人工智能技术的广泛使用和人在回路的新型控制模式，使得定性分析与验证不可能，也没有必要。相反，人们发现很多实际系统没有必要保证绝对正确性，能够给定概率意义下的正确性即可。特别是一旦把定性需求放松为定量需求，分析与验证的效率和规模就会呈多个数量级提升。但是如何在设计安全攸关系统中区分定量需求和定性需求，以及开发更多定量需求分析与验证技术是一个挑战，也是一种趋势。

4）构造即正确

传统上，安全攸关系统的设计和分析与验证是分开的，系统设计者设计并开发系统；独立团队形式分析与验证系统的可信性。而理想情况应该是这两者的有机融合，即系统合成（System Synthesis）或者程序合成（Program Synthesis），这被认为是计算机科学的“圣杯”。但是，这个问题因为挑战性太大，过去被认为是不可能解决的，因而不被重视。但是近年，因为验证成本和难度的增长大大超出人们的想象，人们重新尝试在特定领域实现构造即正确，并取得一定成功，特别是在嵌入式系统领域。这使得将构造即正确应用于更多特定领域成为一种趋势。

4.2 发展建议

1）增强复杂关键软件技术的源头创新能力

进入数据经济时代，软件定义一切并成为了社会发展的基础设施，泛在、高效、可信对复杂软件建模和验证提出了新要求。数据驱动特征不断融入复杂关键软件，软件理论和技术迎来了新赛道，迫切需要在形式化方法理论和技术上有创新和突破。建议加强形式化方法基础研究，关注大数据带来的数据驱动软件建模和验证的新特征与新挑战，加强形式化方法基础研究，在数据与机理融合复杂关键软件方面创新建模和验证理论，形成一批源头创新和变革性软件新技术。

2）增强复杂系统建模和验证工具链的供给能力

工具软件是中国复杂关键软件的关键核心技术，也是自主可持续发展的瓶颈。虽然有了一些工具和成果应用，但是从系统性、先进性、可用性等方面，复杂系统工具链距离国家对软件的重大需求还有很大差距。需要充分利用体制和机制优势，加强顶层设计，充分适应复杂系统成长、演化需求，集中力量协作攻关，产出一批复杂系统建模和验证工具链，基于开源生态和应用推进两方面，切实增强国家软件工具链的供给能力。

3）加大人才培养力度，推动学研用产融合创新持续发展

复杂系统建模和验证，特别是形式化方法面临着通识培养薄弱、专业人才短缺的问题，使得门槛高、推广难问题突出。要加强人才培养力度，一方面从形式化思维的角度加强通识能力的培养，构建系统建模和验证的基本能力和素质；另一方面，将形式化建模和验证的专业知识下沉到本科教育，形成规模化的专业人才群体。同时，实施学研用产联合攻关，融合创新，探索人才培养的新途径，形成研究、工程、应用等各层次人才合理的创新队伍。

5结束语

形式化规约、分析与验证对于确保安全攸关系统正确性和提高可信性具有基础性的作用。形式化规约、分析与验证的应用已经取得了长足的进展，已经成为安全攸关系统设计的各种国际标准推荐的关键技术，也是解决中国“缺芯少魂”的核心技术之一。为了解决这个问题，中国应该加强形式化规约、分析与验证等方面的基础研究，长期固定支持相关工具开发，形成具有知识产权和国际影响力的系列工具，并应用于一些关键领域，服务国家创新战略和发展。

END

关于本刊

《前瞻科技》是由中国科学技术协会主管，科技导报社主办、出版的科技智库型自然科学综合类学术期刊，于2022年创刊。

办刊宗旨：围绕国家重大战略任务、科技前沿重要领域和关键核心技术，刊载相关研究成果的综述和述评，促进学术交流，推动科技进步，服务我国经济社会高质量发展。

常设栏目有“前瞻”“综述与述评”“聚焦”“论坛”“文化”“书评”等，其中“前瞻”“综述与述评”为固定栏目，其他为非固定栏目。

期刊官网：www.qianzhankeji.cn