« November 2019 »
November
MoTuWeThFrSaSu
123
45678910
11121314151617
18192021222324
252627282930
Uni-Logo
You are here: Home Teaching Winter Term 2019/20 Cyber-Physical Systems I - Discrete Models (Lecture)
Document Actions

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.

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

News

  • 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

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.
Personal tools