形式化方法的工程化

作者 |张志鹏上海控安可信软件创新研究院研发工程师

版块 |鉴源论坛 · 观模

01背 景

形式化方法是基于严格的数学基础，通过采用数学逻辑证明来对计算机软硬件系统进行建模、规约、分析、推理和验证，是用于保证计算机系统正确性以及安全性的一种重要方法。经典的形式化语言和相应的建模方法有VDM[1]、Z[2]、Object-Z[3]、B[4]、Event-B[5]、TLA+[6]，在软件工程领域确立了较大的影响力且有较成功工业界应用。如Event-B曾成功用于巴黎地铁的设计与开发，Amazon也将 TLA+用于Web Services的设计与开发。尽管形式化方法已经通过这些案例表现出了巨大潜力，但是由于对大型嵌入式控制软件进行形式化规约的构建过于复杂，以及开发成本过高等问题，难以在工业界进行规模化的应用。其根本性的难点在于缺少一套将形式化方法与软件工程有机融合，并能够对其进行形式化建模的工程方法，引导工程人员从原始的以自然语言描述的需求出发，适应软件需求变更等常见情况，逐步构建精确描述系统功能的形式化需求规约，并提供相应技术实施需求确认以保证需求规约充分而准确地刻画了期望的功能。

02形式化方法工程化面临的挑战

形式化验证技术发展至今，有着三种较为成熟的方法，其基本原理以及特点如表1所示：

表1形式化方法

传统的形式化方法自动化程度较低且理论性较强，在实际应用中利用其直接进行形式化验证存在着不小的障碍。目前随着模型驱动开发以及形式验证工具的发展，形式化验证的自动化程度得到了显著的提高。

“基于模型的软件开发方法”作为一个崭新的技术，使用如图1所示的“Y”型开发流程。在其开发周期中，工程人员将模型作为核心，从而可以更加关注设计与需求的本身，同时在设计时可以对所建立的模型进行仿真测试，以尽早发现所存在的问题。并且针对设计到编码实现的过程，可以由代码自动生成技术完成，有效地降低引入人工错误的可能。

在基于模型的开发方法中，建模语言和建模工具是其最重要的支柱。而形式化方法则能提供建模语言与建模工具的支持。形式化方法被认为是保证软件需求质量的重要手段，主要思想是建立形式化规约，用形式化规约语言精确地描述用户对软件的需求，通过对规约的逐步精化和验证得到可信的软件系统[7,8]。形式方法包含两项重要技术：形式化规约（formal specification）与形式化验证（formal verification）。前者关心的是形式化建模，即关注如何用精确的、无二义性的数学语言来书写形式化规约用以描述软件需求。后者根据数学方法例如定理证明或模型检验（model checking）等手段，对已建立的形式化规约进行分析，确认其是否满足期望的性质，最大程度地发现需求模型中不一致和二义性等错误，从而根本上保证软件的可靠性[9]。下面以一个工业中的具体案例来介绍形式化方法在实际中的应用场景，使用形式化建模验证和形式化验证工具来验证某操作系统的调度系统安全性。

03形式化方法工程化实例

调度系统从需求到源码实现分为三个部分：需求规范、架构设计和源代码。为保证对调度系统的充分验证，基于模型检测、SAT/SMT solver、CSP、Hoare逻辑等技术对这三部分均进行了形式化建模和相应的形式化验证。需求规范部分进行了形式化需求转换，并依据形式化需求和系统架构获得设计模型。而后使用形式化验证工具VCC、CBMC和PAT分别从单元级、模块级和系统设计级对系统构建的模型进行形式化验证。

3.1 调度系统的形式化建模

形式化建模主要是根据调度系统的需求文档和架构设计来定义系统的CSP模型。首先是对调度系统需求的形式化建模，流程如图2所示：

图2 需求形式化建模流程

● 在底层需求的基础上进行需求的精化得到形式化需求；

● 将形式化需求基于类型进行功能需求和非功能需求的划分；

● 针对功能需求构建出系统模型，其中每条功能需求逻辑都在系统模型的进程中进行了详细描述；

● 针对非功能需求构建出其语义等价的模型约束；

● 将系统模型和性质结合构成整个形式化需求的需求模型。

在系统建模阶段，需要对底层需求描述的内容人工转化为形式化需求，在此过程中对系统需求进行进一步精化和建模，便于后续的工具进行相应的分析与验证工作。

然后根据调度系统的架构设计得到的任务状态迁移模型如下图3所示，使用CSP语言来描述系统行为。使用CSP对该模型采用如下建模步骤：

（1）定义模型所需的变量和常量；

