Real-Time Systems (Lecture)
Course type | Lecture |
---|---|
Instructors | Prof. Dr. Andreas Podelski, Dr. Bernd Westphal |
Lecture | Tuesday, 14:00–16:00, HS 82-00-006 (Kinohörsaal) Thursday, 14:00–16:00, HS 82-00-006 (Kinohörsaal) |
Exercise | Tuesday, 14:00–16:00, HS 82-00-006 (two-weekly) |
First session | Lecture 17.10.2017 |
Language of instruction | English |
Credits | 6 |
Exams | see below |
Course Catalog | Real-Time Systems (HISinOne) |
Quicklinks: News - Formalia - Plan - Links & Literature
News
- 2018-04-05: exam results available in HISinOne - exam review ('Klausureinsicht'): Thu, 12.4.2018, 14-16, room 52-00-020.
- 2018-02-01: this time, no sound at all with the recordings (always something new - batteries: ok, mic-to-speakers: ok, mic-to-computer: no...)
- 2018-01-25: tja, batteries let us down again (request for fix pending since 11.1.) - no sound after about 1h
- 2018-01-16, 18:11: tutorial notes re-uploaded with a new comment on 3.(ii).e)
- 2018-01-11: this time it's the battery - half of the recording comes without sound, sorry :-/ (should be fixed by next Thu)
- 2017-12-05: this year's last lecture will be from 12:00 to 14:00 on 21.12.
- 2017-11-16: somebody forgot to re-start the recording after the break so today we only have about the last half of the second half of the lecture on the recording, sorry about that; this happens at least once every season, the named, anonymous "somebody" is still trying to figure out how to systematically avoid this kind of error... :-/
- 2017-11-09: sample solution for 7.11. updated (in ILIAS) to include today's discussion of "realisability"
- 2017-11-07: date/time for the written exam has been fixed (see below) - BSc candidates (who need an oral exam) please contact me directly to negotiate dates for the oral exams.
- 2017-11-05: in case of ILIAS-problems, you can contact / submit by mail to Liridon using
liridon<AT>informatik.uni-freiburg.de - 2017-11-02: exam date and form will be decided on 7.11. - mid/late March is on offer
- 2017-10-16: the corresponding ILIAS course is available, join via this direct link.
- 2017-10-12: this homepage online
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
- Date & time: Thursday, March 15th, 2018 - 14:00 c.t.
- 90 min.
- Room: Building 101, HS 00 026 (µ - SAAL)
- Permitted exam aids: "one sheet A4, all sides may be used"- cf. ILIAS forum post.
Note: The module result (grade, "Note") is completely determined by the exam.
Resources
Slides, Exercises, and Recordings
- Di, 17.10.: VL 1 "Introduction"
+ exercise sheet 1 online (submit via ILIAS)
Motivation, Overview, Formalia.
(Slides (with annotations), 2-up, 6-up, Recording: ILIAS-Download, ILIAS-Stream) - Do, 19.10.: VL 2 "Timed Behaviour"
A formal representation of timed behaviour.
(Slides (with annotations), 2-up, 6-up, Recording: ILIAS-Download, ILIAS-Stream) - Di, 24.10.: Tutorial 1
- Do, 26.10.: VL 3 "Duration Calculus I"
+ exercise sheet 2 online (submit via ILIAS)
Symbols, state assertions, timing diagrams, terms.
(Slides (with annotations), 2-up, 6-up, Recording: ILIAS-Download, ILIAS-Stream) - Di, 31.10.: - (public holiday)
- Do, 2.11.: VL 4 "DC II"
Formulae, substitution lemma, abbreviations.
(Slides (with annotations), 2-up, 6-up, Recording: ILIAS-Download, ILIAS-Stream) - Di, 7.11.: Tutorial 2
- Do, 9.11.: VL 5 "DC III"
+ exercise sheet 3 online (submit via ILIAS)
Valid / satisfiable / realisable, semantical proof of correctness.
(Slides (with annotations), 2-up, 6-up, Recording: ILIAS-Download, ILIAS-Stream) - Di, 14.11.: VL 6 "DC Properties I"
A calculus for DC (brief outlook); decidable discrete time.
(Slides (with annotations), 2-up, 6-up, Recording: ILIAS-Download, ILIAS-Stream) - Do, 16.11.: VL 7 "DC Properties II"
Undecidable continuous time.
(Slides (with annotations), 2-up, 6-up, Recording: ILIAS-Download, ILIAS-Stream) - Di, 21.11.: Tutorial 3
- Do, 23.11.: VL 8 "DC Implementables I"
+ exercise sheet 4 online (submit via ILIAS)
Standard forms, implementables.
(Slides (with annotations), 2-up, 6-up, Recording: ILIAS-Download, ILIAS-Stream) - Di, 28.11.: VL 9 "DC Implementables II"
Example: controller design for the gas burner.
(Slides (with annotations), 2-up, 6-up, Recording: ILIAS-Download, ILIAS-Stream) - Do, 30.11.: VL 10 "PLC Automata"
Programmable logic controllers, from DC implementables to PLC programs.
(Slides (with annotations), 2-up, 6-up, Recording: ILIAS-Download, ILIAS-Stream) - Di, 5.12.: Tutorial 4
- Do, 6.12.: VL 11 "Timed Automata"
+ exercise sheet 5 online (submit via ILIAS)
Basic Timed Automata, computation path, run.
(Slides (with annotations), 2-up, 6-up, Recording: ILIAS-Download, ILIAS-Stream) - Di, 12.12.: VL 12 "Networks of Timed Automata"
Synchronisation, hiding, Uppaal-Demo I.
(Slides (with annotations), 2-up, 6-up, Recording: ILIAS-Download, ILIAS-Stream) -
Do, 14.12.: VL 13 "Region Abstraction"
Decidability of the reachability problem for basic timed automata.
(Slides (with annotations), 2-up, 6-up, Recording: ILIAS-Download, ILIAS-Stream) - Di, 19.12.: Tutorial 5
- Do, 21.12.: VL 14 "Zone Abstraction"
+ exercise sheet 6 online (submit via ILIAS)
An alternative representation of sets of regions; DBMs.
(Slides (with annotations), 2-up, 6-up, Recording: ILIAS-Download, ILIAS-Stream) - Di, 9. 1.: VL 15 "Extended Timed Automata"
Semantics of Extended Timed Automata (data variables, urgent and committed locations).
(Slides (with annotations), 2-up, 6-up, Recording: ILIAS-Download, ILIAS-Stream) - Do, 11. 1.: VL 16 "Automated DC Verification for TA"
Uppaal query language, Uppaal demo II.
(Slides (with annotations), 2-up, 6-up, Recording: ILIAS-Download, ILIAS-Stream) - Di, 16. 1.: Tutorial 6
- Do, 18. 1.: VL 17 "Automated DC Verification for TA II"
+ exercise sheet 7 online (submit via ILIAS)
Testable and untestable DC formulae, observer construction.
(Slides (with annotations), 2-up, 6-up, Recording: ILIAS-Download, ILIAS-Stream) - Di, 23. 1.: VL 18 "TA Properties"
Timed Büchi Automata; some undecidability results ("beyond timed regular").
(Slides (with annotations), 2-up, 6-up, Recording: ILIAS-Download, ILIAS-Stream) - Do, 25. 1.: VL 19 "Quasi-Equal Clocks"
Quasi-equality of clocks; network transformation; correctness by bisimulation; case-studies.
(Slides (with annotations), 2-up, 6-up, Recording: ILIAS-Download, ILIAS-Stream) - Di, 30. 1.: Tutorial 7
- Do, 1. 2.: VL 20 "Formal Methods for Timed Systems in SME-Contexts"
The wireless fire alarm system project: requirements clarification; modelling; analysis;
process aspects in Small to Medium-sized Enterprises (SME).
(Slides (with annotations), 2-up, 6-up, Recording: ILIAS-Download, ILIAS-Stream) - Di, 6. 2.: VL 21 "Wrap-up and Questions"
The WFAS project (Lect. 20) continued; dependency on global scheduling (brief); wrapup.
(Slides (with annotations), 2-up, 6-up, Recording: ILIAS-Download, ILIAS-Stream) - Do, 8. 2.: no lecture
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.)
- E.-R. Olderog, H. Dierks: Real-Time Systems, Cambridge University Press, 2008.
- 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)
- See sources of execise sheets above for examples of usage.