You are here: Home › Teaching › Summer Term 2013 › Real-Time Systems (Lecture)

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 51-03-026
Wednesday, 10:00–12:00, HS 51-03-026
Exercise Wednesday, 10:00–12:00, HS 51-03-026 (two-weekly)
First session Lecture 16.4.2013
Language of instruction English
Credits 6
Exams TBA
Course Catalog Real-Time Systems

 

 

Quicklinks: News - Formalia - Plan - Links & Literature

 

News

  • 2013-07-09: the notes on today's completion of the universality problem for TBA have been added to the slides of Lecture 16 - the slides of Lecture 17 are only about checking DC properties for TA
  • 2013-06-25: seems like the second half of today's lecture didn't get recordet, I'll repeat the essentials tomorrow
  • 2013-06-24: links to slides of Lecture 12 now yield the slides of Lecture 12
  • 2013-06-12: Exercise Sheet 4 updated again, has now 2 pages, 1.(ii) and (iii) explicated.
  • 2013-06-05: conducted an (unofficial) midterm evaluation - if you didn't participate yet, here is the form.  It would in particular be nice if you filled in the form if you left the course due to a reason you think we could improve.
  • 2013-06-04: Exercise Sheet 4 updated, now with correct dates (early submission is now open until 10:00 on Tuesday)
  • 2013-06-04: submission of exercise solutions is always before the tutorial, i.e. 10:00 on Wednesday - there is a mistake on the exercise sheets 3 and 4.
  • 2013-05-29: exam date decided (see below)
  • 2013-05-28: Exercise Sheet 3 updated, now with bonus task.
  • 2013-05-10: recordings now on the eLectures portal - the eLectures portal is updated first, this homepage may lag behind.
  • 2013-05-03: tutorials are now offered on Wednesday (instead of Tuesday) to allow as many students as possible to participate
  • 2013-04-22: added sources of Exercise Sheet 1 as example for usage of LaTeX style files
  • 2013-04-16: table above gave wrong time for exercise - now it's correct.

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

There will be an oral exam of length 30 min. for all,

  • dates: 19.+20.9.2013

Please contact the examination office for times.

 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, 16.4.: VL 01 "Introduction"
    Motivation, Overview, Formalia.
    (Slides (with annotations), 2-up, 6-up, Recording)
  • Mi, 17.4.: VL 02 "Timed Behaviour" + exercise sheet 1 online (sources)
    A formal representation of timed behaviour.
    (Slides (with annotations), 2-up, 6-up, Recording)
  • Di, 23.4.: VL 03 "Duration Calculus I"
    Symbols, state assertions, timing diagrams.
    (Slides (with annotations), 2-up, 6-up, Recording)
  • Mi, 24.4.: VL 04 "DC II" + exercise sheet 2 online
    Terms, formulae.
    (Slides (with annotations), 2-up, 6-up, Recording)
  • Mi, 1.5.: - (labour day) + exercise sheet 2 online (sources)
  • Do, 2.5.: Tutorial 1
  • Di, 7.5.: VL 05 "DC III"
    Substitution, valid/satisfiable/realisable
    (Slides (with annotations), 2-up, 6-up, Recording)
  • Mi, 8.5.: VL 06 "DC Properties I"
    Correctness proof; Decidable discrete time.
    (Slides (with annotations), 2-up, 6-up, Recording)
  • Di, 14.5.: VL 07 "DC Properties II"
    Undecidable dense time.
    (Slides (with annotations), 2-up, 6-up, Recording)
  • Mi, 15.5.: Tutorial 2
  • Di, 21.5.: - (whitsun break)
  • Mi, 22.5.: - (whitsun break)
  • Di, 28.5.: VL 08 "DC Implementables" + exercise sheet 3 online (sources)
    Implementables.
    (Slides (with annotations), 2-up, 6-up, Recording)
  • Mi, 29.5.: VL 09 "PLC Automata"
    An abstract view on programmable logic controllers.
    (Slides (with annotations), 2-up, 6-up, Recording)
  • Di, 4.6.: VL 10 "Timed Automata" + exercise sheet 4 online
    Basic Timed Automata.
    (Slides (with annotations), 2-up, 6-up, Recording)
  • Mi, 5.6.: Tutorial 3
  • Di, 11.6.: VL 11 "Networks of Timed Automata" + minibuffer model and queries
    Synchronisation, hiding, Uppaal-Demo.
    (Slides (with annotations), 2-up, 6-up, Recording)
  • Mi, 12.6.: VL 12 "Region Abstraction"
    Decidability of the reachability problem for timed automata.
    (Slides (with annotations), 2-up, 6-up, Recording)
  • Di, 18.6.: VL 13 "Zone Abstraction" + exercise sheet 5 online
    An alternative representation of sets of regions.
    (Slides (with annotations), 2-up, 6-up, Recording)
  • Mi, 19.6.: Tutorial 4
  • Di, 25.6.: VL 14 "Extended Timed Automata"
    Variables, and urgent and committed locations.
    (Slides (with annotations), 2-up, 6-up, Recording)
  • Mi, 26.6.: VL 15 "Timed Büchi Automata"
    An alternative automaton model with time.
    (Slides (with annotations), 2-up, 6-up, Recording)
  • Di, 2.7.: VL 16 "The Universality Problem for TBA" + exercise sheet 6 online
    Undedicable problems for automata with time.  
    (Slides (with annotations), 2-up, 6-up, Recording)
  • Mi, 3.7.: Tutorial 5
  • Di, 9.7.: VL 17 "Automated DC/PLC Verification I"
    How to automatically verify whether a PLC automaton satisfies a DC requirement.
    (Slides (with annotations), 2-up, 6-up, Recording)
  • Mi, 10.7.: VL 18 "Automated DC/PLC Verification II"
    How to automatically verify whether a PLC automaton satisfies a DC requirement.
    (Slides (with annotations), 2-up, 6-up, Recording)
  • Di, 16.7.: "Wrapup + Questions"
    (Slides (with annotations), 2-up, 6-up, Recording)
  • Mi, 17. 7.: Tutorial 6

Links & Literature