You are here: Home Teaching Winter Term 2019/20 Cyber-Physical Systems I - …

Cyber-Physical Systems I - Discrete Models

In this course we demonstrate how cyber-physical systems, in the wide range of their heterogeneous aspects (large-scale systems, system of systems, embedded systems, concurrent systems, hardware systems, software systems) can be modeled using the basic notion of transition systems. We consider relevant formalisms for modeling correctness properties of cyber-physical systems, and show how the models can be analyzed using algorithmic methods in order to prove correctness or find errors.

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

Course type Lecture
Instructors Prof. Dr. Andreas PodelskiDominik Klumpp
Lecture Wednesday, 16:00 - 18:00, building 101 HS 00-026
Exercise Group 1: Monday, 16:00 - 18:00, building 101 HS 00-026
Group 2: Monday, 16:00 - 18:00, building 101 SR 01-016
Group 3: Monday, 16:00 - 18:00, building 101 SR 01-018
Language of instruction English
Credits 6
Exams Written exam
Course catalog Cyber-Physical Systems -- Discrete Models - Lecture
Cyber-Physical Systems -- Discrete Models - Exercises

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 course provides an introduction to discrete models of cyber-physical systems, their analysis and verification:
  • 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

The lecture is accompanied by exercises. Each Wednesday we will publish an exercise sheet. Students will have time until the next Wednesday to prepare solutions for the problems stated on the exercise sheet. Solutions may be submitted alone or in groups of two. The solutions must be submitted by 15:59 on Wednesday via the post boxes that are located in the ground floor of building 051. The tutors will correct the solutions in the four following days (Thu - Sun) and discuss them in the exercise groups on Monday.
 
The exercises are not optional. You must obtain at least 50% of the exercise points. The goal is to train you to write down things in a formally correct way (being able to write down things in a formally correct way is an important goal of this lecture, and you need to train it). Correcting the exercises will help us to evaluate your knowledge and to evaluate your capability to solve the exercises in the exam.
 
The students present their solutions in the exercise group. This is done on a voluntary basis (you can choose which exercises you want to present), but every student must present his/her solution to an exercise in an exercise group at least once in the semester.

Exam

There will be a written exam at the end of the semester.
You may bring one DIN A4 sheet to the exam. Both sides of this sheet may be filled with any notes (e.g., definitions, theorems, examples) but the notes have to be handwritten. You must not use any other material in the exam (except for writing utensils).
The duration of the exam will be 90 minutes.

Resources 

Slides

The lecture slides are uploaded to the lecture's Ilias course.

Exercise sheets

Exercise Sheet
Submission By
Exercise Sheet 01
Oct 23, 16:00
Exercise Sheet 02
Oct 30, 16:00
Exercise Sheet 03
Nov 06, 16:00
Exercise Sheet 04
Nov 13, 16:00
Exercise Sheet 05
Nov 20, 16:00
Exercise Sheet 06
Nov 27, 16:00
Exercise Sheet 07
Dec 04, 16:00
Exercise Sheet 08
Dec 11, 16:00
Exercise Sheet 09
Dec 18, 16:00
Exercise Sheet 10
Jan 08, 16:00
Exercise Sheet 11
Jan 15, 16:00
Exercise Sheet 12
Jan 22, 16:00
Exercise Sheet 13
Jan 29, 16:00
Exercise Sheet 14
Feb 05, 16:00
Exercise Sheet 15
Feb 10, 16:00

Old lectures

You can find information on previous courses on the following web pages.

Literature

The lecture will follow very closely the famous textbook "Principles of Model Checking" by Christel Baier and Joost-Pieter Katoen (MIT Press).  A copy is available in the library.