@InProceedings{DuggiralaMV:2015c2e2,
  Title                    = {C2E2: A Verification Tool For Stateflow Models},
  Author                   = {Parasara Sridhar Duggirala and Sayan Mitra and Mahesh Viswanathan},
  Booktitle                = {Proceedings of 21st International Conference Tools and Algorithms for the Construction and Analysis of Systems {TACAS} 2015, London, UK, April 11-18, 2015.},
  Year                     = {2015},
  Pages                    = {68--82},
  Publisher                = {Springer},
  Series                   = {Lecture Notes in Computer Science},
  Volume                   = {9035},

  Abstract                 = {Mathwork's Stateflow is a predominant environment for modeling embedded and cyberphysical systems where control software interact with physical processes. We present Compare-Execute-Check-Engine (C2E2)---a verification tool for continuous and hybrid Stateflow models. It checks bounded time invariant properties of models with nonlinear dynamics, and discrete transitions with guards and resets. C2E2 transforms the model, computing simulations using a validated numerical solver, and then computes reachtube over-approximations with increasing precision. For this last step it uses annotations that have to be added to the model. These annotations are extensions of proof certificates studied in Control Theory and can be automatically obtained for linear dynamics. The C2E2 algorithm is sound and it is guaranteed to terminate if the system is robustly safe (or unsafe) with respect to perturbations to the of guards and invariants of the model. We present the architecture of C2E2, its workflow, and examples illustrating its potential role in model-based design, verification, and validation.},
  Codeurl                  = {https://publish.illinois.edu/c2e2-tool/},
  Doi                      = {10.1007/978-3-662-46681-0},
  Keywords                 = {Verification},
  Owner                    = {mitras},
  Pdfurl                   = {research/2015/C2E2_toolpaper.pdf},
  Timestamp                = {2014.10.24},
  Url                      = {http://dx.doi.org/10.1007/978-3-662-46681-0}
}