|Module label||Real-Time Systems|
|Credit points||6.0 KP|
|Institute directory||Department of Computing Science|
|Applicability of the module||
Lehrenden, Die im Modul (Authorized examiners)
Olderog, Ernst-Rüdiger (Authorized examiners)
|Skills to be acquired in this module||
Introduction to formal methods of the specification and verification of time sensitive systems and their combinations.
Examples of time-critical systems are railway control systems, robots, or even gas burners. It is essential for these systems to comply with certain timing conditions. For example, the control of a railway crossing must close the gates not later than 4 seconds after the sensors have reported an approaching train. If the gates are open, they should stay that way for at least 15 seconds to allow for a safe crossing of vehicles.
Different specification methods have been developed to describe such timing conditions.
The Duration Calculus developed by Zhou Chaochen in 1991 is one attractive method. It is a logic combined with a calculus, in which the duration of states can be described. The course will introduce the Duration Calculus and will explain its application by means of examples. As further specification method Timed Automata introduced by Alur & Dill in 1994 will be presented. After the specification of real-time system requirements the verification of programs implementing these requirements will follow. The specification methods of the Duration Calculus and Timed Automata are used to describe the real-time behaviour of these programs. The correctness is then proven on the basis of these behavioral descriptions.
|Languages of instruction||German, English|
|Duration (semesters)||1 Semester|
|Modullevel / module level||AS (Akzentsetzung / Accentuation)|
|Modulart / typ of module||Pflicht o. Wahlpflicht / compulsory or optioal|
|Lehr-/Lernform / Teaching/Learning method||V+Ü|
|Vorkenntnisse / Previous knowledge||Theoretische Informatik I + II|
|Course type||Comment||SWS||Frequency||Workload of compulsory attendance|
|Lecture||3||SoSe oder WiSe||42|
|Exercises||1||SoSe oder WiSe||14|
|Total time of attendance for the module||56 h|
|Examination||Time of examination||Type of examination|
|Final exam of module||
At the end of the lecture period
Exercises and written or oral exam