Mathworks为嵌入式软件增加形式设计方法

[labfans]

为了在基于Simulink模型的设计套件中增加形式设计方法，TheMathworks公司推出了SimulinkDesignVerifier工具，该工具可以为Simulink仿真平台和Stateflow设计与仿真工具提供的模型生成测试和验证属性。
　　DesignVerifier是以形式验证提供商ProverTechnologyAB公司提供的ProverPlug-In验证引擎为基础开发的。Mathworks公司在最近举行的第44届设计自动化会议上展示了该工具。
　　Mathworks公司决定在现有设计软件中增加形式方法，以便给安全性很重要的设备的开发人员提供足够的测试覆盖率，Mathworks公司信号处理和通信部门的行销总监KenKarnofsky表示。最初用户将是嵌入式软件开发人员，Karnofsky指出，不过他相信从长期来看这种功能对硬件和软件设计师都有很大的吸引力。
　　形式方法可以帮助设计师“测试和发现只用仿真很难捕捉到的错误。”Mathworks公司设计自动化部门行销总监PaulBarnard介绍，“你可以执行某种穷尽仿真来尝试和捕捉每种情况，但形式方法能够更早地关注这些情况。”因此需要将形式方法与仿真整合在一起，Barnard指出。
　　DesignVerifier的测试生成功能可以帮助工程师获得测试案例，以支持工业标准的、安全性重要的度量参数，如改进的条件/判定覆盖率。用户可以在Simulink或Stateflow中使用设计验证模块直接定义定制的测试对象。例如，用户可以决定生成只提供100%判定覆盖率的测试。
　　DesignVerifier的属性验证功能可以帮助用户发现诸如遗漏要求和意外状态等问题。举例来说，用户可以确定不可完成的模型覆盖率，比如状态无法进入、开关条件无法发生以及子系统不能执行等。
　　用户可以将Simulink或Stateflow模型上的属性定义为永远真或永远假，Barnard表示。虽然从技术上讲复杂性没有极限，但该工具规定用于“元件尺寸相对合理的”模型，不适合用于具有上千个模块的模型，Barnard指出。　　

图：Simulink采用形式方法,DesignVerifier可用于生成测试和验证属性。

成功和失败
　　DesignVerifier随即会提供一份报告表明哪些属性通过，哪些属性未通过。对于没有通过的属性，工具可以生成反例。
　　为使用DesignVerifier生成测试，用户要提供模型，并规定所需的覆盖率和测试对象。除了测试向量外，DesignVerifier还能生成测试套件，包括“信号建立”模块中的测试输入值和期望输出值。针对失败属性DesignVerifier也会生成相同类型的测试套件。
　　DesignVerifier库中的验证子系统模块可以帮助用户使用Simulink和Stateflow构造体定义复杂的验证对象和约束条件，并且不影响仿真。DesignVerifier功能可以在Matlab环境中以批处理方式进行解释和执行。
　　Mathwork公司的SimulinkDesignVerifier目前可以在Windows和Linux平台上运行，起价8,000美元。