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


Author(s): Duggirala, Parasara S; Fan, Chuchu; Potok, Matthew; Qi, Bolun; Mitra, Sayan; Viswanathan, Mahesh; Bak, Stanley; Bogomolov, Sergiy V; Johnson, Taylor T; Nguyen, Luan V; Schilling, Christian; Sogokon, Andrew; Tran, Hoang D; Xiang, Weiming
Title: Tutorial: Software tools for hybrid systems verification transformation and synthesis C2E2 HyST and TuLiP
Affiliation IST Austria
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. © 2016 IEEE.
Conference Title: CCA: Control Applications
Conference Dates: September 19-21, 2016
Conference Location: Buenos Aires, ARG
ISBN: 978-150900755-4
Publisher: IEEE  
Date Published: 2016-10-10
Start Page: 1024
End Page: 1029
DOI: 10.1109/CCA.2016.7587948
Open access: no
IST Austria Authors
Related IST Austria Work