Cyber-Physical Systems I - Discrete Models

Description

• The students learn how to model cyber-physical systems as transition systems. Here, the main focus lies on software and hardware aspects of cyber-physical systems and on methods for modeling parallelism and communication.

• Moreover, the students learn how to express properties about such systems. The course covers different mechanisms to specify temporal properties including linear time properties and branching time properties such as LTL, CTL, and CTL* properties.

• Finally, the course demonstrates how to develop algorithms for checking whether these properties hold. After presenting algorithms for explicit state systems we introduce symbolic BDD-based algorithms which are able to tackle the well-known "state explosion problem". In addition, the course covers basic "Bounded Model Checking" (BMC) techniques which restrict the analysis to computation paths up to a certain length and reduce the verification problem to a Boolean satisfiability problem.

• All necessary foundations for these algorithms such as fixed point theory, data structures like binary decision diagrams (BDDs), and satisfiability (SAT) solvers are introduced in the course as well.

News 

• Sep. 14: The exam review (Klausureinsicht) for the summer term takes place on Monday, September 25, at 2 pm in room 00-016 of building 052.
• Aug 17: The exam in the summer term (2017) will be a written exam. We have the same rules as in the winter term (see Exam Section below).
  
• Mar. 27: The exam review (Klausureinsicht) takes place on Wednesday, April 19, from 2 pm to 3 pm in room 00-016 of building 052.
• Mar. 13: Most likely you will be able to see the exam results in the Campus Management system starting from some day between 22nd and 24th March. (However, there is some risk that we need more time for providing the results.)
  

• Feb. 08: Added information about the duration of the exam (90min)
  
• Feb. 06: Added information about material that you may bring to the exam (A4 sheet).
  
• Jan. 23: Exercise 2d on sheet 12 became a bonus exercise because the property which was given in natural language was not very precise.
  
• Dec. 04: New "WhithoutOverlay" version of slides available. This version is a compromise between the slides (which contain many overlay frames) and the handout (which is sometimes unreadable). Many thanks to Claus Schätzle for sharing his perl scripts that transform the slides.
  
• Nov. 30: There was a typo in Exercise 1 on sheet 7.
  
• Nov. 24: There was a mistake in sheet 6 (that was corrected yesterday evening): Instead of "bad prefix of minimal total length" we accidentally wrote "minimal bad prefix".
  
• Nov. 2: Exercise 2 on sheet 2 became a bonus exercise.
  
• Oct 27: The room for the group 2 tutorial was changed (see above).
  
• Oct, 21: Solutions for exercises have to be submitted via the post boxes that are located in the ground floor of building 051.
• Oct, 20: From now on Monday's lecture will be in room HS 00-026 in building 101.
  
• Oct, 19: You may submit your solutions of exercise sheets alone or in a group of two.
  
• Oct. 19: Until this evening the exercise groups on this website were accidentally listed in the wrong order. Please re-check the room number before you visit your exercise group.
  

• Oct. 18:

  • The application limit in the course management system (HisInOne) was raised from 80 to 100.
  • The groups have been assigned. To make the group size equal, we had to move some students from group 1 to group 2. If you want to change the group, please write a mail to Christian, ideally with a suitable candidate for swapping.

Exercises

Exam