白皮书

使用仿真和形式化方法验证需求

简介

在系统工程中,两个最重要的任务可以说是了解利益相关方的需求并将其转换为系统需求。本白皮书将探讨如何通过在早期阶段利用建模执行这些任务来展示建模方法。这些建模方法无论是简单的纯描述性模型,还是高级的形式化证明,其复杂性和价值都在日益增加。系统需求质量的提高就足以证明投资这些方法的价值,而由此生成的模型还可以在项目的后期阶段用以更高效地表示利益相关方的需求。接下来,我们将说明如何利用需求模型来实现一致且完整的系统需求。图 1 显示本文中实现这些好处所遵循的过程。

工作流图描述需求的阶段性转换,从利益相关方需求到系统需求再到详细需求,其中涉及系统工程师、软件工程师和测试工程师的需求。在此过程中,会生成各种工件,如架构模型、设计模型、代码文件和测试框架。

图 1.将利益相关方需求细化为系统需求再转化为详细需求的过程。

在本案例研究中,我们将根据下述利益相关方的需求推导出对机器冷却系统的需求:

提供保持机器工作温度的系统,避免因过热而损坏机器。

  • [约束] 冷却系统需要将工作温度保持在 40 ˚C 以下。
  • [约束] 冷却需要在预定时间内有效。
  • [假设] 环境温度高于 -10 ˚C 且低于 80 ˚C。
图中一名工程师正站在冷却系统旁边。

这些利益相关方的需求模糊不明,可能还容易被误解,这也许会使系统需求不完整和/或不正确,从而最终导致设计达不到利益相关方的期望。为了避免这种情况,验证利益相关方的需求是必不可少的。

有一些建模方法可以帮助我们验证对利益相关方需求的了解,并将其转换为一组系统需求。这些方法需要使用以下各项:

  1. 描述性模型
  2. 仿真模型
  3. 形式化模型

我们将在接下来的章节中说明其中每种方法,最后讨论如何使用数字线索来建立利益相关方需求和各级派生需求之间的可追溯性。

节

  1. 使用描述性模型

要了解利益相关方的需求,第一步是描述冷却系统在实际使用中遇到的各种不同场景。例如,当温度过高,或冷却似乎无效时,会产生什么需求?

与传统的自然语言需求模型相比,描述性需求模型向前迈进了一步,因为它们提供了结构化、图形化的需求表示方式,这种方式改进了相关团队之间的协作。体现这种表示方式的一个好例子就是序列图

什么是描述性模型?

描述性模型是一种图形化的系统设定,它以人类可理解的方式描述系统是什么或做什么。

图 2 描述以下场景:如果温度 (T) 过高 (T>=40),则需要冷却;如果冷却有效 (T<40),则应关闭冷却系统;但如果冷却无效(delay>=30),则需要关闭机器。

描述冷却系统三种不同工作场景的序列图。

图 2.描述我们场景的序列图。

节

  1. 使用仿真模型

序列图以图形化的方式描述了冷却系统的建模组件在不同场景下是如何协同工作的。然而,这些描述性需求模型仍仅专用于工程领域,而可仿真(或可执行)需求模型可以为系统领域带来观测值和有用信息,使利益相关方能够直接了解其领域特定的场景中的需求。对于可产生这些输出的可执行形式化工具,一个好例子就是状态图(参见图 3)。

什么是仿真模型?

仿真模型是一种旨在供机器解释的系统设定,其解释的结果需要通过人类的解释得出结论。

一种可仿真的状态图,图中显示通过仿真生成的输出。

图 3.一个可仿真的架构组件(状态机)及其输出。

使用仿真模型很重要,因为仿真为前面序列图中所述的每个场景提供了明确的解释。仿真还可用于将这种解释传达给利益相关方,探索不同场景,了解其具体需求,以便我们可以在系统需求中描述这些信息。

既然我们有一个模型对序列图中指定的行为进行仿真,我们就可以观察并与利益相关方讨论状态机生成的输出。此外,我们可以验证状态机的行为是否与序列图中所描述的场景一致。如图 4 所示,序列图中的绿色对勾表示在仿真期间正确的事件以正确的顺序发生。这证实功能模型行为是正确的。这些结果也可用于与利益相关方一起验证。

