C2E2

Description: Compare Execute Check Engine (C2E2) is a tool for verifying bounded-time invariant properties of hybrid automata and Stateflow models. It supports models with nonlinear dynamics.

C2E2 implements the simulation-based verification approach described in the sequence of publications Duggirala et al. [2013, 2014, 2015]. The new C2E2 (v0.3 2016) uses an on-the-fly discrepancy computation algorithm described in Fan and Mitra [2015]. This eliminates the need for the user to provide annotations (called discrepancy functions).

C2E2 can take inputs in the form of Stateflow model (.mdl) or a hybrid automaton (.hyxml). It generates numerical simulations using CAPD or ODEINT, and it iteratively refines reach set over-approximations to prove invariants. It can also find counterexamples or bug traces. C2E2’s plotter can show 2D sections of the reach sets computed.

C2E2 is developed by the C2E2 development team at University of Illinois at Urbana-Champaign.

VO Integration: No

Active: No

Available Benchmarks: N/A

Website: https://publish.illinois.edu/c2e2-tool/

Download: Instructions can be found here.

Documentation: User guides and publications can be fournd here.

Contact: c2e2help@gmail.com

Excerpt and Graphics from: https://publish.illinois.edu/c2e2-tool/