形式主义研究方法，形式化方法的特点

CCF于2018年10月出版了新一期《中国计算机科学技术发展报告》，详细介绍和讨论了AI与系统软件的深度融合等10个方向的研究进展。

我们分期分享报告的精彩内容。

请加入CCF，登录CCF数字图书馆下载并浏览。

1引言

随着信息技术的广泛应用特别是信息技术随着物理世界和人类社会的高度融合全社会信息化程度的不断提高人们对计算机系统的可靠性和安全性提出了更高的要求

计算机系统的小失误和安全隐患，可能会影响国家安全和人民群众的生命财产安全。

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

形式化方法是计算机科学的传统研究方向，迄今已有12位学者因形式化方法的研究而获得图灵奖。

形式化方法是基础性和交叉性较强的研究方向，与计算机科学的其他分支如计算理论、编程语言、软件工程、计算机安全等密切相关； 同时，近年来与生物信息、控制理论、电子自动化设计等诸多学科的交叉较为明显。

形式化方法越来越受到国际/国内计算机学界的重视。 例如，在国际组织IFIP下至少有三个工作组( Working Group )涉及形式化方法，欧洲有专门的形式化方法组织FME，美国计算机学会) ACM )于2014年成立了SIGLOG。 即逻辑与计算专业委员会( specialinterestgrouponlogicandcomputation )涵盖计算逻辑、自动机理论、形式语义、程序验证等方向，而中国计算机学会将于2015年成立形式化方法专业小组

形式化方法国际旗舰会议包括关注形式化方法理论基础的逻辑计算( LICs )、关注形式化方法理论与应用结合的计算机辅助验证( CAV )、 FM ) internationalsymposiumonformalmethods )，关注自动推理的IJcar ) internationaljointcoods )。

形式化方法在保证计算机软硬件系统的准确性和可靠性方面很有效被许多国际标准化组织列为保证安全关系系统的必要技术手段。

例如，国际航空软件标准DO178B、DO178C明确要求开发安全可靠的航空软件必须使用形式化方法，并且对软件安全等级SIL1-4有最高的安全级别

而且，形式化的方法越来越被IT产业界所接受和采用。 例如

微软开发了Z3、Dafny、F*、SLAM等影响力较大的形式化验证工具，用于分析开发的许多软件的正确性。

•Facebook在安卓APP开发过程中广泛使用基于隔离逻辑的验证工具Infer。

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

国内华为公司最近成立了形式验证小组，利用定理证明辅助工具验证了操作系统内核的正确性和安全性。

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

定理证明：研究逻辑推理过程，尽量提高逻辑推理过程的自动化程度

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

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

形式规约：为了推论验证计算机系统的举动，也需要用某种形式语言(逻辑学、自动机等)严密地定义程序的举动所满足的性质

形式验证技术和方法：基于形式语义/形式建模和形式规约，将计算机系统分析和验证问题转化为逻辑推理问题或形式模型判决问题，并通过定理证明工具/求解器或某形式模型原型工具进行验证；

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

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

本文对形式化方法近五年来国内外的研究进展进行比较全面的介绍，并展望发展趋势。

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]，亚马逊也将TLA用于web服务的设计和开发[230]。

但国内产业界由于形式化方法的抽象、可扩展性等问题，对形式化重视不够，在系统的实际设计和开发过程中形式化方法的作用没有充分发挥，缺乏具有影响力的成功案例。

2.4格式条款

国内从事形式规约的研究者很少，目前流行的形式规约语言，如分离逻辑、时序逻辑等，基本上都是国外研究者提出的。

国内研究者将形式规约语言的研究工作集中在对现有规约语言的理论性质(如表达能力和判定算法)的探讨上。

国内研究者近5年在分离逻辑和时序逻辑的各种拓展上开展了深入的工作，总体上比以前有了进步。

2.5格式验证技术和方法

与国际研究的现状相比，国内在基于演绎推理的验证技术方面的工作相对较少，特别是在新的验证理论和过程逻辑方面的工作相对较少。

的程序性质主要集中在功能的正确性上，对信息流控制等其他性质的安全性验证工作较少。

在并发程序的精深验证方面，特别是在并发程序活性验证方面的工作在国际上处于领先地位。

我国实际系统中的验证工作比较活跃，但大多数工作集中在模型和算法层面，对代码的验证工作相对较少。

