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

doi:10.1109/CCA.2016.7587948

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 proceeding › Conference contribution

3 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 language	English (US)
Title of host publication	2016 IEEE Conference on Control Applications, CCA 2016
Publisher	Institute of Electrical and Electronics Engineers Inc.
Pages	1024-1029
Number of pages	6
ISBN (Electronic)	9781509007554
DOIs	https://doi.org/10.1109/CCA.2016.7587948
State	Published - Oct 10 2016
Externally published	Yes
Event	2016 IEEE Conference on Control Applications, CCA 2016 - Buenos Aires, Argentina Duration: Sep 19 2016 → Sep 22 2016

Publication series

Name	2016 IEEE Conference on Control Applications, CCA 2016

Conference

Conference	2016 IEEE Conference on Control Applications, CCA 2016
Country/Territory	Argentina
City	Buenos Aires
Period	9/19/16 → 9/22/16

ASJC Scopus subject areas

Control and Optimization
Modeling and Simulation

Access to Document

10.1109/CCA.2016.7587948

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). Article 7587948 (2016 IEEE Conference on Control Applications, CCA 2016). Institute of Electrical and Electronics Engineers Inc.. https://doi.org/10.1109/CCA.2016.7587948

Tutorial: Software tools for hybrid systems verification, transformation, and synthesis: C2E2, HyST, and TuLiP. / Duggirala, Parasara Sridhar; Fan, Chuchu; Potok, Matthew et al.
2016 IEEE Conference on Control Applications, CCA 2016. Institute of Electrical and Electronics Engineers Inc., 2016. p. 1024-1029 7587948 (2016 IEEE Conference on Control Applications, CCA 2016).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Duggirala, PS, Fan, C, Potok, M, Qi, B, Mitra, S, Viswanathan, M, Bak, S, Bogomolov, S, Johnson, TT, Nguyen, LV, Schilling, C, Sogokon, A, Tran, HD & 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., 7587948, 2016 IEEE Conference on Control Applications, CCA 2016, Institute of Electrical and Electronics Engineers Inc., pp. 1024-1029, 2016 IEEE Conference on Control Applications, CCA 2016, Buenos Aires, Argentina, 9/19/16. https://doi.org/10.1109/CCA.2016.7587948

Duggirala PS, Fan C, Potok M, Qi B, Mitra S, Viswanathan M et al. Tutorial: Software tools for hybrid systems verification, transformation, and synthesis: C2E2, HyST, and TuLiP. In 2016 IEEE Conference on Control Applications, CCA 2016. Institute of Electrical and Electronics Engineers Inc. 2016. p. 1024-1029. 7587948. (2016 IEEE Conference on Control Applications, CCA 2016). doi: 10.1109/CCA.2016.7587948

Duggirala, Parasara Sridhar ; Fan, Chuchu ; Potok, Matthew et al. / Tutorial : Software tools for hybrid systems verification, transformation, and synthesis: C2E2, HyST, and TuLiP. 2016 IEEE Conference on Control Applications, CCA 2016. Institute of Electrical and Electronics Engineers Inc., 2016. pp. 1024-1029 (2016 IEEE Conference on Control Applications, CCA 2016).

@inproceedings{9a32730ada384428bfdd6778f34a48b6,

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

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.",

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

year = "2016",

month = oct,

day = "10",

doi = "10.1109/CCA.2016.7587948",

language = "English (US)",

series = "2016 IEEE Conference on Control Applications, CCA 2016",

publisher = "Institute of Electrical and Electronics Engineers Inc.",

pages = "1024--1029",

booktitle = "2016 IEEE Conference on Control Applications, CCA 2016",

note = "2016 IEEE Conference on Control Applications, CCA 2016 ; Conference date: 19-09-2016 Through 22-09-2016",

}

TY - GEN

T1 - Tutorial

T2 - 2016 IEEE Conference on Control Applications, CCA 2016

AU - Duggirala, Parasara Sridhar

AU - Fan, Chuchu

AU - Potok, Matthew

AU - Qi, Bolun

AU - Mitra, Sayan

AU - Viswanathan, Mahesh

AU - Bak, Stanley

AU - Bogomolov, Sergiy

AU - Johnson, Taylor T.

AU - Nguyen, Luan Viet

AU - Schilling, Christian

AU - Sogokon, Andrew

AU - Tran, Hoang Dung

AU - Xiang, Weiming

PY - 2016/10/10

Y1 - 2016/10/10

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=84994235416&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84994235416&partnerID=8YFLogxK

U2 - 10.1109/CCA.2016.7587948

DO - 10.1109/CCA.2016.7587948

M3 - Conference contribution

AN - SCOPUS:84994235416

T3 - 2016 IEEE Conference on Control Applications, CCA 2016

SP - 1024

EP - 1029

BT - 2016 IEEE Conference on Control Applications, CCA 2016

PB - Institute of Electrical and Electronics Engineers Inc.

Y2 - 19 September 2016 through 22 September 2016

ER -

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

Abstract

Publication series

Conference

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Cite this