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
N1 - Publisher Copyright:
© 2016 IEEE.
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 -