In this seminar we address foundations, applications and tools for the safety analysis of hybrid systems.
What are hybrid systems?
Hybrid systems are systems with mixed discrete and continuous behaviour. Typical examples are physical systems which continuously evolve over time and are controlled by some discrete controller, e.g., a chip or a computer.
Why modeling and analysis?
The behaviour of hybrid systems is often safety-critical. For example, in case of an accident an airbag can save the life of the car driver, but only if the airbag reacts in time. To assure the correct functioning of such safety-critical hybrid systems, their automatic synthesis and analysis is of high importance.
Times
- Introductory Meeting: 15-17.10.2014
- Complete the structure of your paper by 07.11.2014
- Complete the first version of your seminar paper by 28.11.2014
- Complete the final version of your seminar paper by 12.12.2014
- Complete the first version of your slides by 07.01.2015
- Complete the final version of your slides by 19.01.2015
- Seminar: 02-06.02.2015
(The exact times for the introduction meeting and seminar will be later decided by doodles.)
Topics
- Flow*: An Analyzer for Non-Linear Hybrid Systems. X. Chen, E. Abraham and S. Sankaranarayanan.
- dReal: An SMT Solver for Nonlinear Theories over the Reals. S. Gao, S. Kong and E. M. Clarke.
- SAT Modulo ODE: A Direct SAT Approach to Hybrid Systems. A. Eggers, M. Fränzle, and C. Herde.
- Computation Platform for Automatic Analysis of Embedded Software Systems Using Model Based Approach. A. Dubey, X. Wu, H. Su and T. J. Koo.
- The algorithmic analysis of hybrid systems. R. Alur, C. Courcoubetis, N. Halbwachs, T. A. Henzinger, P.-H. Ho, X. Nicollin, A. Olivero, J. Sifakis and S. Yovine.
- Symbolic model checking of hybrid systems using template polyhedra. S. Sankaranarayanan, T. Dang, F. Ivančić.
- Reachability Analysis of Hybrid Systems via Predicate Abstraction. R. Alur, T. Dang and F Ivančić.
- Reachability of uncertain linear systems using zonotopes. A. Girard.