Title :
Verification of annotated models from executions
Author :
Duggirala, Parasara Sridhar ; Mitra, Subhasish ; Viswanathan, Meera
Author_Institution :
Dept. of Comput. Sci., Univ. of Illinois at Urbana, Champaign, IL, USA
fDate :
Sept. 29 2013-Oct. 4 2013
Abstract :
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.
Keywords :
embedded systems; formal verification; Simulink-Stateflow modeling environment; annotated models verification; contraction metrics; discrepancy function; embedded systems; incremental Lyapunov functions; robustly safe systems; robustly unsafe systems; simulation-based verification framework; switched system control mode; trajectory convergence; trajectory divergence; Computational modeling; Lyapunov methods; Mathematical model; Measurement; Safety; Switches; Trajectory;
Conference_Titel :
Embedded Software (EMSOFT), 2013 Proceedings of the International Conference on
Conference_Location :
Montreal, QC
DOI :
10.1109/EMSOFT.2013.6658604