（2）描述各个进程内任务行为；

（3）描述进程转换信息；

（4）定义验证目标。

图3任务状态迁移模型

图中显示了调度系统的六种任务状态，包括Ready（就绪态），Running（运行态），Int（中断态），Suspend（挂起态），Dormant（睡眠态），Null（空状态）。其中Null空状态是任务在任务模块初始化后的状态，任务被创建后由空状态迁移到Dormant睡眠态。任务创建完毕开始执行调度，睡眠态的任务可以迁移到Ready就绪态进入就绪队列等待调度执行，进而迁移到Running运行态；或者被挂起迁移到Suspend挂起态；处于运行态的任务若被高优先级的任务抢占会迁到Int中断态；而所有其他任务状态在运行任务删除调用后，都会返回到Dormant睡眠状态。

3.2 调度系统的形式化验证

为了保证验证的充分性，使用VCC、CBMC对源代码进行形式化验证分析从而验证系统源代码的准确性与一致性。使用PAT工具对系统设计需求进行建模，验证系统中的死锁、活性等安全性质，并根据来自高层需求中的性质验证系统设计需求是否满足高层需求。验证结果如下：

源代码验证模块：在验证了调度系统内所有的单元的函数和子模块后，发现了许多测试不能发现的类型不匹配、变量溢出、除0错误、分支不可达、数组越界、指针内存安全性等问题。

系统设计验证：调度系统应该满足任务间调度的无死锁，且在中断情况下的正确执行。待验证的性质主要包含以下三条：

（1）对于任务调度的无死锁，使用PAT中提供的deadlockfree性质来验证；

（2）对于任务调度的安全性性质，这里定义为在任意时刻，只有一个任务处于运行状态；

（3）对于任务调度的活性性质，满足调度系统的优先级执行原则，不会出现优先级反转。

验证结果如下图4所示：

图4 PAT验证结果

在模拟了1147592状态后，

（1）系统无死锁性质验证通过；

（2）系统未能够执行到同时有两个任务处于运行状态错误状态，系统的安全性性质满足；

（3）系统未能够执行到优先级反转的错误状态，因此系统的活性性质得到满足。

若存在调度系统的迁移关系发生改变等异常情况时，PAT也能验证出调度系统的错误，并给出错误的路径实例，存在死锁的验证结果如下图5所示：

图5 PAT死锁验证结果

04总 结

经过调度系统的形式化验证发现了调度系统实现过程中的部分问题，源代码模块的问题是真实存在的问题，在某个函数或某个模块的代码实现中，该函数或模块的输入依赖于其他部分的传递，可能真实的场景下不会发生上述问题，但形式化验证可以发现这些测试发现不了的错误。系统设计验证模块可以发现系统设计中存在缺陷的地方，可以验证系统设计需要满足的各种性质，并可以注入特殊情况性质来验证系统设计的完备性与安全性，存在错误时，查看具体的错误路径来改善系统设计架构。

综上所述，形式化工程方法，就是以软件形式化方法理论为基础，以系统化的工程方法引导工业界工程人员构建高质量的软件模型，用以引导后续的代码编写和相关测试分析。并选取了工业实际场景中的某操作系统的调度系统的形式化验证工作作为典型的形式化方法的工程化案例，应用了形式化方法的需求分析、建模与验证，由此验证了形式化方法的可行性与有效性。

参考文献：

[1]JPL, NASA. Formal methods guidebook –nasa. http://eis.jpl.nasa.gov/quality/Formal Methods/.

[2]Hall, Using Formal Methods to Develop an ATC Information System, IEEE Software, vol. 13, no. 2, Mar., pp. 66-76, 1996.

[3]C. Jones, Systematic Software Development Using VDM. Prentice Hall, Second Edition, 1990.

[4]J.M.Spivey, The Z Notation: A Reference Manual. Prentice Hall International (UK) Ltd, Second Edition, 1998.

[5]G.Smith. The Object-Z Specification Language. Advancesin Formal Methods, Kluwer Academic, 2000.

[6]Chaudhuri K, Doligez D, Lamport L, et al. Verifying Safety Properties With the TLA+ Proof System[J]. Lecture Notes in Computer Science, 2010, 6173:142-148.

[7]METEOR-S: Semantic Web Services and Processes, http://lsdis.cs.uga.edu/proj/meteor/, 2015.

[8]Paradkar et al., Automated functional conformance test generation for semantic web services, IEEE Int. Conf. Web Services (2007) pp. 110–117.

[9]王戟,詹乃军,冯新宇,等.形式化方法概貌[J].软件学报,2019,(01):33-61[37].

审核编辑黄宇