Theoretische Informatik I und II

The students learn about methods and tools, and how to apply, specify, simulate, verify, and implement real-time systems (RTS). The students gain hands-on experience using tangible Mini-Robots (Lego Mindstorms).

Professional competence
The students:

• implement RTS with Lego Mindstorm Robots NXT
• simulate and verify RTS on the basis of real-time automata with the model checker UPPAAL
• apply the tool Moby/RT to specify and simulate RTS on the basis of PLC-Automata, and to translate them into Java-Code for Lego Mindstorms NXT and into UPPAAL

Methodological competence
The students:

• realise control tasks with Lego Mindstorms
• specify RTS as networks of real-time automata and verify them with UPPAAL
• design RTS using Moby/RT
• realise systematically sophisticated time-dependent control tasks with Moby/RT, Lego Mindstorms, and UPPAAL

Social competence
The students:

• solve tasks in a team
• present solutions and discuss them

Self-competence
The students:

• recognise (sub-)problems of RTS and are responsible for their realisation

Real-time-systems are systems, where the time at which an output is generated or at which data are read is of importance. Compared to usual programming methods, RTS models are extended by the additional dimension of time. An example for a RTS is an airbag in a car, which needs to be triggered at the right moment of time, not too early and not too late, because the effect of the airbag is useful only for a few hundredths of seconds.

The course introduces methods and tools which are then practically applied to specify, verify, and implement RTS.
The students gain hands-on experience using Mini-Robots (Lego-Mindstorms) to implement RTS.

E.-R. Olderog, H. Dierks: Real-Time Systems: Formal Specification and Automatic Verification, Cambridge University Press, 2008

At the end of the lecture period

exercises