形式化方法的研究进展与趋势

2018 年 11 月 8 日 中国计算机学会

CCF于2018年10月出版了新一期《中国计算机科学技术发展报告》，对AI与系统软件的深度融合等10个方向的研究进展做了详细的介绍和讨论。我们将分期分享报告中的精彩内容。请加入CCF，登录CCF数字图书馆下载和浏览。

1 引言

随着信息技术的广泛应用，特别是信息技术与物理世界和人类社会的高度融合，整个社会的信息化程度不断提高，人们对计算机系统的可靠性与安全性提出了更高的要求。计算机系统的一个小小的错误或者安全隐患可能影响到国家安全或者人民群众的生命财产安全。

形式化方法是保证计算机系统正确性与安全性的一种重要方法，其采用数学（逻辑）证明的手段对计算机系统进行建模、规约、分析、推理和验证。

形式化方法是计算机科学的一个传统研究方向，迄今为止，共有12位学者因为或者部分因为形式化方法的研究工作而获得图灵奖。形式化方法是一个基础性和交叉性很强的研究方向，它与计算机科学的其他分支，比如计算理论、编程语言、软件工程、计算机安全等都密切相关；同时，近年，与生物信息、控制理论、电子自动化设计等多个学科交叉明显。

形式化方法越来越受到国际/国内计算机学术界的重视，比如国际组织IFIP下面有至少三个工作组（Working Group）与形式化方法相关，欧洲有专门的形式化方法组织FME，美国计算机学会（ACM）在2014年成立了SIGLOG，即逻辑与计算专委会 (Special Interest Group on Logic and Computation)，涵盖计算逻辑、自动机理论、形式语义、程序验证等方向，而中国计算机学会则在2015年成立了形式化方法专业组，今年刚刚正式更名为形式化方法专业委员会。

形式化方法方面的国际旗舰会议包括：关注形式化方法的理论基础的LICS（LogicIn Computer Science）、关注形式化方法的理论和应用结合的CAV（Computer-Aided Verification）和FM（International Symposium on Formal Methods）、关注自动推理的IJCAR（International Joint Conference on Automated Reasoning）等。

由于形式化方法在保证计算机软硬件系统的正确性和可靠性方面的有效性，它已经被许多国际标准化组织列为保证安全攸关系统必备的技术手段。例如，国际航空软件标准DO178B、DO178C中明确要求开发安全可靠航空软件必须使用形式化方法；又如，在软件安全等级SIL1-4中，安全级别最高的SIL3和SIL4要求必须使用形式化方法。而且，形式化方法已经逐渐为IT产业界所接受和采纳，例如

•微软开发了一系列影响深远的形式化验证工具，比如Z3、Dafny、F*、SLAM等，用于对其开发的众多软件的正确性进行分析，

•Facebook将基于分离逻辑的验证工具Infer广泛用于其Android应用的开发过程中，

•Amazon在2014年成立了自动推理组，用SMT求解器去验证其Web服务的正确性，

•国内的华为公司最近建立了形式验证团队，使用定理证明辅助工具来验证操作系统内核的正确性和安全性。

形式化方法使用数学（逻辑）证明的手段对计算机系统进行建模、规约、分析、推理，其主要涵盖以下几个研究方向：

•定理证明：对逻辑推理过程进行研究，尽可能提高逻辑推理过程的自动化程度；

•形式模型：对形式模型的理论性质和各种判定问题进行研究，提出高效的判定算法，并开发原型工具；

•形式语义与形式建模：为了对计算机系统的行为进行推理验证，需要对编程语言的语义进行严格的定义，使用形式模型对计算机系统的行为进行建模；

•形式规约：为了对计算机系统的行为进行推理验证，也需要对程序行为所满足的性质用某种形式语言（逻辑、自动机等）进行严格地定义；

•形式验证技术与方法：在形式语义/形式建模以及形式规约的基础上，将计算机系统的分析与验证问题转化为逻辑推理问题或者形式模型的判定问题，用定理证明工具/求解器或者某个形式模型的原型工具来进行验证；

•形式验证工具以及应用：基于形式验证理论、方法和技术上的研究成果，开发自动形式验证工具并在工业级系统中进行应用；

•量子程序分析与验证：针对量子程序的特点发展其分析与验证理论、方法、与工具。

本报告将对形式化方法的最近5年的国内外研究进展进行一个相对全面的介绍，并对发展趋势进行展望。

2 国内外研究进展比较

2.1定理证明

