Symbolic analysis for improving simulation coverage of Simulink/Stateflow models
Symbolic analysis for improving simulation coverage of Simulink/Stateflow models
复制标题
用于提高 Simulink/Stateflow 模型仿真覆盖范围的符号分析
DOI：
--
复制
发表时间：
2008
期刊：
影响因子：
--
通讯作者：
K. Shashidhar
中科院分区：
文献类型：
--
作者：
R. Alur;Aditya Kanade;S. Ramesh;K. Shashidhar
为了验证嵌入式控制软件的混合系统模型的安全性和提高仿真覆盖率，我们提出了一种将数值模拟和符号方法相结合的状态集计算技术。我们考虑在商业建模工具Simulink/Stateflow中描述的线性动力学系统。给定初始状态x和离散时间仿真轨迹，我们的方法计算一组保证与x等效的初始状态，其中两个初始状态被认为是等效的，如果结果仿真轨迹在仿真的每一步包含相同的离散分量。我们通过两个案例研究来说明我们的方法的好处。一个案例研究是混合系统验证文献中提出的基准，另一个是来自Mathworks的Simulink演示模型。
Aimed at verifying safety properties and improving simulation coverage for hybrid systems models of embedded control software, we propose a technique that combines numerical simulation and symbolic methods for computing state-sets. We consider systems with linear dynamics described in the commercial modeling tool Simulink/Stateflow. Given an initial state x, and a discrete-time simulation trajectory, our method computes a set of initial states that are guaranteed to be equivalent to x, where two initial states are considered to be equivalent if the resulting simulation trajectories contain the same discrete components at each step of the simulation. We illustrate the benefits of our method on two case studies. One case study is a benchmark proposed in the literature for hybrid systems verification and another is a Simulink demo model from Mathworks.