inf456 - Real-Time Systems (Complete module description)

inf456 - Real-Time Systems (Complete module description)

Original version English PDF Download
Module label Real-Time Systems
Modulkürzel inf456
Credit points 6.0 KP
Workload 180 h
Institute directory Department of Computing Science
Verwendbarkeit des Moduls
  • Master's Programme Computing Science (Master) >
  • Master's Programme Engineering of Socio-Technical Systems (Master) >
  • Master's Programme Engineering of Socio-Technical Systems (Master) >
Zuständige Personen
  • Olderog, Ernst-Rüdiger (module responsibility)
  • Lehrenden, Die im Modul (Prüfungsberechtigt)
Prerequisites

Theoretical Computer Science I + II

Skills to be acquired in this module

Introduction to formal methods of the specification and verification of time sensitive systems and their combinations.
Professional competence 
The students:

  • learn about different models of time and real-time properties
  • specify and verify real-time systems
  • model real-time systems using Timed Automata and PLC-Automata
  • apply the model checker UPPAAL for the verification of real-time properties
  • specify real-time systems using the Duration Calculus
  • learn about decidability and undecidability results for real-time systems

Methodological competence
The students:

  • recognize logic and automata as adequate forms for describing real-time systems

Social competence
The students:

  • work together in small groups to solve problems
  • present their solutions to groups of other students

Self-competence
The students:

  • learn persistence in pursuing difficult tasks
  • learn precision in specifying problems
Module contents

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.
Topics:

  • discrete and continuous model of time
  • logics and automata models for the specification of real-time systems (predicate logic, Duration Calculus, Timed CTL, Timed Automata, PLC-Automata)
  • decidability and undecidability results for real-time systems
  • model checker UPPAAL for Timed Automata
  • formal specification of real-time systems using Duration Calculus as well as Timed Automata and PLC-Automata
  • verification of concrete Timed Automata using the model checker UPPAAL,
  • transformation of Duration Calculus for discrete time into regular languages
  • implementability of real-time systems on PLC-like hardware
Literaturempfehlungen

Essential: 

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

Recommended:

  • C. Heitmeyer and D. Madrioli, editors. Formal Methods for Real-Time Computing, Wiley, 1996.
  • M. Joseph, editor. Real-time Systems -- Specification, Verification and Analysis, Prentice Hall, 1996 (siehe http://docencia.etsit.urjc.es/moodle/file.php/31/documentos/RTSbook.pdf ).
Links
Languages of instruction German, English
Duration (semesters) 1 Semester
Module frequency irregular
Module capacity unlimited
Teaching/Learning method V + Ü
Previous knowledge Theoretical Computer Science I + II
Form of instruction Comment SWS Frequency Workload of compulsory attendance
Lecture 3 SoSe oder WiSe 42
Exercises 1 SoSe oder WiSe 14
Präsenzzeit Modul insgesamt 56 h
Examination Prüfungszeiten Type of examination
Final exam of module

At the end of the lecture period

Exercises and written or oral exam