交互式定理证明在国内的起步较晚，一直到2000年以后，清华、华师大等相继举办Coq暑期班，它在国内形式化方法领域才逐渐得到推广应用。国外对于交互式定理证明的理论技术和应用两方面都进行研究，而国内主要集中于交互式定理证明在形式化领域的应用研究。近年来，由于安全攸关软件的发展需求，国内关于交互式定理证明在系统验证等方向的应用研究明显增多，也取得了一些显著的成果，但距离国际领先水平仍存在些许差距。

国内外对SMT的研究，大致是国外起步较早，研究成体系，技术比较成熟。国内的研究起步较晚，但是在某些特定的研究方向上有一定优势。SMT在国外的发展有很长的历史，主流的求解算法均产生在国外的研究机构。欧美的一些大学和科研机构成立有专门的SMT研究组，并开发出一系列成熟的求解工具。最具影响力的SMT求解器Z3、CVC4，其中微软在很长一段时间内处于领先地位。

相对来说，国内专门研究SMT的研究组较少，只有中科院、清华等少数科研院所和高校的科研人员从事这一研究。就研究内容而言，国内的研究工作重点放在一些新兴方向上面，所研发的求解器支持的理论较少。

2.2 形式模型

关于概率自动机模型的研究，绝大多数活跃在国外，国内对于概率自动机模型的研究尚还不够重视，活跃在这一领域的学者还是太少。一方面，我国概率模型检测的起步相对落后于西方，从2010年以后才陆续出现我国学者在这一领域发表成果，另一方面概率自动机模型的研究往往是跨学科跨背景的，需要一些背景知识和研究经验。不过令人欣喜的是，近些年来越来越多的中国学者在这一方向有所成果，我们也能时常在这一领域看到中国学者的名字。我们在概率自动机以及概率模型检测方面的脚步，已经有追赶上国外的趋势。纵观这一领域，某个重要的定义或者重要领域的发现和开发往往源于西方，而我国学者在之后能做出相当多的成果，这表明现在国内已经具有研究概率模型检测的能力和实力，但在创新性方面表现略显不足。

总体来讲，国内在混成自动机模型的研究方面处于国际前沿，与美国和欧洲等处于同一水平。近年来，中科院软件所、华东师范大学、南京大学、北京航空航天大学等团队在混成系统建模、验证、分析和设计等方面取得多项具有国际影响的成果，例如：中科院软件所詹乃军等解决了半代数集成为多项式混成系统不变式的充要条件问题，首次提出了时滞混成系统形式验证问题等；北航佘志坤等提出基于数值求解的混成系统可达集高效计算方法等。

在无穷状态并发系统模型的研究中，国内的研究进展与国外几个顶级实验室进展速度相当，多方之间在友好竞争当中，获得了越来越多的成果。

2.3 形式语义与形式建模

目前国内程序语言形式语义研究人员相比国外程序语言研究者偏少，研究力量不足，归其原因是这方面的工作比较基础和冷门，入门门槛高且就业难。

在操作语义和指称语义方面，国外大部分对工业级程序语言的语义进行研究，语义通常会在定理证明器或K框架中实现，实现的语义会进行测试并用于程序的分析和验证；语义的研究不仅仅为了更好地理解程序语言，而是为了更好的对程序进行分析和验证。与之相反，国内程序语言的语义研究，主要（除Rust外）是针对一些学术性语言，还停留在形式语义研究初期的目的，即为了更好的理解程序语言，而非对这些语义进行应用。

尽管国内形式建模方面的研究在近五年有较为快速的发展，也有大量的论文发表，然而与国外研究相比，国内的研究多是在国际上提出的形式模型的基础上，做一些扩展性研究工作，缺少原创性工作。另外，与国外许多相对成熟的建模与验证工具相比，如SPIN^[228]，PAT^[229]，K框架^[190]，UPPAAL^[211]等，国内开发的形式建模工具多是已有工具的扩展，缺少独立开发的原创性工具，导致在国际上的影响较小。

另一方面，形式化方法作为解决工业应用领域系统安全可靠性问题的重要技术，在国内缺少比较有影响力的成功案例。国际上，有很多有影响力的案例使得产业界对形式化建模与验证有足够的重视，如Event-B曾成功用于巴黎地铁的设计与开发^[205]，Amazon也将TLA+用于Webservice的设计与开发^[230]。然而，国内产业界由于形式化方法过于抽象，扩展性等问题，对形式化的重视力度不够，在系统的实际设计与开发过程中未充分发挥形式化方法的作用，缺少具有影响力的成功案例。

