初探形式化方法基本原理
1.形式化方法基本概念
形式化方法是基于严格的数学基础，通过采用数学逻辑证明来对计算机软硬件系统进行建模、规约、分析、推理和验证，是用于保证计算机软硬件系统正确性以及安全性的一种重要方法。
形式化方法使用数学及逻辑证明的手段对计算机系统进行建模、规约、分析、推理，其主要涵盖以下几个研究方向：定理证明、形式模型、形式语义与形式建模、形式规约、形式验证技术。下面以高可信工业领域实际应用中最广泛的形式化规格说明、定理证明和模型检测为例，介绍其基本原理。
2.形式化规格说明
通过对编程语言的语义进行严格的定义，加之使用形式模型对计算机系统的行为进行建模，最终形成形式化规格说明书来对计算机系统的行为进行推理验证，形式规格说明是对计算机系统进行验证的基础，形式规格说明的基础是形式语义学和形式建模。
形式语义学（formal semantic）是研究程序设计语言的语义的学科，以数学为工具，利用符号和公式，精确地定义和严格地解释计算机程序设计语言的语义，从而消除设计者、开发者和使用者之间的理解的差异性。形式语义帮助理解语言，指导语言的设计，帮助编写编译器和语言系统，支持程序验证和软件可靠性，有助于软件规范化。形式语义学主要分为四大流派：操作语义，代数语义，指称语义和公理语义。操作语义着重模拟数据处理过程中程序的操作；代数语义基于代数，用代数结构刻画程序语法实体，用代数公理刻画实体含义以及语法实体间的关系；指称语义主要刻画数据处理的结果，而不是处理的细节；公理语义用公理化的方式描述程序对数据的处理，主要用于程序的推理和论证。早期的程序语言的语义只是在论文中给出，不能用计算机测试语义的正确性和一致性，也不能用于程序的验证和分析。中期的语义一般用定理证明器的元语言实现，此类语义可用于程序语言语义和程序性质的手动或半自动验证。K框架是最近流行的定义语言的形式语义的途径，基于重写逻辑，通过定义语言的操作语义，自动生成对应程序的形式分析和验证工具。
形式建模是对计算机软硬件系统的行为和性质用某种形式模型精确的刻画。形式模型一般采用通用形式建模语言（如Petri Net、Event-B、Pi-演算、CSP、SysML、Lusture等）或者专用形式模型（如有限自动机、下推自动机、概率自动机等）来进行。函数式程序可以用树自动机、高阶下推自动机来建模，自适应系统与多智能体一般使用Petri网、UML、Z以及马尔可夫模型等来建模，对于深度神经网络的形式建模最近也成为研究热点。
2.1 形式化规格说明举例
假设有一个“农夫过河”系统，其需求文档如下：
（1）一个人带着狼、山羊和白菜在一条河的左岸，有一条船，大小正好能装下这个人和其它三者之一，人和他的随行物都要带过岸，但他每次只能带一样东西摆渡过河。
（2）如人将狼和羊留在同一岸，无人照顾，那么狼会把羊吃掉。同样，如羊和白菜在同一岸，无人照顾，那么羊会吃了白菜。
该系统在设计完成后，应当满足性质：至少存在一条过河路径，使得人和他的随行物全部渡过了河。
为了验证上述系统是否满足相对应的性质，使用NuSMV形式化验证工具进行性质的验证工作。NuSMV是一款经典的基于BDDs(Binary Decision Diagrams)的模型验证器。在本例中，我们将使用NuSMV提供的形式化描述语言对一个系统的需求进行形式化规格说明的转化。
用对上述自然语言描述的需求文档进行形式化建模，使用NuSMV的形式化语言描述如图1所示。
▲图1 农夫过河系统的形式化规格说明
对待验证的性质使用性质描述语言进行描述，如图2所示。
▲图2 待验证性质的形式化描述
使用NuSMV进行模型检测的基本原理是将形式化语言描述的系统和待验证的性质抽取形成一个状态迁移系统，在该状态迁移系统中若存在一个可接收状态即为该系统满足特定性质。后续的形式化验证工作即是建立在该形式化规格说明上的。
3.形式化验证技术
3.1 定理证明技术
在形式语义与形式建模以及形式规约的基础上，将计算机系统的分析与验证问题转化为逻辑推理问题或者形式模型的判断问题，用定理证明工具/求解器或者某个形式模型的原型工具来进行验证。形式化验证主要的技术有定理证明和模型检测。
定理证明的基本思想是，将程序满足其形式规约的证明问题转化为一组数学命题的证明。若这一组数学命题，称作证明义务（proof obligation），能够蕴含“程序满足其规约”这一命题，那么我们可以说该证明系统是正确（sound）的。
3.1.1 简单推理举例
在数学运算中，有许多运算公理及其推导出的运算属性。在给出如图3所示的运算公理时，证明运算属性P1：x=x+y*0 成立便是一个简单的推理证明过程。推理证明过程如图4所示。
▲图3 数学运算公理
▲图4 数学运算属性证明过程
3.1.2 定理证明举例
同上述章节中推导出来的数学运算的性质等同，在程序中，使用Hoare logic来证明程序的部分正确性。它以一阶逻辑为基础，利用运算规则、公理与推理规则进行程序证明。即：如果断言P在程序S执行前为真时可推出断言R在S终止时为真，则程序S对于P和R来说是正确的，使用三元组表示为：{P} S {R}。
尝试证明：{x <> y∧x > y} x := y – 1 {x = y ∨ x < y}的正确性。在该语句中，P={x<>y ∧x > y} ；S=x:=y-1；Q={x = y ∨ x < y}。为了证明该语句，需要使用两条公理，一条是赋值公理（Ass-D0），一条是推论规则。赋值公理指，{P[f/x]} x := f {P}成立，P[f/x]是用f替代P中所有x得到的谓词表达式。推论规则指：如果{P} S {R}成立，则对于所有Q=>P，{Q} S {R}均成立。根据上述两条公理，当我们想证一条{P}S{R}成立时，我们可以根据赋值公理找到一个一定使后置条件满足的情况{R[f/x]}x:=f{R},当P能够=>P[f/x]时，{P}S{R}得证。如图5所示，使用赋值公理，将后置条件中的x使用赋值语句中的x=y-1替代，得到{y<y+1}x:=y-1{x=y∨x<y}恒成立。下面，只需证明{ x="" <="">y∧x >y}=>{y<y+1}，即可使用推论规则得到{x <="">y∧x > y} x := y – 1 {x = y ∨ x < y}成立。由于y < y + 1 <=> true,所以{ x <> y∧x >y}=>{y<y+1}。因此{x <="">y∧x > y} x := y – 1 {x = y ∨ x < y}成立。
▲图5 赋值公理的使用过程
3.2 模型检测技术
模型检验的基本思想是通过遍历系统的状态空间以验证系统模型是否满足给定的关键性质，并在不满足性质时给出具体反例路径。因此，如何对模型状态空间进行快速遍历对于模型检验至关重要，而状态空间爆炸问题则自然成为模型检验技术面临的主要问题。与模型检验技术取得成功的硬件领域相对比，软件系统的状态空间复杂性更高。将相关状态空间符号化表达, 并在符号化后的空间上进行计算和遍历是软件模型检验的基本方法。然而，即使是符号化后的状态空间，其验证也并不是一个简单问题，因此对复杂的状态空间进行抽象简化是一个重要研究方向。
3.2.1 模型检测举例
将上述章节中的农夫过河系统转化成相应的状态迁移图如图6所示，其中MGCW-Empty表示初始状态，“-”左边的符号表示对应的符号在左岸。“-”右边的服务表述对应的符号在右岸。M表示人，G表示羊，C表示白菜，W表示狼，箭头表示表示每次在船上运输的物品的种类。其中因为有一些约束限制所以导致一些理论上会出现的状态并没有出现。
▲图6 农夫过河状态迁移图
该系统待验证的性质在该图中可表述为初始状态为“MGCW-Empty”的情况下， 是否存在一条路径，能够到达终止状态“Empty-MGCW”。即在图6中，是否存在一条路径，使得状态1能够到达状态8。若存在该路径，那么说明经过验证，该系统满足了该性质，若不存在该路径，那么说明经过验证，该系统不满足该性质。
关于形式化验证的定理证明、模型检测等方法在行业中的实际应用情况，我们将在后续的章节中陆续为大家介绍。
4.形式化验证的实际应用
形式化验证可应用于软件领域。传统软件工程的测试通常指通过各种测试手段来验证大部分情况下软件是正确的，而为了使软件绝对安全可靠，可以用形式化验证的手段，证明软件在任意情况下都是正确的。
形式化验证的编译器具有语义保持性，有着极好的口碑。ModelCoder便是一款使用形式化验证的代码生成工具。
L2C(ModelCoder的代码生成工具)其前身是清华大学王生原老师团队研究项目，现由迪捷软件负责商业化开发。ModelCoder是一个模块图环境，用于仿真和基于模型的设计，支持系统级的设计、仿真、自动代码生成以及嵌入式的连续测试和验证，目前客户主要来自核电、航空、航天等领域。
▲ModelCoder模块组成框图
参考文献
1. Jifeng He: A New Roadmap for Linking Theories of Programming. UTP 2016: 26-43.
2. CCF Formal Methods Technical Committee. Advances and trends on formal methods. In: The Progress Report of Computer Science and Technology in China from 2017 to 2018. Beijing: China Machine Press, 2018. 1-68(in Chinese with English abstract).
3. Roșu G, Șerbănută T F. An overview of the K semantic framework[J]. The Journal of Logic and Algebraic Programming, 2010, 79(6): 397-434.
4. Cimatti A , Clarke E , Giunchiglia F . NUSMV: a new symbolic model checker[J]. International Journal on Software Tools for Technology Transfer, 2000, 2(4):410-425.
5. Wang S, Zhan N, Zou L. An improved HHL prover: an interactive theorem prover for hybrid systems[C]//International Conference on Formal Engineering Methods. Springer, Cham, 2015: 382-399.
6. Cousot P, Cousot R. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints[C]//Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages. 1977: 238-252.
