Demo: C2E2 - A tool for verifying annotated hybrid systems

Parasara Sridhar Duggirala, Matthew Potok, Sayan Mitra, Mahesh Viswanathan

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

Abstract

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.

Original languageEnglish (US)
Title of host publicationProceedings of the 18th International Conference on Hybrid Systems
Subtitle of host publicationComputation and Control, HSCC 2015
PublisherAssociation for Computing Machinery, Inc
Pages307-308
Number of pages2
ISBN (Electronic)9781450334334
DOIs
StatePublished - Apr 14 2015
Event18th ACM International Conference on Hybrid Systems: Computation and Control, HSCC 2015 - Seattle, United States
Duration: Apr 14 2015Apr 16 2015

Publication series

NameProceedings of the 18th International Conference on Hybrid Systems: Computation and Control, HSCC 2015

Other

Other18th ACM International Conference on Hybrid Systems: Computation and Control, HSCC 2015
Country/TerritoryUnited States
CitySeattle
Period4/14/154/16/15

ASJC Scopus subject areas

  • Computer Networks and Communications
  • Computer Science Applications
  • Control and Systems Engineering
  • Electrical and Electronic Engineering

Fingerprint

Dive into the research topics of 'Demo: C2E2 - A tool for verifying annotated hybrid systems'. Together they form a unique fingerprint.

Cite this