计数器和计时器
Simulink® Design Verifier™ 分析搜索状态序列来找到驱动分析达到满足目标的状态的输入值。每个计数器值或计时器步骤对应不同的状态,因此长计时器或计数器的存在可以显著增加状态表示的大小。由于分析复杂性取决于状态表示的大小,因此您必须特别考虑模型中的计数器和计时器,以避免过度复杂化Simulink Design Verifier分析。
注意
为了Simulink Design Verifier分析的目的,术语配置是指模型中所有持久信息的一组值。
搜索过程会先调查在单个计时器步骤中可以达到的所有配置,然后再考虑在两个计时器步骤中可以达到的任何配置。同样,搜索会先调查所有可以通过两个计时器步骤达到的配置,然后再考虑需要三个或更多计时器步骤的配置,依此类推。耗尽计数器所需的计时器步数直接影响分析需要搜索的状态数。包含时间延迟的模型(例如倒计时器)会强制搜索跨越大量状态,从而使分析变得复杂。
当系统使用大量平均和过滤来延迟对输入变化的响应时,您可能会看到类似的效果。设计中任何延迟响应的方面都会导致测试序列包含更多的计时器步骤,从而产生更长的测试用例,并且更难识别。
您可以使用一些基本技术来提高带有计数器或计时器的模型的分析性能,包括:
选择非常小的时间延迟值。当时间延迟设置为 2000 步时,出现逻辑错误的系统通常会在时间延迟更改为 2 步时显示该错误。如果您的系统有多个延迟,请为每个延迟选择较小但唯一的值,以便逐步满足您的延迟。
将计数器和计时器的初始值设为Simulink Design Verifier可以修改的参数值。该软件找到允许较短的测试用例超过阈值的初始值。有关更多信息,请参阅 分析参数配置 。
选择更高的滤波器截止频率和更少的平均样本,以最大限度地减少滤波延迟。
您可以使用一些更高级的技术来提高带有计数器或计时器的模型的分析性能,包括:
使用
sldvtimer
来识别可针对 Simulink Design Verifier 测试生成进行优化的计时器模式。使用现有的测试用例或一组测试用例来耗尽计数器或计时器,并扩展这些测试用例以创建完整的测试套件。有关更多信息,请参阅 定义和扩展现有测试用例 。