Many of the (embedded) software systems we are confronted with in everyday life have time-critical functionalities. For example, an airbag should be activated within a certain, very short period of time in the event of an accident. We also expect fast response times from the various apps on our smartphones in order to use them conveniently and effectively.

Time" is therefore a decisive factor when modeling software systems. This lecture describes various mechanisms for formalizing so-called real-time systems. In addition to modeling, the lecture also focuses on the analysis of the systems. The following topics are covered in particular:

- Timed automata (an extension of finite automata by time)

- Model checking of timed automata with the help of UPPAAL

- Timed Games (two players try to achieve their own goals in a time-critical game)

- Interval Temporal Logic (a logic that talks about time intervals)

- Extensions and applications of Timed Systems

The weekly lecture consists of both theoretical and applied parts. The applied parts consist of voluntary exercises, which will be discussed in the lecture.