« December 2017 »
December
MoTuWeThFrSaSu
123
45678910
11121314151617
18192021222324
25262728293031
Uni-Logo
You are here: Home Teaching Winter Term 2017/18 Real-Time Systems (Lecture)
Document Actions

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, 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

  • 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: tba.
  • Permitted exam aids: to be negotiated (somewhere between "one sheet A4, all sides handwritten" (preparation of such notes is usually a good preparation for the exam as such) and "anything not alive or electronic" (may trick oneself into "ach, it's all there, I can look it up in the books" - there's usually not too much time for extensive book searches during the exam))

 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.

 

  • 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; Uppaal query language, Uppaal demo II.
    (preliminary Slides, 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 PLC/DC Verification"
    Testable and untestable DC formulae, observer construction.
    (Slides (with annotations), 2-up, 6-up, Recording: ILIAS-Download, ILIAS-Stream)
  • Di,  16. 1.: Tutorial 6
  • Do, 18. 1.: VL 17 "TA Properties I" + exercise sheet 7 online (submit via ILIAS)
    Timed Büchi Automata; some undecidability results ("beyond timed regular").
    (Slides (with annotations), 2-up, 6-up, Recording: ILIAS-Download, ILIAS-Stream)
  • Di,  23. 1.: VL 18 "tba"
  • Do, 25. 1.: VL 19 "tba"
  • Di,  30. 1.: VL 20 "tba"
  • Do,   1. 2.: VL 21 "tba"
  • Di,   6. 2.: Tutorial 7 + "Wrapup + Questions"
    (Slides (with annotations), 2-up, 6-up, Recording: ILIAS-Download, ILIAS-Stream)
  • Do,  8. 2.: tba

Links & Literature

Personal tools