Verification of Annotated Models from Executions

Duggirala, Parasara Sridhar; Mitra, Sayan; Viswanathan, Mahesh

Permalink

https://hdl.handle.net/2142/90437 Copy

Description

Title

Verification of Annotated Models from Executions

Author(s)

• Duggirala, Parasara Sridhar
• Mitra, Sayan
• Viswanathan, Mahesh

Issue Date

2013-06

Keyword(s)

• Verification
• Hybrid systems
• Simulink
• Lyapunov functions

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 nonlinear, switched systems. In our framework, users are required to annotate the dynamics in each control mode of a switched system by something we call a “discrepancy function” that formally measures the nature trajectory convergence/divergence in 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 show that the approach (a) outperforms other verification tools on standard linear and nonlinear benchmarks, (b) scales reasonably to larger dimensional systems and to longer time horizons, and (c) applies to models with diverging trajectories and unknown parameters.

Publisher

Coordinated Science Laboratory, University of Illinois at Urbana-Champaign

Series/Report Name or Number

Coordinated Science Laboratory Report no. UILU-ENG-13-2204, CRHC-13-04

Type of Resource

text

Language

en

Permalink

http://hdl.handle.net/2142/90437

Sponsor(s)/Grant Number(s)

National Science Foundation / NSF CNS 1016791

Owning Collections