形式化方法对软件开发的挑战：一些历史与现实

几年前到某著名大学参加学术活动，无意中听到该校两位老师闲聊，现在还记得的一句话就是“形式化方法已经不行了”。看来真是隔行如隔山，不在一行里的人做评价，而且信口开河，难免出错。在关注形式化方法的人看来，它不仅没有“不行”，近年还发展得挺迅猛。只不过，形式化方法也就是做软件或硬件，并没有做出什么新东西，很难像近来热炒的云计算、大数据、人工智能那样，被疯狂追捧。

一些情况说明，不少计算机（包括软件）专业人士对形式化方法的认识还停留在几十年前。这里想介绍一些事例，说明形式化方法已经取得了真正的进展，正在被人们用来解决软件开发中一直没有解决的问题，也实际开发了一些重要系统或系统部件。

较早开展的与实际软件开发有关的形式化工作是证明程序正确性，工作以论文形式发表，内容是证明了一些小程序或算法（抽象程序）。研究者也想去证明复杂程序，但由于其中的复杂结构和设计，很难做下去。这种想法也因此被人诟病为“只能对付小程序”，没用。

一些研究者想到，证明已有程序很难，而构造具有所需功能的正确程序（或软件），更多方面可以自主控制，可以采用构造与证明并进的方式，目标是做出“构造即正确”的软件。最早提出这方面想法的人可能是Dijkstra，其著名的A Discipline of Programming给出了许多严格推导的程序。后来还有些类似著作，如The Science of Programming、Programming fromSpecification等。这些工作流行于上世纪80-90年代，由一批著名计算机科学家推动，但这类方法并未受到软件领域的重视，主要批评还是说只能做“玩具程序”。

用形式化技术开发实际系统的最早突破可能是法国Abrial的B方法。据Abrial自己说，他在牛津开发了Z语言后觉得这种想法可以用于实际软件领域，回法国后开发了B方法。B方法支持从系统抽象规范描述到代码生成（生成C或Ada代码）的整个开发流程，现在已有工业强度的开发工具（包括证明工具）。B方法的开发就是为了用于实际，其最早的应用案例是开发了巴黎地铁的信 系统和一些控制系统，包括巴黎地铁14 线的自动驾驶系统等。具粗略统计，目前全世界有数十条地铁线路的自动驾驶系统是用B方法开发的。B方法也被应用于其他安全攸关领域，如铁路、汽车和航空等领域。用B开发生成的控制系统可能大到数十万行的目标代码。我国从欧洲引进的高铁系统和设备中，有一些就是用B方法开发的。Abrial曾在2006年国际软件大会（在上海展开）做过有关“形式化方法的工业应用”的特邀 告，其著作The B-Book介绍了B方法。他与华东师大有长期合作，2016年被中国政府授予国际合作奖。Abrial曾告诉笔者，用B方法开发的（某个）系统在测试中没发现任何错误。对常规软件开发技术，这是根本不可能出现的情况。

形式化方法在系统软件开发领域也取得了许多成果。这方面最重要的成果之一是CompCert编译器。编译器显然是最重要的系统软件，目前正在运行的绝大多数程序都是编译器生成的。但是，常用编译器都没经过验证，并不保证目标代码与源代码语义一致。2012年法国研究者发布了经过验证的优化编译器CompCert，后不断增加功能。目前版本能处理ANSI C几乎所有特征和一些C99扩充，能生成PowerPC、ARM和X86代码，支持64位系统结构、分别编译和连接，能生成DWARF调试信息和语法错误的解释等。CompCert基于计算机辅助证明系统Coq开发，严格证明了目标代码与源程序的等价性。X. Yang等人的论文Finding and Understanding Bugs in C Compilers（PLDI 2011） 告了他们用6年时间检查各种在用编译器（包括VC、gcc等）错误的工作，只有当时版本的CompCert验证过的部分没发现错误，其他广泛使用的编译器都发现了错误。

近年的另一有趣工作是2015年MIT学者开发的经过验证的文件系统FSCQ（SOSP 2015），可以保证在使用中任何时候系统崩溃，系统重新boot都能正确恢复，不会丢失数据（称为crash safety）。常规的文件系统并没有这种保证。

美国国防部的HACMS项目（High-AssuranceCyber Military Systems，高可信军事 络系统）的目标是开发高可信、黑客无法入侵的军用系统。该项目的一个成果是一个无人机控制系统，开发成功后组织白帽黑客攻击，没被攻破。该系统的基础是经过形式化验证的OS内核seL4，在该内核上用Isabelle形式化工具开发和验证整个系统。HACMS项目的另一成果是邵中领导开发的经过验证的支持多核CPU的操作系统内核CertiKOS（OSDI’16）。

显然，上面这些例子都是很重要软件，而且是很难做的软件。这些工作的完成，说明形式化方法确实能用于做软件，而且能做出最高质量的重要软件。

形式化开发的工作过程与常规软件开发有类似之处。B方法基于一阶逻辑和集合论，其开发过程从高层规范开始，基于一种严格定义的精化（refinement）概念，可看作是软件领域中重要的自上而下开发方法和程序设计的逐步求精方法的严格化。另一方面，上面说到的好几项工作都是用Coq系统开发的，包括CompCert、FSCQ和CertiKOS，其中CertiKOS的开发中还使用了CompCert，系统的大部分是经过验证的C代码，用CompCert编译到汇编。这些工作的开发流程基本是自下而上，逐个（逐层）构造所需软件概念和部件，最终得到整体的软件。当然，最关键的特征就是开发与证明携手并进。

特别值得提出，CertiKOS是一个操作系统内核体系结构，可用于开发实际的操作系统。OSDI’16论文中 告的一个具体系统只用了两个人年，这一效率十分惊人。对形式化软件开发的另一重要质疑是成本，CertiKOS可看作一个证据，说明情况可能并不悲观。

形式化开发的工作在国内也有些进展，例如王生原领导的小组开发了从同步流语言Lustre到C语言的经过验证的编译器，可以通过CompCert接力，生成可执行代码。Lustre是国际上开发控制系统使用很多的语言，特别是在核电领域。这一工作结果也已成为国内某核企业的重要工具。此外，上海一些开发团队也在做轨道交通方面应用系统的形式化开发。笔者没有下功夫去收集这方面的信息，恳请有关专家自己补充。

当然，软件形式化开发还处在起步阶段，许多问题尚未研究。对于形式化软件开发方法本身，一个重要问题是正确性的组合和传播：如何严格保证由证明正确的部分构造出的系统仍然正确，即使这些部分是基于不同方法构造出来的。作为与常规方式不同的另一种软件质量保证手段，形式化方法将怎样与常规开发方法相互作用多事情都还不清楚。但无论如何，这方面工作已经取得了实质性进展，并已开始在实际领域发挥作用。

可以认为，以B方法和CompCert等软件的出现为标志，形式化软件开发方法实实在在地进入了实际软件系统开发的领域。今后我们会看到越来越多的经过严格证明的软件系统或者系统部件。另一方面，有些用户也可能要求经过证明的系统。回顾一下各种重要的软件规范标准，其最高级别的质量保证都要求形式化方法，有些作为选择性要求，，只是因为撰写时还缺乏实践基础。下一版的标准将会怎样些标准强制性地要求严格证明，不是不可能出现的情况。这些都要求我们及早做好准备。