与国际同行相比，缺乏经过验证的系统的规模和影响力。

近年来，国外在抽象解释的理论、方法、工具等方面形成了许多有影响的成果，形成了许多有影响的开源和商业化的有效工具平台，一些工具在工业界获得了成功。

国内在新型抽象域的设计与实现、特定领域的应用，如中断驱动程序的分析等方面的研究形成了特色。

但国内在开发基于抽象解释的程序分析工具、产业影响等方面与国外还存在一定差距，相信随着国内软件可靠需求的提高，差距会越来越短。

在模型检测方面，近年来国外在软件形式化验证的理论、方法和技术等方面产生了许多有影响的成果，形成了许多高效的软件形式化验证工具。

国内特定领域的研究形成特色达到国际领先水平，包括国防科技大学开发的并行程序验证工具Yogar-CBMC等。

在符号执行方面，总体而言，国内符号执行各方面的研究与国外相接触，包括理论、方法和工具等，国内相关研究学者的工作也可以在主要的符号执行国际会议和期刊上发表，这些工作也引起了国外学者的广泛关注，同时与国外相关学者的交流与合作也越来越多。

但国内在符号执行工具和平台开发、产业影响方面与国外还存在一定差距，相信随着国内软件业自主控制需求的提高，这部分差距将不断缩短。

2.6格式验证工具及应用

近十年来国外在软件形式化验证的理论、方法和技术等方面产生了许多有影响的成果形成了许多高效的软件形式化验证工具。

国内对软件形式化验证工具的开发起步较晚，通用工具的开发与国外仍存在较大差距。

但国内在某些特定领域的研究已形成特色，如国防科技大学开发的并行程序验证工具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从判决问题扩展到优化问题，即优化模式理论。

优化模态理论问题以寻求满足SMT约束的最优解为目的，具有实际应用意义。

目前的代表性研究来自意大利Trento大学[ 68，69 ]。

作为SMT求解的完整算法框架，DPLL(t )取得了很大的成功，但本质上是一种基于回溯框架的指数复杂度算法，难以持续突破求解效率，求解规模有限。

近年来，在SAT领域，基于局部搜索的SAT算法在工业化案例中取得了很大的成功，形成了与基于CDCL的完备算法比肩的局面。

在SMT领域，目前出现了不完备的SMT求解算法，主要用于BV理论。

不完备算法在设计上具有灵活性，对问题的规模不敏感，是未来SMT求解算法的发展趋势。

3.2型号

概率自动机模型不仅在概率模型的检测中具有重要的理论价值和应用场合，而且广泛应用于概率程序的语义和验证[ 91，99 ]、随机算法[ 115，72，105 ]甚至机器学习领域[ 74，102 ]

这表明概率自动机模型不仅在形式化验证领域，而且在计算机其他领域，包括数学、物理、生物、医学等其他自然科学领域也有相当大的研究前景。

包括概率自动机模型及其相关理论、验证问题和应用，具有广泛的研究空间和较高的研究价值。

经过近30年的概率模型检验研究，其理论基础已经十分坚实，许多重要问题已经解决，但同时一些重要的公开问题(如PCTL公式满足性的判定问题)仍然存在。

这一领域还存在许多看似不大但仍然重要的问题有待解决和开发同时这一领域与计算机科学其他领域和其他自然科学的结合也将是一个新的研究方向

混合机器人模型的研究取得了一定的进展，但还有许多问题有待解决。

未来五年混合自动机模型的研究将集中在随机和概率混合系统的形式验证、时滞混合系统的形式验证、大规模非线性混合动态模型的形式验证、开放动态模型的行为预测和验证。

无限并发系统模型的研究取得了很大进展，强相互模拟的判定问题大部分得到了解决，但在允许内部转移的情况下，相互模拟判定可能性的结果很少。

因此，重点解决2.2节表中记载的未解决的公开问题是本领域的趋势。

由于这些问题长期公开，用现有的证明方法很难得到结果，如何开发新的证明方法是该领域的关键。

3.3形式语义与形式建模

从目前国内外对程序语言语义的研究来看，未来程序语言语义的研究将不再是学术上的实用语言，以工业级程序语言为对象的语义研究的目的不仅是为了更好地理解程序语言，而且是为了更好地进行程序分析和验证。

