Real-Time Systems (Lecture)

Real-time systems need to react to certain input stimuli within given time bounds. For example, an airbag in a car has to unfold within 300 milliseconds in a crash. There are many embedded safety-critical applications and each requires real-time specification techniques. We will study and apply some of these techniques, based on logic and automata, most prominently timed automata.

Course type	Lecture
Instructors	Prof. Dr. Andreas Podelski, Dr. Bernd Westphal
Lecture	Tuesday, 10:00–12:00, HS 51-03-026 Thursday, 10:00–12:00, HS 51-03-026
Exercise	Thursday, 10:00–12:00, HS 51-03-026 (two-weekly)
First session	Lecture 29.4.2014
Language of instruction	English
Credits	6
Exams	TBA
Course Catalog	Real-Time Systems (HISinOne)

Quicklinks: News - Formalia - Plan - Links & Literature

News

2014-05-08: fixed links for stylefiles in Resources below, added sources of Exercise Sheet 01
2014-03-14: homepage

Formalia

Prerequisites for admission to the final exam, form of the final exam, and everything will be announced in the first lecture.

Admission criteria

50% of the total admission (or: good will) points in the exercises are sufficient for exam admission. (For example, perfect solutions to exercise sheets 1, 3, 5, and 7 and no solutions to 2, 4, and 6 would satisfy this requirement; so would 50% of the points in each exercise).

Exercise Submission Scheme

The exercise sheets are online early in order to allow you to be aware of the tasks while following the lecture. There will be an early/regular submission scheme following a pattern to be announced.

Note: The exercises will be rated on two scales: admission points (given your knowledge before the tutorial, how sensible is your proposal; "good will rating", "upper bound") and exam points (given the additional knowledge from the comments on your proposal and the tutorial, how many points would your proposal at least be worth in a written exam; "evil rating", "lower bound").

Exam

tba.

Note: The module result (grade, "Note") is completely determined by the exam.

Resources

Slides, Exercises, and Recordings

Note: the following plan is tentative

in the sense that the assignment of topics to dates is subject to change depending on the flow of the lecture. The assignment of form (lecture or tutorial) to dates is fixed. Slides will be typically only provided after the lecture.

Note: the TechSmith Screen Capture Codec seems to be necessary for playback of the recordings provided on the Electure portal.

Di, 29.4.: VL 01 "Introduction"
Motivation, Overview, Formalia.
(Slides (with annotations), 2-up, 6-up, Recording)
Do, 1.5.: - (labour day)
Di, 6.5.: VL 02 "Timed Behaviour" + exercise sheet 1 online (sources)
A formal representation of timed behaviour.
(Slides (with annotations), 2-up, 6-up, Recording)
Do, 8.5.: VL 03 "Duration Calculus I"
Symbols, state assertions, timing diagrams.
(Slides (with annotations), 2-up, 6-up, Recording - preliminary slides)
Di, 13.5.: Tutorial 1
Do, 15.5.: VL 04 "DC II" + exercise sheet 2 online (sources)
Terms, formulae.
(Slides (with anotations), 2-up, 6-up, Recording - preliminary slides)
Di, 20.5.: VL 05 "DC III"
Substitution, valid/satisfiable/realisable
(Slides (with annotations), 2-up, 6-up, Recording, preliminary Slides)
Do, 22.5.: VL 06 "DC Properties I"
Correctness proof; Decidable discrete time.
(Slides (with annotations), 2-up, 6-up, Recording, preliminary Slides)
Di, 27.5.: Tutorial 2
Do, 29.5.: - (ascension day)
Di, 3.6.: VL 07 "DC Implementables" + exercise sheet 3 online (sources)
Implementables.
(Slides (with annotations), 2-up, 6-up, Recording, preliminary Slides)
Do, 5.6.: VL 08 "DC Implementables II"
Implementables cont'd.
(Slides (with annotations), 2-up, 6-up, Recording, preliminary Slides)
Di, 10.6.: - (whitsun break)
Do, 12.6.: - (whitsun break)
Di, 17.6.: Tutorial 3
Do, 19.6.: - (corpus christi)
Di, 24.6.: VL 09 "DC Properties IIa"
Undecidable dense time.
(Slides (with annotations), 2-up, 6-up, Recording)
Do, 26.6.: VL 10 "DC Properties IIb"
Undecidable dense time.
(Slides (with annotations), 2-up, 6-up, Recording)
Di, 1.7.: VL 11 "Timed Automata" + exercise sheet 4 online
Basic Timed Automata.
(Slides (with annotations), 2-up, 6-up, Recording, preliminary Slides)
Do, 3.7.: VL 12 "Networks of Timed Automata"
Synchronisation, hiding, Uppaal-Demo.
(Slides (with annotations), 2-up, 6-up, Recording, preliminary Slides)
Di, 8.7.: Tutorial 4
Di, 15.7.: VL 13 "Region Abstraction" + exercise sheet 5 online
Decidability of the reachability problem for timed automata.
(Slides (with annotations), 2-up, 6-up, Recording, preliminary Slides)
Do, 17.7.: VL 14 "Zone Abstraction"
An alternative representation of sets of regions; Extended Timed Automata syntax.
(Slides (with annotations), 2-up, 6-up, Recording, preliminary Slides)
Di, 22.7.: Tutorial 5
Do, 24.7.: VL 15 "Extended Timed Automata" + exercise sheet 6 online
Semantics of Extended Timed Automata (Variables, and urgent and committed locations); the logic of Uppaal; testable DC properties.
(Slides (with annotations), 2-up, 6-up, Recording, preliminary Slides)
Di, 29.7.: VL 16 "PLC Automata, Timed Büchi Automata"
Undedicable problems for automata with time.
(Slides (with annotations), 2-up, 6-up, Recording, preliminary Slides)
Do, 31.7.: Tutorial 6 + "Wrapup + Questions"
An abstract view on programmable logic controllers.
(Slides (with annotations), 2-up, 6-up, Recording)

Links & Literature

Textbooks
- E.-R. Olderog, H. Dierks: Real-Time Systems, Cambridge University Press, 2008.
  The lecture is mostly based on material from this book.
  (Errata on the author's homepage; the book is also available as an eBook in the UB.)
Papers
- G. Behrmann, A. David, K. G. Larsen: A Tutorial on Uppaal, Technical Report, 2004.
- R. Alur, D. Dill: A theory of timed automata, TCS, 126(2):183-235, 1994.
Resources
- Typesetting DC symbols (LaTeX style file)
- Typesetting Timing Diagrams (LaTeX style file)