引言：需求建模是一种从源头确保软件质量的重要手段。需求建模可分为需求规约和需求确认两个部分，前者通过严格设计的形式化语言精确地将需求文档转换为了形式化规约，后者使用基于模型的技术对形式化规约进行多方面的验证以确保需求文档的正确性、有效性以及完备性。

01前 言

在上一次的文章（《形式化工程方法之需求建模(上)》点击阅读详情）中，我们介绍了一种用于引导机载控制系统的形式化规约和需求确认的形式化工程方法，并着重介绍了该形式化工程方法中的需求模型提取部分。本文将继续介绍剩下的需求模型确认部分。

02需求模型确认

需求确认的目的是为了通过确保需求文档的正确性、有效性以及完备性来保证后续工程实现的整个系统是正确可靠的，并作为通过在需求阶段发现问题来减少研发成本的重要手段。经典的需求确认有需求审查、需求规约的动画化和需求规约的测试等方式，而需求审查是作为使用最为广泛的一种确认方式。虽然需求审查本身易推广，但因为其本身存在对需求审查人员要求比较高以及耗时等局限性存在难以得到普及。我们提出了一种基于模型的需求模型确认方法，该方法主要包含以下四个部分：模型确认、基于模型的测试用例生成、模型仿真、性质验证。 

（1）模型确认

模型确认主要是以图形化的方式来展示构建好的需求模型中的一些关键信息，为了更好地帮助工程人员发现需求中的问题，我们针对变量和模式流建立了２种关系图：变量之间的影响关系和模式之间的迁移关系，我们将这２种关系使用变量影响关系图和模式迁移关系图进行表达。

图1 变量依赖关系图

变量影响关系图用节点表示不同的变量，用箭头表示变量间的影响关系，箭头指向被影响的变量。箭头上标注的条件表示特定条件下的变量直接影响关系。

图2 模式迁移关系图

而模式迁移关系图用节点表示不同的模式，用箭头表示模式间的迁移关系，箭头指向要迁移到的模式。箭头上标注的条件表示特定条件下的迁移关系。在状态迁移图中还可以通过选定想要观察的状态进一步观察此状态的各迁移条件，分析状态迁移图以及状态迁移关系来确认模型是否符合预期。可以快捷地帮助需求工程师判断需求功能的描述是否存在缺失。

（2）基于模型的测试用例生成

在航空领域中对测试用例的覆盖准则有严格的要求，测试用例需要满足DO-333标准：测试用例需满足MC/DC覆盖准则的要求。根据DO-333认证标准的要求，我们提出根据形式化需求自动生成符合MC/DC覆盖准则的测试用例，并辅以真值表帮助人工检查生成测试用例的正确性。该方法还可以帮助发现模型本身的一些错误。生成满足MC/DC覆盖准则的测试用例的方法针对的是模型中的每个模块。对于模块中的计算逻辑，通过算法收集满足MC/DC覆盖准则的约束并将其输入Z3约束求解器中求解来得到测试用例。

图3 约束有误的示例

图3展示了一个条件错误的示例，通过对该例子进行基于MC/DC覆盖准则的测试用例约束与求解，可以得到如表１所示的结果。

表1测试用例

表1中空白的一项因为条件约束有错，无法求出测试用例。在模型检查的过程中，根据MC/DC覆盖准则生成测试用例，如果有无法生成测试用例的情况，那么就代表模型中的控制算法有错，说明原需求文档的控制逻辑有误。

（3）模拟仿真

模拟仿真操作是在基于需求建立的模型基础上结合上外部输入来使得需求模型模拟真实系统在实际运行中的本质过程，在模拟系统在实际运行过程中，会再以动图的形式实时模拟状态的变化，并提供每个数据各个周期的值。也正是由于其可以根据需求模拟真实执行过程，并记录该系统下每个周期的状态以及变量的值，可以做到代替传统测试中测试人员根据所测需求来进行的手动计算，避免因为人工计算引发的一些不必要的错误，提高了计算的准确性和效率。控制工程师给定的物理环境模拟器是一个确定性系统，即给定相同的输入序列，必然得到同样的输出序列。在此假设下获得可执行程序的方法的模拟结果。模拟执行示意图如图4所示。

图4 模拟执行示意图

模拟仿真的过程是：首先进行初始化，为全局变量设置初值，为各个基本模式的计算过程创建相应的任务，启动物理环境模拟器；然后进入控制回路。在该回路中，首先调用物理环境模拟器的接口，从环境采集数据，更新输入变量；然后执行当前模式相对应的计算任务，计算任务由一系列模块组成。如果计算任务完成，则开始检查模式切换条件，调用物理环境模拟器的接口驱动执行机构，然后进入下一次迭代。如果计算任务因为超时被挂起，则调用物理环境模拟器的接口驱动执行机构，然后进入下一次迭代，直接继续未完成的执行计算任务。

（4）性质验证

性质验证是一种经典的用于验证模型是否满足给定性质的技术。一个非常流行的性质描述语言是 LTL，其可以用于描述线性执行的系统。航空航天领域的发动机控制软件和飞行器控制软件均是典型的线性运行的系统。然而，由于飞行器的执行被随机的环境变量所影响，导致传统的模型检查技术不能够直接适用。与此同时，需求工程师们需要一种不需经过模拟仿真即可找到需求中错误的方法，具体来说，用户需要验证一个性质，希望知道在所得到的需求模型之中，该性质是否始终满足，若不满足，则给出其反例。为了解决工业上的实际性质验证需求，我们提出了一个简易版本的性质验证方法用于进行静态时全局的性质验证。性质验证的框架如图5所示。

图5 性质验证框架