另一方面，编程语言的设计者在设计语言时从形式上定义程序含义的问题在很多年前就被期待着没有得到解决。

当提出学术性的程序语言时，设计者赋予其形式上的意义。

但是，在c、Rust、Go等工业级程序语言中，设计者没有定义形式上的语义，甚至没有定义完整的形式语法定义。

主要原因是工业级程序语言比较复杂，语义难以定义，具有这方面能力的工业界人员很少，也没有一个友好的语义开发框架。

大数据系统、人工智能系统、无人驾驶系统等新计算系统的出现，给形式建模技术的发展带来新的机遇和挑战。

系统的智能性、实时性、空间离散性等特点对系统的安全性和可靠性提出了更高的要求，针对这些系统的特性需要发展新的建模理论、方法和工具，这将成为形式化方法领域的研究热点。

但是由于系统的复杂性和特性越来越高，很难定义统一的建模方法来完整描述系统的所有特性。

如何在模型的表达能力和验证问题的可判定性和复杂度等方面进行取舍，是一项非常困难的工作。

3.4格式条款

大数据、机器学习算法等新的计算模型层出不穷。

这些计算模式下的程序行为与经典的串行程序和并发程序大不相同，需要设计新的规约语言，分析验证方法和技术。

针对这些新计算模型的形式规约语言将成为今后5年左右的研究热点。

3.5格式验证技术和方法

近年来，随着云计算、人工智能等各种研究的热点，在相关领域进行的验证也越来越受到重视。

在云计算和分布式系统的验证中，一些分布式算法和系统的验证工作逐渐出现[303-304]。

但其中分布式数据一致性协议和算法的验证还处于初级阶段，国内外相关工作较少。

人工智能算法和演绎推理技术的结合是另一个有前景的方向。

国内外已初步开展了模型检测和利用其他技术验证人工智能算法的工作，但基于演绎推理的验证工作较少。

这里的主要困难在于，基于演绎推理的验证技术需要形式上定义正确性，以及验证过程本身需要明确验证对象的动作原理。

这两点在人工智能研究领域还没有明确的答案。

未来，抽象解释技术将在新体系结构、语言、应用等实际需求的驱动下进一步发展，值得关注的方向是弱存储器模型分析验证[ 335，322 ]、神经网络分析验证[ 339，364 ]、大数据处理

与约束求解、自动推理、人工智能等基础支撑技术的紧密结合[ 358，350，328，341，357 ]抽象地解释了后续的研究趋势之一[333]。

同时降低误报率仍然是基于抽象解释的程序分析技术实用化的研究课题和重点。

在模型检测部分，我们主要侧重于介绍一般软件代码近年来的验证工作。

另外，近年来，相关领域的关注点进一步扩展到多线程代码的验证、递归等特定类型程序的验证、领域相关代码的验证等。

另外，除了上述的安全性/可达性验证Reachability之外，软件代码的激活/终止可行性验证近年来也备受关注。

在符号执行方面，符号执行技术是受软件工程、安全、系统、网络等相关领域实际需求驱动而发展起来的面向大型软件的高效符号执行方法、技术和工具，是下一步的研究课题和重点，同时符号执行检索策略的更加智能化也是下一步研究的重点，同时为了进一步提高软件分析的效果，与其他技术在不同层次上的密切合作也将成为符号执行的下一个研究趋势之一。

3.6格式验证工具及应用

软件形式化验证面临着严重的状态空间爆炸问题。

软件形式化验证工具开发的重要趋势之一是多技术融合。

利用形式化方法的严格性和其他技术的可伸缩性，在验证规模和验证精度上实现协调统一。

混合系统由于其行为离散、连续纠缠十分复杂，难以掌握和控制，现阶段能够进行有效分析的系统种类和规模还存在一定的局限性。

目前主要关注的问题是大规模非线性混合系统的验证、开放型动态系统的行为预测与验证、随机行为的建模与验证、混合系统的控制生成、混合系统的测试生成等。

相关领域的科研人员试图突破上述问题，对实际系统规模问题具备分析能力，保障相关系统的运行安全。

3.7量子程序分析与验证

总的来说，量子程序分析和形式化验证领域已经取得了一些可喜的进展，但目前的研究还非常零散，许多问题甚至不清楚确切的定义。

