C2E2 hybrid verification engine | analyze hybrid system models, fast (original) (raw)
Compare Execute Check Engine (C2E2) is a tool for verifying hybrid automata. Hybrid automata are models combining finite state machines and differential equations. They are used for modeling and analyzing robots, autonomous cars, medical devices—more generally, dynamical systems controlled by software. C2E2 can automatically check bounded time invariant properties of nonlinear hybrid automata. The new C2E2 (ver 2.0, Sept 2018) supports compositional modeling, nonlinear dynamics, model editing, and has a powerful new plotter. Read more about the background theory here. Email c2e2help@gmail.com for support.
Video tutorial for most recent C2E2 release
Latest news
Summer, 2020: C2E2 ver 2.1 open source release
November, 2018: C2E2 ver 2.0.1 released for academic use. New: Bug fixes, added tests.
September, 2018: C2E2 ver 2.0 released for academic use. New features: Compositional modeling, model editing, new plotter, constant inputs.
May 15, 2017: C2E2 ver 1.0 released for academic use. New features: Thin variable, can work on Macs.
Version history. C2E2 implements the simulation-based verification approach described in the sequence of publications Duggirala et al. [2013, 2014, 2015]. From version 0.3 onward C2E2 (2016) uses an on-the-fly discrepancy computation algorithm described in Fan and Mitra [2015]. This eliminates the need for manual annotations (called discrepancy functions). Features in version 2.1 (2020):
- Open source release
- Command line operations
- Compositional models
- Thin input variables
- Integrated hybrid model editor (.hyxml)
- Model parsing error messaging
- New general purpose reachtube plotter
- Dropped support for Stateflow
New in version 1.0 (2016):
- Full automation with on-the-fly discrepancy (no need for annotations)
- Support for both CAPD or ODEINT simulations
- Plotter for 2D sections of the reach sets computed.
Contributors. Lucas Brown, Parasara Sridhar Duggirala, Chuchu Fan, Zhenqi Huang, Suket Karnawat, Yangge Li, Yu Meng, Sayan Mitra, Matthew Potok, Bolun Qi, Vyom Thakkar, Mahesh Viswanathan, Le Wang.
Support. The research is in part supported by the National Science Foundation.