2.4形式规约

国内从事形式规约的研究人员不多，目前流行的形式规约语言，比如分离逻辑、时序逻辑等，基本是国外的研究人员提出来的。国内研究人员在形式规约语言的研究工作集中在对已有规约语言的理论性质（比如表达能力和判定算法）的探讨上。国内研究人员最近5年在分离逻辑和时序逻辑的各种扩展上开展了较深入的工作，总体来讲较以前有所进步。

2.5 形式验证技术与方法

与国际研究现状相比，国内在基于演绎推理的验证技术方面工作相对较少，特别是在新型验证理论和程序逻辑方面的工作相对较少。关注的程序性质主要集中在功能正确性方面，对于其他性质，如信息流控制等安全性的验证工作较少。在并发程序精化验证方面，特别是并发程序的活性验证方面的工作处于国际领先的地位。

我国在实际系统方面的验证工作较为活跃，但很多工作集中在模型和算法层面，对于代码的验证工作相对较少。与国际同行相比，验证的系统的规模和影响力上面有所欠缺。

近年来，国外在抽象解释的理论、方法、工具等方面形成了许多有影响力的成果，形成了较多有影响力的开源和商业化的有效工具平台，并且有些工具在工业界取得了成功应用。国内在新型抽象域的设计与实现、特定领域应用（如中断驱动型程序的分析）方面研究形成特色。然而，国内在基于抽象解释的程序分析工具研发、产业影响等方面还与国外存在一定差距，相信随着国内软件可信需求的不断提升，差距会不断缩短。

在模型检测方面，近年来，国外在软件形式化验证的理论、方法和技术等方面产生了大量有影响力的成果，形成了许多高效的软件形式化验证工具。国内在特定领域的研究形成特色，已经达到国际领先的水平，如国防科技大学研发的并行程序验证工具Yogar-CBMC等。

在符号执行方面，总体而言，国内在符号执行各个方面的研究正逐渐与国外接轨，包括理论、方法与工具等，国内相关研究学者的工作也能发表在主流的符号执行相关的国际会议或期刊上，这些工作也引起了国外学者的注意，同时与国外相关学者的交流与合作也越来越多。然而，国内在符号执行的工具和平台的开发、产业影响方面还与国外存在一定差距，相信随着国内软件行业自主可控需求的不断提升，这部分的差距会不断缩短。

2.6 形式验证工具以及应用

近10年来，国外在软件形式化验证的理论、方法和技术等方面产生了大量有影响力的成果，形成了许多高效的软件形式化验证工具。国内在软件形式化验证工具开发方面起步较晚，通用工具的研发与国外仍存在较大差距。然而，国内在某些特定领域的研究形成特色，已经达到国际领先的水平，如国防科技大学研发的并行程序验证工具Yogar-CBMC等。

在混成自动机验证工具方面，国内外研究各有侧重与特色。国内工作在混成系统定理证明，线性混成自动机有界验证等领域上处于国际领先地位。而国外近年来则在非线性混成自动机有界可达性检验方面取得系列进展，开发了以Flow*，SpaceEx等为代表的系列工具。

2.7量子程序分析与验证

从量子程序的分析与验证来讲，国内与国外基本处于同一水平，国内中科院软件所应明生教授团队在量子程序的分析与验证方面处于国际引领地位。

3 发展趋势与展望

3.1定理证明

定理证明本质上可以看作一个证明搜索问题。由于一般使用的逻辑的不可判定性，一个能够高效率地解决所有证明问题的算法是不存在的。因此启发法（heuristics）的使用尤其重要。目前交互式定理证明里的自动化在一般情况下还远远不及人类的能力，其中主要问题是人在证明中使用的有目的的搜索还无法在计算机上实现。机器学习，尤其是深度学习的方法为实现这种有目的的搜索提供了新的希望。[34]首次把递归神经网络运用到定理证明问题上。在这项工作中，机器学习被用于使用自动定理证明器之前筛选已有定理（premise selection），但没有用于指导证明搜索本身。对使用各种机器学习方法指导证明搜索本身也开始有一些研究，比如 [36, 37, 38]。使用机器学习的一个主要问题是如何获取大量的可供学习的数据。现在使用的一些主要的数据库来自Mizar和HOL Light，各包括几万个定理。更大的数据库还有待建立。除了定理证明本身，机器学习也开始应用于非形式化数学到形式化数学的自动转换^[35]。

