In this seminar we address foundations, applications and tools for the safety analysis of 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. 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.

Prerequisites
Participants should be interested in algorithmic aspects of theoretical computer science, and should possess basic knowledge in the area of formal methods (for example from courses on “Satisfiability Checking”, “Modeling and Analysis of Hybrid Systems”, “Model Checking”, “Logic Programming”, “Functional Programming”, “Term Rewriting” etc.).

Requirements
You will work out a written document (seminar paper) and give a presentation about a scientific topic. The seminar paper should have 10 pages and be written in either English or German. You do not need to provide an index or table of contents, but attach a list of references. You can find templates for your paper here.
The presentations will be given in either English or German, use slides and should have a duration of 20 minutes.

Dates
The seminar will take place as a block seminar at the end of the semester.
04.11.2016 Contact your supervisor to obtain and discuss relevant literature.
18.11.2016 Read and understand your primary sources, if needed, obtain more literature. Discuss a rough sketch of your seminar paper with your supervisor.
09.12.2016 Complete your seminar paper (10 pages including title and references, English or German) and send it to your supervisor to get comments for improvements. Please use a spell checker!
23.12.2016 Send the final version of your seminar paper (pdf) to your supervisor such that it can be made available on the seminar’s web page.
20.01.2017 Prepare your talk and send your slides to your supervisor to get comments for improvements.
03.02.2017 Send the final version of your slides (pdf) to your supervisor such that it can be made available on the seminar’s web page.
14.03.2017 (start: 9am, location: I2 seminar room) Presentation

Topics

• Support functions as state set representations (Lange, supervision: Schupp)
• Zonotopes as state set representations (Alexandrov, supervision: Schupp)
• Guaranteeing over-approximation in hybrid systems reachability analysis (Petrushkov, supervision: Schupp)
• Undecidability of hybrid systems reachability analysis (Mughis, supervision: Schupp)
• Transformation of SFCs to hybrid automata (Ahmed, supervision: Nellen)
• Rigorous simulation (Gomaa, supervision: Nellen)
• Transformation of Simulink models to hybrid automata (Mahadevan, supervision: Nellen)

Contact and supervisors
For further details please contact Stefan Schupp.
Further instructors are Prof. Dr. Erika Ábrahám, Gereon Kremer, Johanna Nellen.