Verification of annotated models from executions
Verification of annotated models from executions
复制标题
DOI：
10.1109/emsoft.2013.6658604
复制
发表时间：
2013-09
期刊：
影响因子：
--
通讯作者：
Parasara Sridhar Duggirala;S. Mitra;Mahesh Viswanathan
中科院分区：
文献类型：
--
作者：
Parasara Sridhar Duggirala;S. Mitra;Mahesh Viswanathan
仿真可以帮助提高系统设计的信心，但它们几乎没有提供正式的保证。在本文中，我们提出了一个基于仿真的验证框架描述的非线性，切换系统的嵌入式系统。在我们的框架中，用户需要注释的动态切换系统的每个控制模式的东西，我们称之为差异功能，正式衡量的性质轨迹收敛/发散的系统。离散函数推广了轨迹收敛和发散的其他度量，如收缩函数和增量李雅普诺夫函数。利用这样的注释，我们提出了一个健全的和相对完整的验证程序鲁棒安全/不安全的系统。我们已经建立了一个工具的基础上，集成到流行的Simulink/Stateflow建模环境的框架。与我们的原型工具的实验表明，该方法（a）优于其他验证工具的标准线性和非线性基准，（B）规模合理，更大的维度系统和更长的时间范围，（c）适用于模型与发散的轨迹和未知参数。
Simulations can help enhance confidence in system designs but they provide almost no formal guarantees. In this paper, we present a simulation-based verification framework for embedded systems described by non-linear, switched systems. In our framework, users are required to annotate the dynamics in each control mode of switched system by something we call a discrepancy function that formally measures the nature of trajectory convergence/divergence of the system. Discrepancy functions generalize other measures of trajectory convergence and divergence like Contraction Metrics and Incremental Lyapunov functions. Exploiting such annotations, we present a sound and relatively complete verification procedure for robustly safe/unsafe systems. We have built a tool based on the framework that is integrated into the popular Simulink/Stateflow modeling environment. Experiments with our prototype tool shows that the approach (a) outperforms other verification tools on standard linear and non-linear benchmarks, (b) scales reasonably to larger dimensional systems and to longer time horizons, and (c) applies to models with diverging trajectories and unknown parameters.