用户选择待验证的需求条目，工具将自动抽取待验证需求条目中的控制流路径，形成所有路径的集合。然后对模型中每一条路径进行分析，收集路径中的约束条件。根据用户撰写的性质，将用户的性质取反后与路径中的约束条件做合取操作得到待验证的性质。对待验证的性质进行求解，得到验证结果，验证结果包括收集到的路径数量，满足性质的路径的数量，不满足性质的路径数量，并针对不满足性质的路径提供反例来说明在何种情况下不满足性质。将该验证结果反馈给用户后，用户可以根据该结果扩大或缩小待验证的需求条目集合，进行更进一步的性质验证。

在该方法中，路径收集本质上是为了收集路径中的约束条件，为了保障约束条件的准确性，我们使用了符号执行的方法进行路径的收集。在路径收集的过程中主要是为了得到所有的状态路径集合，每个状态路径中维护了该路径下的符号表、内存模型和约束条件。由于在路径收集的过程中已经排除了不可达路径，因此当路径收集结束后，遍历所有的状态路径，根据用户撰写的性质，将用户的性质取反后与可达路径做合取操作得到待验证的性质。将合取得到的表达式输入给求解器进行求解。如果Z3求解器无法得到解，说明该性质在该路径的取值域内是成立的，将该状态路径归类于满足性质的可达路径。反之，如果 Z3求解器得到了解，说明该性质在该路径的取值域内存在不成立的情况，将该路径归类于不满足性质路径。针对所有的状态路径，如果它们在要验证的性质下都属于满足性质路径，那么认为该性质在需求模型中是满足的；只要存在任意一条可达路径属于不满足性质路径，那么认为该性质在需求模型中是不满足的。最终将不满足性质的路径的反例返回给用户查看。

这种简易版本的性质验证方法在实际实现时存在的问题如下：

· 路径收集问题：在路径收集时，由于在该模型语言中路径的概念存在于各个模块之中，类比于C语言中的函数的话，那么函数的先后执行情况预先并不可知，导致收集到了大量系统实际运行时根本不会执行的路径。

· 状态爆炸问题：为了解决赋值语句对于条件的影响变化的问题，最终使用了符号执行的技术进行路径的收集，然而，当嵌套的分支过多时，比如当三个模块都发生十几层的嵌套时，会使路径收集工作无法正常完成。

基于上述问题，目前该性质验证仅能用于少量模块间的全局系统性质验证。

· 实验结果：为了验证该形式化工程方法的可行性并展示其有效性，我们将其应用到真实的航空发动机控制软件的需求分析中。实验中有２名经验丰富的工程师全程参与。在将非形式化需求逐步转化成形式化规约的过程中，因为工程师对领域知识非常熟悉，需求规约的构建大约用时２个月。该控制软件的形式化需求规约是一份包含了10个模式、152个模块、1145个变量的Microsoft Word文件。在规约转化成原型的过程中，一共发现了78个语法错误、72个变量遗漏、23个变量类型错误。在进行图形化审查时，一共生成了152个变量依赖关系图、152个变量模块依赖关系图、152个模块模式依赖关系图、1个模式迁移关系图。另外，通过对需求模型的分析，一共生成2342条基于MC/DC覆盖准则的测试用例。通过合作方提供的外部数据，我们顺利完成了需求模型的模拟执行，与合作方通过Matlab模拟的情况一致。

03总 结

本文主要介绍了形式化工程方法中需求建模技术的需求确认部分，我们设计了一种基于模型的需求确认技术，包括模型确认、基于模型的测试用例生成、模型仿真、性质验证。

我们提出的形式化工程方法在实际航空发动机软件开发项目中展现了优于工业界传统手工审查方法的缺陷发现能力和提供了直观地展示需求中变量关系的能力，进一步佐证了形式化方法在嵌入式控制软件领域的良好前景。未来随着更多技术的发展，我们会继续致力于更为系统化、更能被工业界工程人员接受的嵌入式控制软件形式化规约构建方法和工具链。

作者 | 杨坤 上海控安可信软件创新研究院系统建模组版块 |鉴源论坛 · 观模社群 |添加微信号“TICPShanghai”加入“上海控安51fusa安全社区”

主要参考文献：

[1] Youn Kyu Lee, Hoh Peter In, Rick Kazman. Customer Requirements Validation Method Based on Mental Models[C] // Proc of Software Engineering Conference, 2015:199-206.

[2] Aceituna D, Do H, Lee S W. SQ^(2)Ｅ：An approach to requirements validation with scenario question[C] //Proc of 2010 Asia Pacific Software Engineering Conference，2010: 33-42.

[3] Li M, Liu S. Integrating Animation-Based Inspection Into Formal Design Specification Construction for Reliable Software Systems[J]. IEEE Transactions on Reliability, 2016, 65(1): 88-106.

[4] Aceituna D, Do H, Lee S W. Interactive requirements validation for reactive systems through virtual requirements prototype[C] // Proc of Model-Driven Requirements Engineering Workshop, 2011:1-10.

[5] Wang H, Liu S, Gao C. Study on model-based safety verification of automatic train protection system[C] // Proc of Asia-Pacific Conference on Computational Intelligence and Industrial Applications, 2009: 467-470.

[6] Ahmad E, Dong Y W, Larson B, et al. Behavior modeling and verification of movement authority scenario of Chinese Train Control System using AADL[J]. Science China Information Sciences, 2015, 58(11):1-20.

[7] Miao W, Pu G, Yao Y, Ting S, et al. Automated Requirements Validation for ATP Software via Specification Review and Testing[M] // Formal Methods and Software Engineering. Berlin : Springer International Publishing, 2016:26-40.