You are here: Home Teaching Winter Term 2020/21 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 will take place ONLINE (at the originally scheduled date and time, Monday, 15th March 16:00h). More details below.

Course type Lecture
Instructors Prof. Dr. Andreas PodelskiDominik Klumpp, Frank Schüssele
Lecture Live session via BigBlueButton, Wednesday 16:00 - 18:00
Recordings will be uploaded
Exercise Weekly exercise groups
  • Group 1: Monday,  16:00 - 18:00, BigBlueButton
  • Group 2: Monday,  16:00 - 18:00, BigBlueButton
  • Group 3: Tuesday, 16:00 - 18:00, BigBlueButton
  • Group 4: Tuesday, 16:00 - 18:00, BigBlueButton
  • Group 5: Monday,  10:00 - 12:00, BigBlueButton
  • Group 6: Monday,  10:00 - 12:00, BigBlueButton

To participate, join the ILIAS course room (see below) and contact us (Frank/Dominik)
to assign you to an exercise group with free spaces (if you are not already assigned).
Language of instruction English
Credits 6
Exams Written exam (online)
Course catalog Cyber-Physical Systems -- Discrete Models - Lecture
Cyber-Physical Systems -- Discrete Models - Exercises
ILIAS course https://ilias.uni-freiburg.de/goto.php?target=crs_1755223&client_id=unifreiburg

Online Exam due to Corona pandemic

Due to the pandemic situation, we will not have an in-presence exam as originally planned. Instead, the exam exercises will be made available for download, and exam participants will solve them at home (on paper) and upload their solutions. If you are registered for the exam in HisInOne, you should have been added to a new ILIAS course for the exam, and you should have received an email with further details.

If you are registered but did not receive this email, please contact Dominik Klumpp or Frank Schüssele immediately. Similarly, if you are having trouble with your registration via HisInOne, you can participate in the exam conditionally, meaning that we will only mark your submission if the examination office resolves the registration issues. If this applies to you, please also contact Dominik Klumpp or Frank Schüssele immediately.

News

  • Feb 24: Online exam announced.
  • Feb 05: Exercise sheet 12 (Bonus!) is added, submission until Feb 14.
  • Nov 02: Start of exercise sessions.
  • Oct 30: ILIAS course online.
  • Oct 22: In light of rising COVID case numbers, we have decided to move all exercise sessions online.
  • Oct 15: 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.

Lecture

The lecture will take the form of a weekly live session on BigBlueButton. We encourage you to participate in these sessions, and use the opportunity to ask questions about the lecture content directly. The lectures will be recorded and the recordings will be made available through ILIAS.

Note that we will NOT record cameras of students, only the slides and the lecturer. Questions asked via BigBlueButton's chat function will be read aloud and answered by the lecturer, but the chat itself is not recorded, nor is the list of participants.

Exercises

The lecture is accompanied by weekly exercises. Each Thursday 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 23:59 on Wednesday via the lecture's ILIAS course. The tutors will mark the solutions in and discuss them in the exercise groups the following week.

The exercises are not optional. You must obtain at least 50% of the exercise points. The idea is that you train yourself to write down things in a formally correct way. Your solutions to 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.

Exercise sessions will be conducted online via BigBlueButton. The exercise sessions will NOT be recorded. We encourage you to actively participate in these exercise sessions, as they are essential to practice and better understand the lecture content.

Exam

There will be a written exam at the end of the semester. According to university regulations, there is no possibility to remotely participate in the exam.

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 exam takes place online on 15th March 2021, 15:00 for 90 minutes. See above for more information.

Resources 

Slides

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

Exercise Sheets

The weekly exercise sheets are uploaded here. You can submit your solution via the lecture's ILIAS course.
Exercise SheetSubmission Deadline
Exercise Sheet 01 Wednesday, 11th November, 23:59
Exercise Sheet 02 Wednesday, 18th November, 23:59
Exercise Sheet 03 Wednesday, 25th November, 23:59
Exercise Sheet 04 Wednesday, 2nd December, 23:59
Exercise Sheet 05 Wednesday, 9th December, 23:59
Exercise Sheet 06 Wednesday, 16th December, 23:59
Exercise Sheet 07 Wednesday, 6th January, 23:59
Exercise Sheet 08
Wednesday, 13th January, 23:59
Exercise Sheet 09 Wednesday, 20th January, 23:59
Exercise Sheet 10 Wednesday, 27th January, 23:59
Exercise Sheet 11 Wednesday, 3rd February, 23:59
Exercise Sheet 12 Sunday, 14th February, 23:59

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.