C2E2: a tool for verifying annotated hybrid systems
C2E2: a tool for verifying annotated hybrid systems
复制标题
C2E2：用于验证带注释的混合系统的工具
DOI：
--
复制
发表时间：
2015
期刊：
影响因子：
--
通讯作者：
Mahesh Viswanathan
中科院分区：
文献类型：
--
作者：
Parasara Sridhar Duggirala;Matthew Potok;S. Mitra;Mahesh Viswanathan
我们提出了比较执行检查引擎（C2E2），一个工具，实现了基于仿真的验证算法的注释混合系统。C2E2的输入是一个带注释的Stateflow模型（或XML格式的带注释的混合系统），可能具有非线性常微分方程（ODE）和时态属性，该属性可以是不变属性或时态优先属性。为了验证，C2E2使用经验证的数值求解器编译ODE，生成模拟，并计算可达状态集的过度近似。如果可达状态的过近似满足（或违反）指定的时间属性，则C2E2终止，否则它计算更精确的过近似并重复。我们将展示C2E2的以下特性：（a）图形用户界面，（B）指定安全性和时间优先级属性，以及（c）验证属性并可视化可达集，这有助于建立对混合系统行为的直觉。
We present Compare-Execute-Check-Engine (C2E2), a tool that implements a simulation based verification algorithm for annotated hybrid systems. The input to C2E2 is an annotated Stateflow model (or an annotated hybrid system in an xml format) with possibly nonlinear ordinary differential equations (ODEs) and a temporal property, which can be either an invariant property or a temporal precedence property. For verification, C2E2 compiles the ODEs using a validated numerical solver, generates simulations, and computes an over-approximation of the set of reachable states. If the over-approximation of the reachable states satisfies (or violates) the temporal property specified, then C2E2 terminates, otherwise it computes a more precise over-approximation and repeats. We would demonstrate the following features of C2E2 (a) the graphical user interface, (b) specifying the safety and temporal precedence properties, and (c) verifying the properties and visualizing the reachable set, which helps in building intuition about the behaviors of the hybrid system.