Cyber-Physical Systems I - Discrete Models

The CPS I exam has been rescheduled for May 07, 09:00 - 12:00. More details below.

CPS Exam in times of Corona

The CPS I exam has been rescheduled to Thursday, May 07, 9:00-12:00. Please read the follwing organizational details carefully.

• The exam will take place in building KG II in the city center, not as originally scheduled on the TF campus. We will have the rooms 2004 and 2006, the entrances are in the big foyer right when you enter the building.
• The exam conditions will remain the same: You have 90 min to answer the questions, one A4 sheet of handwritten notes is permitted.
• Due to the Corona situation, the uni has put in place special measures and rules:
  • Please keep your distance while waiting for entrance, and after the exam as well.
  • You can find a declaration for students participating in exams under the current conditions here. Check this declaration carefully, and if all conditions apply to you, you must bring a signed copy of the declaration in order to participate in the exam.
  • If one of the conditions does not apply to you, you cannot participate in the exam. In this case, or if for other reasons you cannot participate (e.g. travel restrictions), please contact the examination office immediately.
  • It is mandatory to wear a mask or some other nose-mouth cover when entering and exiting the exam rooms. If you do not have such a nose-mouth cover, we cannot allow you to enter the exam rooms. You can take it off once you reached your seat.

News

• Apr 30: Additional details of the rescheduled exam have been added (see above).
  
• Apr 08: The exam has been rescheduled for the May 07, 09:00 - 12:00.
  
• Mar 13: The university has canceled all exams until April 19 to protect students and employees from Corona virus infections (http://www.uni-freiburg.de/universitaet/corona). Hence, there will be no CPS I exam today.
  

• Feb 05: The last exercise sheet, exercise sheet 15, is now available. Please submit this exercise sheet by Monday, February 10. The submissions will be graded and returned to you in the next and final lecture, on February 12.

  This last lecture will be used to discuss the solution to the exercise sheet, to discuss the results of the lecture evaluation, and to answer your questions on the lecture content.

• Dec 19: News on the situation after the holidays:
  • There will be no exercise session on Monday January 06, due to a public holiday.
  • There will be a lecture on Wednesday January 08, as usual.
  • The next exercise session will be on Monday January 13. In this exercise session, exercise sheet 9 (submitted by December 18) will be discussed.
  • There will be an additional exercise session on Wednesday January 15, 16:00 - 18:00, instead of a lecture. In this exercise session, exercise sheet 10 (submitted by January 08) will be discussed. The exercise session will take place in the following rooms:
    
    • Group 1 (Enid) will meet in room 00-026 in building 101, as always.
    • Group 2 (Mehdi) will meet in room 00-031 in building 051. (NOTE: different building!)
    • Group 3 (Miriam) will meet in room 01-009/013 in building 101.
• Dec 04: Early warning: There will be an exercise sheet published on December 18 which will have to be submitted by January 8. The exercise sessions in the first week after the break will be moved to a different day, as Monday (January 6) is a holiday. More details to follow.
  
• Nov 13: Due to illness, the lecture for today is canceled.
• Nov 04: The registration for the Studienleistung for this lecture (11LE13SL-2070) is now open. You must register for it in HisInOne in order to receive credit for your exercise points and pass the unit.
  
• Oct 18: On Monday, Oct 21, there will be a lecture instead of the exercise sessions. The lecture will take place in room HS 00-026 in building 101.
• Oct 18: An Ilias course has been created for the lecture. The lecture slides will be uploaded there, and there exists a discussion forum for your questions. If you are registered for the lecture in HisInOne, you will receive a link allowing you to join.
  
• Oct 14: Exercise Sheet 01 uploaded. This is a short exercise sheet which has to be submitted by Wednesday in the first week of lectures (Oct 23).
  
• Sep 27: Homepage online.
  

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.

Exercises

Exam

Old lectures

Literature