Tutorial: Software tools for hybrid systems verification, transformation, and synthesis: C2E2, HyST, and TuLiP

Parasara Sridhar Duggirala, Chuchu Fan, Matthew Potok, Bolun Qi, Sayan Mitra, Mahesh Viswanathan, Stanley Bak, Sergiy Bogomolov, Taylor T. Johnson, Luan Viet Nguyen, Christian Schilling, Andrew Sogokon, Hoang Dung Tran, Weiming Xiang

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

2 Scopus citations

Abstract

Hybrid systems have both continuous and discrete dynamics and are useful for modeling a variety of control systems, from air traffic control protocols to robotic maneuvers and beyond. Recently, numerous powerful and scalable tools for analyzing hybrid systems have emerged. Several of these tools implement automated formal methods for mathematically proving a system meets a specification. This tutorial session will present three recent hybrid systems tools: C2E2, HyST, and TuLiP. C2E2 is a simulated-based verification tool for hybrid systems, and uses validated numerical solvers and bloating of simulation traces to verify systems meet specifications. HyST is a hybrid systems model transformation and translation tool, and uses a canonical intermediate representation to support most of the recent verification tools, as well as automated sound abstractions that simplify verification of a given hybrid system. TuLiP is a controller synthesis tool for hybrid systems, where given a temporal logic specification to be satisfied for a system (plant) model, TuLiP will find a controller that meets a given specification.

Original languageEnglish (US)
Title of host publication2016 IEEE Conference on Control Applications, CCA 2016
PublisherInstitute of Electrical and Electronics Engineers Inc.
Pages1024-1029
Number of pages6
ISBN (Electronic)9781509007554
DOIs
StatePublished - Oct 10 2016
Externally publishedYes
Event2016 IEEE Conference on Control Applications, CCA 2016 - Buenos Aires, Argentina
Duration: Sep 19 2016Sep 22 2016

Publication series

Name2016 IEEE Conference on Control Applications, CCA 2016

Conference

Conference2016 IEEE Conference on Control Applications, CCA 2016
CountryArgentina
CityBuenos Aires
Period9/19/169/22/16

ASJC Scopus subject areas

  • Control and Optimization
  • Modeling and Simulation

Fingerprint Dive into the research topics of 'Tutorial: Software tools for hybrid systems verification, transformation, and synthesis: C2E2, HyST, and TuLiP'. Together they form a unique fingerprint.

  • Cite this

    Duggirala, P. S., Fan, C., Potok, M., Qi, B., Mitra, S., Viswanathan, M., Bak, S., Bogomolov, S., Johnson, T. T., Nguyen, L. V., Schilling, C., Sogokon, A., Tran, H. D., & Xiang, W. (2016). Tutorial: Software tools for hybrid systems verification, transformation, and synthesis: C2E2, HyST, and TuLiP. In 2016 IEEE Conference on Control Applications, CCA 2016 (pp. 1024-1029). [7587948] (2016 IEEE Conference on Control Applications, CCA 2016). Institute of Electrical and Electronics Engineers Inc.. https://doi.org/10.1109/CCA.2016.7587948