序列图显示通过仿真结果验证预期行为,绿色对勾表示“通过”了验证标准。

图 4.通过仿真进行验证。

节

  1. 使用形式化模型

尽管仿真方法能够很好地覆盖系统行为,但仿真通常专注于关键场景以支持协同工作。另一方面,形式化需求模型包含能够对模型质量进行更系统化评估的形式。

其中一种形式化工具就是需求表,它可用于以形式化方式证明一组需求的一致性完整性。一致的需求不会发生冲突,而完整的需求不会遗漏任何功能。图 5 中的预条件列 (A) 描述了系统输入(温度值)以及某项需求何时有效或“处于活动状态”。后条件列 (B) 描述了指定的需求处于活动状态时的预期行为。

什么是形式化模型?

形式化模型是一种旨在供机器解释的系统设定,其解释的输出经过进一步处理,以得出最终的结论供人们使用。

需求表使用形式化表示法解释需求,预条件列描述输入,而后条件列描述预期的输出。

图 5.描述需求的形式化模型。

例如,需求 #1 表示,当 T 低于 40 °C (T<40) 时,冷却系统应关闭 (Turn_off_cooling == true)。

现在,通过使用 Simulink Design Verifier™ 的形式化方法功能进行分析,可以确定需求是否一致和完整。在图 6 中,温度恰好为 40 °C 的场景没有包括在内,因此该需求集并不完整。

对需求表进行形式化分析的结果,其中标记了一个不完整性问题,即缺失 T=40 度这个预条件。

图 6.通过形式化分析确定了不完整性问题(缺失 T=40)。

节

需求模型的更多注意事项和用法

设计模型的测试

形式化需求模型为下游团队提供了良好的开端,因为需求的质量更高,而且需求模型的元素可以在设计、自动测试生成和验证过程中重用。需求模型可以作为单元测试的一部分,以确保开发的功能模型能够满足需求。这些单元测试既能以交互方式执行,也可作为 CI/CD 框架的一部分执行。图 7 显示需求 1 和 2.2 通过了测试,而其他需求尚未执行。

图中显示重用需求表进行验证的测试框架。

图 7.使用形式化需求作为测试方法来验证设计模型。

数字线索及其他

许多工件是在产品开发生命周期的不同阶段创建和/或生成的。这些数字工件包括需求、架构、设计模型、代码文件以及验证和确认文件。要了解需求如何影响其他需求、模型或者验证和确认活动,必须在这些工件之间建立可追溯的关联。这种关联就相当于数字线索。

例如,需求可追溯性图可以从需求和架构模型中自动生成,有助于用户深入了解这些需求、模型和验证工件是如何以图形方式相互关联的。

图 8 显示一位利益相关方的需求被另一位利益相关方满足的数字线索。事实上,多个利益相关方会分布在组织的不同职能领域,涵盖不同的抽象层面。在这种情形下,数字线索就变得不可或缺。此外,数字线索有利于使用自动化、敏捷和迭代的过程和基础架构(开发运营一体化)。例如,图 8 说明了一个测试的验证状态如何自动反馈给负责的工程师。

可追溯性图:显示利益相关方需求、工件(如模型和测试用例)之间的关系,以及关联到需求的验证状态。

图 8.显示冷却系统数字线索的可追溯性图。

随着组织数字化转型之旅的开启,数字线索、数字孪生和开发运营一体化的概念互为补充,共同奠定了数字化工程的基础。通过将这些概念相结合,可以创建一个基础架构,以支持从传统的工程实践转换到以数字为中心的工程实践。

节

结束语

在本文中,我们描述了一个使用仿真和形式化方法将利益相关方需求转化为(可仿真/可执行)系统需求的过程。为此,我们使用了可以仿真的需求模型(状态机)、可以评估的需求模型(序列图),以及可进行形式化分析的需求模型(需求表)。

通过使用需求模型,可以实现验证和确认活动的自动化,从而产生完整、一致且经过验证的系统需求。此外,还能够改进不同团队之间的协作,因为需求模型提供的信息比纯描述性或基于文本的需求要多。

作者:Alan Moore、Becky Petteys 和 Stephan van Beek

节