当前基于DPLL(T)框架的主流SMT求解技术已经趋于成熟，但尚不能完全满足现实应用的需要，在一些特定的发展方向上仍有很大的研究空间，包括SMT的扩展问题、非完备求解算法等。

SMT本身为判定问题，但科学研究和现实世界中的很多问题不仅关心解的存在性，而且要进一步探寻最优解，乃至解空间的大小，因此对SMT问题类型的扩展近年来引起了国际学界的重视。上文所提到SMT解计数问题即是一个重要的SMT扩展问题，在程序分析与验证、近似推理等领域有广泛的应用前景。另一个热门的扩展方向是将SMT由判定问题扩展到优化问题，即优化模理论（Optimization ModuloTheories）。优化模理论问题旨在求出满足SMT约束的最优解，在实际应用中很有意义。目前代表性的研究来自于意大利Trento大学^[68,69]。

作为一个SMT求解的完备算法框架，DPLL(T)虽然已取得了巨大的成功，但本质上是基于回溯框架的指数级复杂度的算法，其求解效率难以持续突破，在求解规模上很受限制。近年来，在SAT领域，基于局部搜索的SAT算法在工业化的例子上取得了较大成功，与基于CDCL的完备算法形成了并驾齐驱的局面。在SMT领域，当前已有非完备的SMT求解算法出现，主要用于BV理论。非完备算法在设计上具有灵活性，并对问题的规模不敏感，会是将来SMT求解算法的一个发展趋势。

3.2 形式模型

概率自动机模型不仅在概率模型检测上有重要的理论价值和应用场景，它在概率程序语义和验证[91, 99]、随机算法[115, 72, 105]、甚至机器学习领域^{[74, 102]}都有着广泛的应用。这表明，概率自动机模型不仅在形式化验证领域是一个有研究价值的热门话题，在计算机的其他领域，甚至于数学、物理、生物、医学等其他自然科学领域，也都有着相当的研究前景。包括概率自动机模型及其相关理论、验证问题和应用都有广泛的研究空间和很高的研究价值。经过了近三十年在概率模型检测的研究，其理论基础已十分坚实，很多重要问题已经得到解决，但同时不乏一些重要的公开问题（如PCTL公式可满足性的判定问题）仍然存在。这一领域仍有很多虽然看起来不大却依然重要的问题有待解决和开发，同时该领域与计算机科学其他领域及其他自然科学的结合也必将成为新的研究方向。

混成自动机模型的研究取得了一定的进展, 但仍有许多问题亟待解决。未来5年混成自动机模型的研究将集中在以下几个方面：随机和概率混成系统的形式验证，时滞混成系统的形式验证，大规模非线性混成动态模型的形式验证，开放动态模型的行为预测与验证。

无穷状态并发系统模型研究方面取得了很大的进展，有关强互模拟的判定问题大部分已解决，而当允许内部迁移时，互模拟的可判定性结果很少。所以着重解决2.2节的表中列出的悬而未决的公开问题，是本领域的趋势。因为这些问题长期公开，因此可见，用已有的证明方法很难得到结果，如何开发新的证明方法，是这一领域的关键所在。

3.3 形式语义与形式建模

从目前国内外程序语言语义的研究来看，未来程序语言语义的研究将针对工业级的程序语言，而非学术性无实际应用的语言；语义研究的目的也不在仅仅为了更好的理解程序语言，而是为了更好的对程序进行分析与验证。

另一方面，多年前就寄望于程序语言设计者在设计语言时就对程序的语义进行形式化定义的问题尚未解决。虽然在学术性程序语言提出时，设计者会给出其形式语义。但是对于工业级程序语言，比如C、Rust和Go，设计者都没有定义形式语义，甚至没有完整的形式化语法定义。主要原因是工业级程序语言相对复杂，语义的定义困难，具备这方面能力的工业界人员少，也没有易用的语义开发框架。

新型计算系统如大数据系统、人工智能系统、无人驾驶系统等的出现为形式建模技术的发展带来新的机遇和挑战。系统的智能性、实时性、空间离散性等特征对系统的安全性和可靠性提出更高的要求，迫切需针对这些系统的特性发展新的建模理论、方法和工具，这将成为形式化方法领域研究的热点问题。然而随着系统的复杂性越来越高、特性越来越多，很难定义一种统一的建模方法来完整地描述系统的所有特性。如何在模型的表达能力与验证问题的可判定性及复杂度等方面做出取舍，都是非常具有挑战性的工作。

3.4形式规约

