Verification of annotated models from executions

Parasara Sridhar Duggirala, Sayan Mitra, Mahesh Viswanathan

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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.

Original languageEnglish (US)
Title of host publication2013 Proceedings of the International Conference on Embedded Software, EMSOFT 2013
PublisherIEEE Computer Society
ISBN (Print)9781479914432
DOIs
StatePublished - 2013
Event13th International Conference on Embedded Software, EMSOFT 2013 - Montreal, QC, Canada
Duration: Sep 29 2013Oct 4 2013

Publication series

Name2013 Proceedings of the International Conference on Embedded Software, EMSOFT 2013

Other

Other13th International Conference on Embedded Software, EMSOFT 2013
CountryCanada
CityMontreal, QC
Period9/29/1310/4/13

ASJC Scopus subject areas

  • Software

Fingerprint Dive into the research topics of 'Verification of annotated models from executions'. Together they form a unique fingerprint.

Cite this