这主要有两个理由。 一是尽管近几年量子硬件设备的物理实现取得了很大的进展，但离能够运行真正实用的量子程序的通用量子计算机还很远。

因此，大部分传统计算机科学家和编程与验证专家仍持观望态度，未充分重视这一领域二、由于量子程序与传统计算机程序有较大差异，尤其是由于量子叠加和纠缠的存在，量子普

但是我们有理由相信量子程序理论和验证的研究会引起越来越多计算机科学家的关注并使这一领域蓬勃发展

4结束语

形式化方法是计算机科学的传统研究方向，涵盖了许多不同的研究方向。

本文比较全面地总结了形式化方法各方面近五年来的研究进展，并展望了发展趋势。

本报告希望计算机科学与技术其他领域的研究者和IT产业界的从业人员更好地理解形式化方法这一学科的内涵、外延、国内外研究现状，促进形式化方法与其他领域的交叉融合，促使形式化方法在IT产业界有更多的应用。

作者简介

卜磊

南京大学副教授，主要研究方向是实时混合CPS系统、软件代码等复杂系统的形式化验证和分析测试技术。

CCF形式化专业委员会委员、系统软件专业委员。

陈立前

国防科技大学副教授，主要研究项目分析与验证，抽象解释，CCF形式化专业委员会委员。

陈哲

南京航空航天大学副教授，主要研究形式化方法、软件验证、航空电子系统可靠性与安全性验证、软件工程，CCF形式化专业委员会委员。

陈振邦

国防科技大学副教授、硕导，主要研究方向为形式化方法、流程分析及其应用，为CCF形式化专业委员会委员。

冯新宇

南京大学教授，研究方向为编程语言、形式化程序验证、软件安全。

CCF形式化方法专业委员会委员、系统软件专业委员会委员。

冯元

悉尼科技大学量子软件与信息中心，教授，主要研究量子程序的分析和验证。

贺飞

清华大学，副教授，博导，主要研究形式化方法、程序分析与验证等，CCF形式化专业委员会委员。

李国强

上海交通大学，副教授，博导，主要研究形式化验证、程序语言理论、知识表示与推理，CCF形式化专业委员会委员。

刘万伟

国防科技大学，副教授，主要研究时间序列逻辑、模型检验、自动机理论，CCF形式化专业委员会委员。

墨菲

中国科学院软件研究所，副研究员，主要研究自动推理、约束求解。

宋富

上海科技大学，助教，研究员，博导，主要研究形式化方法、流程分析与验证、计算机安全与软件工程，CCF形式化专业委员会委员。

田聪

西安电子科技大学，教授，主要研究可信软件理论与方法、大数据与机器学习软件开发方法、CCF形式化方法专业委员会、CCF青工委委员、女工委委员。

王淑灵

中国科学院软件研究所副研究员，主要研究形式化方法、交互定理证明以及混合系统的建模与验证，CCF形式化专业委员会委员。

吴志林

中国科学院软件研究所，副研究员，主要研究项目分析与验证，计算逻辑，自动机理论，CCF形式化专业委员会委员。

薛白

中科院软件研究所，副研究员，主要研究混合系统的分析与验证。

杨鹏飞

中国科学院软件研究所，博士生，主要研究概率模型检验。

尹良泽

国防科技大学，讲师，主要研究方向是形式化方法、流程分析和验证。

简博华

慕尼黑工业大学，博士后，主要研究交互式定理证明、证明自动化、形式化数学和流程验证。

张民

华东师范大学副教授，主要研究形式化方法、程序分析验证、计算机系统建模和软件工程，是CCF形式化专业委员会委员。

张立军

中国科学院软件研究所，研究员，主要研究概率模型检验，CCF形式化专业委员会委员。

张兴元

中国人民解放军理工大学，教授，主要研究领域是计算机辅助定理的证明，是CCF形式化专业委员会成员。

赵永望

北京航空航天大学副教授，主要研究形式化方法、操作系统内核、程序验证等，为CCF形式化方法专业委员会委员、系统软件专业委员会委员。

中国计算机学会

微信号： ccfvoice

用识别二维码关注我们

CCF推荐

【精品文章】

CCF发布2017-2018中国计算机科学技术发展报告点击“阅读原文”，下载并查看报告。