新的计算模式，比如大数据、机器学习算法等，不断涌现。这些计算模式下的程序的行为与经典的串行和并发程序非常不同，需要设计新的规约语言以及分析验证方法与技术。针对这些新的计算模式的形式规约语言将是今后5年左右的研究热点。

3.5 形式验证技术与方法

近年来，伴随着云计算、人工智能等各种研究热点，在相关领域中开展的验证也越来越得到人们的重视。在云计算和分布式系统验证方面，逐步出现了一些对分布式算法和系统的验证工作^[303-304]。但其中对分布式数据一致性协议和算法的验证尚处于起步阶段，国内外相关工作较少。

人工智能算法和演绎推理技术的结合是另外一个很有发展前景的方向。国内外已经有了初步的采用模型检测或者其他技术来对人工智能算法进行验证的工作，但基于演绎推理的验证工作较少。这里的主要困难在于，基于演绎推理的验证技术需要对正确性有形式化定义（什么是正确），同时验证过程本身要求明确验证对象工作的原理（为什么正确）。而以上这两点在人工智能研究领域尚未有明确答案。

未来，抽象解释技术将进一步在新的架构、语言、应用等实际需求驱动下不断发展，值得关注的方向包括对弱内存模型的分析验证^{[335, 322]}、神经网络的分析与验证^[339,364]、大数据处理相关错误的分析^[353]、Python程序的自动分析^[338]等。与约束求解、自动推理、人工智能等基础支撑技术的紧密结合^{[358, 350,328,341,357]}，将是抽象解释后续研究趋势之一^[333]。同时，降低误报率将依然是基于抽象解释的程序分析技术拓展实际应用的研究挑战和重点。

在模型检测部分，我们主要侧重于一般软件代码近年来相关验证工作的介绍。在此之外，近年来相关领域关注热点进一步拓展到针对多线程代码验证，对递归等特定类型程序验证，对领域相关代码验证等。在此之外除了上述安全性（Safety）／可达性验证（Reachability）之外，软件代码的活性（Liveness）／可终止性（Termination）验证也是近年来关注热点所在。

在符号执行方面，符号执行技术将进一步在软件工程、安全、系统、网络等相关领域的实际需求驱动下不断发展；面向大规模软件的高效符号执行方法、技术和工具将是下一步的研究挑战和重点；同时，符号执行搜索策略的更加智能化也将是下一步的研究重点；此外，与其他技术在不同层面的密切结合，以进一步提高软件分析效果，也将是符号执行后续的研究趋势之一。

3.6 形式验证工具以及应用

软件形式化验证面临严重的状态空间爆炸问题。软件形式化验证工具研发的一个重要趋势是多技术融合。利用形式化方法的严格性和其他技术的可伸缩性，力求在验证规模和验证精度上达成协调和统一。

混成系统由于其行为离散、连续交织非常复杂，难以掌握与控制，现阶段可进行有效分析的系统种类和规模仍有一定限制。当前主要关注问题包括大规模组合非线性混成系统验证、开放动态系统行为预测与验证、概率随机行为建模与验证、混成系统控制生成以及混成系统测试生成等。相关领域科研人员力图在上述问题上取得突破，力图对实际系统规模问题具备分析能力，从而保障相关系统运行安全。

3.7量子程序分析与验证

总的来说，虽然量子程序的分析与形式化验证领域已经取得了一些可喜的进展，但目前的研究还非常零散，很多问题甚至还不清楚如何准确定义。这大体上有两方面的原因：一、尽管最近几年量子硬件设备的物理实现取得了长足的进展，但距离能够运行真正实用的量子程序的通用量子计算机仍然非常遥远。因此绝大部分传统计算机科学家和程序设计和验证的专家还持观望态度，并没有对这一领域给予足够多的重视；二、由于量子程序和传统计算机程序相比具有很大的不同，特别是由于量子叠加和纠缠的存在，量子程序的验证往往非常困难。但是，我们有理由相信，量子程序理论和验证的研究将会吸引越来越多计算机科学家的关注，从而带动这一领域蓬勃发展。

4 结束语

形式化方法是计算机科学的传统研究方向，其涵盖很多不同的研究方向。本报告对形式化方法的各个方面的近5年的研究进展进行了相对全面的总结，对发展趋势进行了展望。希望本报告能够让计算机科学与技术的其他领域的研究人员和IT产业界的从业人员更好地了解形式化方法这个学科的内涵、外延、以及国内外研究现状，促进形式化方法跟其他领域的交叉融合，促使形式化方法在IT产业界得到更多应用。

作者简介