ACM SIGAda’s High Integrity Language Technology
International Workshop on
Model-Based Development and Contract-Based Programming
as part of Embedded Systems Week (ESWEEK)
The hybrid automaton formalism can be used for modeling cyberphysical systems in which software implemented controller interact with physical processes through sensors and actuators. Safety verification of such models is an important step in model-based design and analysis of safety critical systems. In this talk, we will present C2E2: a time bounded reachability analysis tool for a general class of nonlinear dynamical systems and hybrid automaton models. C2E2 can be used for verifying safety requirements and also for finding counter-example traces. Previous versions of the tool required users to annotate each system of differential equations of the hybrid automaton with discrepancy functions, and since these annotations are difficult to get for general nonlinear differential equations, the tool had limited usability. The new version of C2E2 is improved in several ways, the most prominent among which is the elimination of the need for user-provided discrepancy functions. It automatically computes piece-wise (or local) discrepancy functions around the reachable parts of the state space using symbolically computed Jacobian matrix and eigenvalue perturbation bounds. The special cases of linear and constant rate differential equations are handled with more efficient algorithm analysis routines. We will discuss these and other new features that make the new C2E2 a usable tool for bounded reachability analysis of hybrid systems. We will also report on our experience using C2E2 on a number of challenging and relevant case studies such as powertrain control systems, oscillator models, and landing protocols.