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 case of an accident. Similarly, we expect fast response times from the various apps on our smartphones in order to use them conveniently and in a goal-oriented manner.

Thus, "time" is a crucial factor when modeling software systems. This lecture describes different mechanisms to formalize so-called real-time systems. In addition to modeling, the lecture also focuses on the analysis of the systems. In particular, the following topics are covered:

• Timed Automata (an extension of finite automata by time)
• Model checking of timed automata using 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 portions. The applied parts consist of optional exercises that will be discussed during the lecture.