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

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

Fingerprint

Hybrid systems
Software Tools
Hybrid Systems
Synthesis
Specification
Specifications
Controller
Air Traffic Control
Controllers
Discrete Dynamics
Air traffic control
Temporal logic
Formal methods
Model Transformation
Formal Methods
Temporal Logic
Robotics
Simplify
Trace
Control System

ASJC Scopus subject areas

  • Control and Optimization
  • Modeling and Simulation

Cite this

Duggirala, P. S., Fan, C., Potok, M., Qi, B., Mitra, S., Viswanathan, M., ... 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

Tutorial : Software tools for hybrid systems verification, transformation, and synthesis: C2E2, HyST, and TuLiP. / Duggirala, Parasara Sridhar; Fan, Chuchu; Potok, Matthew; Qi, Bolun; Mitra, Sayan; Viswanathan, Mahesh; Bak, Stanley; Bogomolov, Sergiy; Johnson, Taylor T.; Nguyen, Luan Viet; Schilling, Christian; Sogokon, Andrew; Tran, Hoang Dung; Xiang, Weiming.

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 proceedingConference 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). https://doi.org/10.1109/CCA.2016.7587948
Duggirala, Parasara Sridhar ; Fan, Chuchu ; Potok, Matthew ; Qi, Bolun ; Mitra, Sayan ; Viswanathan, Mahesh ; Bak, Stanley ; Bogomolov, Sergiy ; Johnson, Taylor T. ; Nguyen, Luan Viet ; Schilling, Christian ; Sogokon, Andrew ; Tran, Hoang Dung ; Xiang, Weiming. / 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 = "10",
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",

}

TY - GEN

T1 - Tutorial

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

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.

ER -