Real-Time Systems (Vorlesung)

Quicklinks: News - Submission - Formalia - Links, Literature & Ressources - Plan

News

• 2009-08-31: announced exam place (room 00-017, building 52)
  
• 2009-07-06: again a mild rearrangement of the plan
  
• 2009-07-01: the bonus on exercise sheet 05 is only granted if the solution to this taks is submitted before Wed, 8.7., 09:00 local time (because the solution may be subject of lecture 15).
  
• 2009-06-22: split LaTeX style file for DC symbols into two, one for DC only and one for timing diagrams (see Ressources below)
  
• 2009-06-10: we want to conduct an evaluation on 2009-06-17 (next Wednesday) - if you want to tell us anything (negative or even positive), please come and do so, there's still plenty of time for changes in the second half of the lecture
  
• 2009-05-28: fixed slides for lecture 07, missing negation in (Syn-1)
  
• 2009-05-28: apparently, the CMS has been restored from the backup to a state from four days ago; we tried to remember the changes to this page, please notify us if something is missing that was there a few days ago.
  
• 2009-05-26: rearranged plan mildly
  
• 2009-05-20: no recording, no handwritten annotations today, the beamer refused to work; the proofs we presented can be found in the book (note: sometimes it's [c,d], not [b,e])
  
• 2009-05-11: mistake in Exercise 02.3 fixed (should be "<> F = true ; (F ; true)")
  
• 2009-05-06: restored annotations of lecture 03 slides from recording
  
• 2009-05-06: on popular request a LaTeX style file with the DC symbols I use to prepare the slides (partly (c) J. Hoenicke, see Ressources below)
  
• 2009-05-01: the plan now considers the public holidays
  
• 2009-04-29: unfortunately, I seem to have lost (or not saved) the slides with handwritten annotations; I'll try to reconstruct at least the fixes from the recording
  
• 2009-04-21: room change, now in 051-00-031 on Wednesday
  
• 2009-04-01: on popular request, date and location of one lecture changed, please see Dates and Times below. If this change is a problem for you, contact us soon.
  

Exercise Submission Scheme

• new exercise sheets typically appear on Wednesday, after the lecture
• early submission deadline is 24h before the tutorial,
  so typically 9:00 of the next Wednesday after hand-out
• regular submission deadline is right before the corresponding tutorial,
  so typically 9:00 of the second Thursday after hand-out
  

Formalia

On popular demand, the exam will be in oral form.

Exam dates and times for which you can apply by mail.
Times in brackets are already assigned (there may be additional times on Tuesday morning):

• Tuesday, 1.9. (13:15, [14:00], [14:45], [15:30]) and
• Thursday, 3.9. ([10:00], [10:45], [11:30], [14:00], [14:45], [15:30]).
  

Admission criteria for the final exam have been announced in the first lecture.

Links, Literature & Ressources

• Textbooks
  • E.-R. Olderog, H. Dierks: Real-Time Systems, Cambridge University Press, 2008.
    The lecture is mostly based on material from this book.
• 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.
    
• Ressources
  • Typesetting DC symbols (LaTeX style file)
    
  • Typesetting Timing Diagrams (LaTeX style file)
    

Plan

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.

Regarding the recordings provided on the Electure portal, the TechSmith Screen Capture Codec seems to be necessary for playback.

• Wed, 22.4.: VL 01 "Introduction, Formalia"
  (Slides, 2-up, Electure)
• Thu, 23.4.: VL 02 "Timed Behaviour, Duration Calculus I"
  (Slides (with annotations), 2-up, Electure)
• Wed, 29.4.: VL 03 "DC cont'd" + Hand-out Exercise Sheet 1 (Exercises)
  (Slides (with annotations), 2-up, Electure)
• Thu, 30.4.: VL 04 "Correctness Proofs with DC"
  (Slides (with annotations), 2-up, Electure)
• Wed, 6.5.: VL 05 "DC Proof Systems" + Hand-out Exercise Sheet 2 (Exercises, corrected)
  (Slides (with annotations), 2-up, Electure)
• Thu, 7.5.: Tutorial 1
• Wed, 13.5.: VL 06 "DC Properties"
  (Slides (with annotations), 2-up, Electure)
• Thu, 14.5.: Tutorial 2
• Wed, 20.5.: VL 07 "DC Implementables" + Hand-out Exercise Sheet 3 (Exercises)
  (Slides (without annotations, see news), 2-up, no recording (see news))
• Thu, 21.5.: general holiday ("Christi Himmelfahrt")
  
• Wed, 27.5.: VL 08 "PLC-Automata"
  (Slides (with annotations), 2-up, Electure)
• Thu, 28.5.: Tutorial 3
• Wed, 3.6.: Whitsun break
• Thu, 4.6.: Whitsun break
• Wed, 10.6.: VL 09 "DC Semantics for PLC Automata"
  (Slides (with annotations), 2-up, Electure)
• Thu, 11.6.: general holiday ("Fronleichnam")
• Wed, 17.6.: VL 10 "Timed Automata" + Hand-out Exercise Sheet 4 (Exercises)
  (Slides (with annotations), 2-up, Errata, Electure)
• Thu, 18.6.: VL 11 "Timed Automata of Uppaal"
  (Slides (with annotations), 2-up, Electure)
• Wed, 24.6.: VL 12 "Decidabilty Results"
  (Slides (with annotations), 2-up, Electure)
• Thu, 25.6.: Tutorial 4
• Wed, 1.7.: VL 13 "Constraint Reachability and Zones" + Hand-out Exercise Sheet 5 (Exercises, updated)
  (Slides (with annotations), 2-up, Electure)
• Thu, 2.7.: VL 14 "Live Sequence Charts"
  (Slides (with annotations), 2-up, Electure)
• Wed, 8.7.: VL 15 "The TBA-Semantics of LSCs"
  (Slides (with annotations), 2-up, Electure)
• Thu, 9.7.: Tutorial 5
• Wed, 15.7.: VL 16 "WCET Estimation (Martin Mehlmann)" + Hand-out Exercise Sheet 6 (Exercises)
  (Slides (with annotations), 2-up, Electure)
• Thu, 16.7.: VL 17 "Observer-based LSC-Verification"
  (Slides (with annotations), 2-up, Electure)
• Wed, 22.7.: VL 18 "Automated DC/PLC-Verification and Recap"
  (Slides (with annotations), 2-up, Electure)
• Thu, 23.7.: Tutorial 6

• Instructors: Bernd Westphal
• Times & Locations: Wed, 9.00 - 11.00, SR 00-031, Geb. 051 | Thu, 9.00 - 10.00, SR 00-007, Geb. 106
• Tutors: Daniel Dietsch | Sergio Feo Arenis
• Times & Locations of tutorials: Thu, 10.00 - 11.00, SR 00-007, Geb. 106