始于模型，不止于仿真-使用 MATLAB 和 Simulink 进行验证、确认和测试系列技术文章（二）

作者 : 胡乐华、MathWorks

在Simulink中对带有时序逻辑算法进行验证

在传统的嵌入式控制软件开发工作中，保证产品满足客户最终的功能和质量要求是一项复杂且极具挑战的工作。特别是在工业产品功能日趋多样并高度集成的今天，控制系统软件的需求往往来自四面八方，这迫使开发团队不得不投入大量的人力与时间确认设计要求、制定测试大纲、构建评审机制，依靠一套成熟完善的产品开发流程来保证预期的功能和质量目标。

一套成熟完善的产品开发流程不仅需要超强的团队协作能力，更需要长期的历史经验累积。想要在行业竞争如此激烈的今天立足，一切从零开始显然是不现实的。各类计算机辅助工具提升了传统开发工作的效率，使得每一个新的项目或者项目中每一项新的工作不必从零开始。在控制领域，MATLAB/Simulink也提供了相应的解决方案，通过建模与仿真，助力嵌入式系统软件的产品开发。在基于模型的设计方式下，工程团队不仅可以使用MATLAB和 Simulink设计复杂的嵌入式控制系统软件算法和逻辑，还能直接将模型自动生成产品级 C\C++ 代码。让一切工作始于模型，实现产品的快速设计迭代。

但基于模型的设计不止于此，MATLAB and Simulink还提供了Model Validation & Verification工具链，支持用户使用仿真测试和基于形式化方法的静态分析，在严谨性和自动化方面完善基于模型的设计，以尽早发现错误，达到更高的质量，帮助用户更快地建立起一套成熟完善的产品开发流程，更从容地应对产品功能和质量目标。

为了让广大用户更加深入地了解上述内容，MATLAB推出《始于模型，不止于仿真-使用 MATLAB 和 Simulink 进行验证、确认和测试》系列技术文章，旨在以三个典型的行业案例，详细阐述如何利用MATLAB and Simulink，在基于模型的设计方式下，开展验证、确认和测试工作，实现开发工具和开发流程的深度融合。该系列包含四篇技术文章，面向嵌入式控制软件开发流程中的不同工作和角色，将共同助力用户产品的设计、实现与测试，具体如下图所示。

• 本文将从动态测试的角度出发，阐述如何进行模型的测试和验证。文章通过一个简单的时序逻辑需求，介绍如何对其进行功能测试例子，带领大家了解时序逻辑在Stateflow中的实现，Test框架的构建，以及使用Test Manager提供的逻辑评估模板快速进行时序逻辑验证。

概述

在做系统设计时，除了包含控制律算法，设计中通常也包含大量的逻辑算法。而时序逻辑算法又是逻辑系统中的重要部分。时序逻辑算法将某种状态的持续时长用于系统的状态控制。此时系统的输出是系统输入、系统当前状态和时间的函数。一些常见的时序逻辑有其固定的格式。针对常见的几种时序逻辑算法，MATLAB 19a在Simulink Test工具箱中推出了验证模板，加快算法的需求验证。

时序逻辑的需求

在系统设计中，我们经常有类似如下的需求

系统进入待机状态3秒后，应进入运行状态；
当车速超过当前档位最高速度，且持续时间超过1秒，变速器应升档；

时序的需求，有时候是为了防止系统模态频繁切换，有时候是为了让系统进入某种稳定状态。对于时序需求，系统的状态取决于系统的输入和当前状态的持续时间，我们在设计系统时，必须引入系统的时间，同时记录系统在进如某个状态的时间点。

为了说明Simulink对时序逻辑算法验证，我们拿最简单的空调系统（制冷和加热功能）说明。对于空调，我们不希望空调的制冷或者加热模式频繁的打开和关闭，于是有下面的需求。

Stateflow中时序逻辑设计

对于温控系统，简化为有加热，制冷和仅换气保持三个状态。在stateflow中，可以使用有限状态机进行系统状态设计。上面的需求中，1.3是进入加热模态的条件。在Stateflow中，将上述条件作为风扇模式到启动热泵的转移条件，在此基础上，根据室温高于还是低于设定温度，确定热泵的工作模式。实现如下

在从风扇模式到热泵模式中，我们使用了时序逻辑函数after来度量系统在风扇模式的保持时间，其语法是after(number_of_events,event)。这里我们使用系统的关键字sec作为事件。

时序逻辑的测试

对于包含时序逻辑的设计，我们如何验证其是否满足了需求呢？这里其实包含两层意思，其一如何设计验证的框架，其二是如何设计验证的激励。

Simulink Test 工具箱提供了多种工具为我们对算法设计提供验证。

我们可以使用Simulink Test提供的测试框架功能，为我们的模型或子系统构建框架。在框架的输入激励端，Signal Builder提供灵活的激励设置，其也可以从Excel表格中导入复杂的激励；测试框架中也可以加入test sequence, 将模型的输出引入到输入中，根据自己的需要，设计根据系统输出变化的激励或时变的激励。

在输出端，可以包含对模型结果的评估，如使用范围检查，断言等模型检查工具模块，对模型的输出进行运行时检查，也可以将结果使用Simulink Data Inspector记录下来，进行仿真后的详细处理。

使用运行时检查模块对时序逻辑进行分析需要建立分析模型，对于复杂的时序逻辑还是挺费时间的。

而使用Simulink Data Inspector记录的数据，要么使用图形本身，借助光标进行观测，或者使用MATLAB代码将验证的逻辑写好，自动化。同样费时且不太友好。

Test Manager集成时序验证

Test Manager作为测试用例管理工具，除了能将测试用例进行归集、分类，还集成了非常丰富的功能。如直接定义测试用例、参数重载运行、参数扫描、模型设置重载和结果评估等。

结果评估中，Test Manager中集成预定义的评估策略和自定义的评估策略。自定义的评估中，包含了许多API供MATLAB评估函数调用，判断测试是否通过。

时序逻辑中，一些有其固定格式。为了提高测试人员的验证速度，新版的MATLAB中推出了图形化时序验证功能。

我们可以将时序逻辑形式化，使用特定的格式编写。对于上面的需求，我们可以将其形式化为“触发—响应“的形式，也就是

当……为真，（且持续……时间后），

则……应为真，（且持续……时间）。

对于我们的这条需求，则是

当温差（室温和设定维度之差的绝对值）为真，且持续2秒以上

则泵的启动指令应为真，且持续至少2秒。

Simulink Test中新的逻辑和时序验证功能模块中，内置了这样的格式的时序验证功能块，可以快速的需求创建形式化的验证语句，同时具有图形化的表示形式。形式化的验证一方面更加严格，同时能够在测试验证中执行。在后期也会加入更加多的模板。

我们的将上面的需求在Simulink Test中实现如下。除了左边的定义区域，Simulink在右边提供对应的图形化形式，方便我们查看定义的准确性，理解时序逻辑。相关的变量也可以非常方便的和模型中的信号映射，或者用MATLAB表达式给出（下图右下角）。时序验证的条件也可以和对应的需求条目关联起来，建立追述关系（下图中间部分）。