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.
|Instructors||Prof. Dr. Andreas Podelski, Dr. Matthias Heizmann, Christian Schilling|
|Lecture||Monday, 16:00 - 18:00, building 101 HS 00-026
Wednesday, 16:00 - 17:00, building 101 SR 00-010/014
|Exercise||Wednesday, 17:00 - 18:00
|Language of instruction||English
|Exams||Written exam, on 13th March at 14:00 (s.t.) in rooms 026, 036, and 010/14 in building 101
|Course catalog||Cyber-Physical Systems – Discrete Models - Lecture
Cyber-Physical Systems – Discrete Models - Exercise
DescriptionThe 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.
- 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.
- Mar. 27: The exam review (Klausureinsicht) takes place on Wednesday, April 19, at 2 pm.
- 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.
- 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.
You may bring to the exam one DIN A4 sheet. Both sides of this sheet may be filled with any notes (e.g., definitions, theorems, examples) but the notes have to be handwritten. You may not use any other material in the exam (except for writing utensils).
The duration of the exam will be 90 minutes.
|Mon, October 17
|Wed, October 19
||Formal verification, Transition systems, Transition systems for sequential circuits
|Mon, October 24
||Program graphs, Transition systems for program graphs, Guarded Command Language
|Wed, October 26
||lec04-slides.pdf||lec04-WithoutOverlays.pdf||lec04-handout.pdf||Guarded Command Language, Spin
|Mon, October 31
||lec05-slides.pdf||lec05-WithoutOverlays.pdf||lec05-handout.pdf||Parallel systems, Interleaving operator
|Wed, November 2
||lec06-slides.pdf||lec06-WithoutOverlays.pdf||lec06-handout.pdf||Parallel systems, Synchronization operator, Nondeterminism
|Mon, November 7
||lec07-slides.pdf||lec07-WithoutOverlays.pdf||lec07-handout.pdf||Parallel systems, Mutual exclusion, State-based view on transition systems
|lec08-slides.pdf||lec08-WithoutOverlays.pdf||lec08-handout.pdf||State-based view on transition systems, Paths, Traces
|lec09-slides.pdf||lec09-WithoutOverlays.pdf||lec09-handout.pdf||Traces, Regular expressions, Omega-regular expressions
|lec10-slides.pdf||lec10-WithoutOverlays.pdf||lec10-handout.pdf||LT properties, Trace inclusion, Trace equivalence|
|lec11-slides.pdf||lec11-WithoutOverlays.pdf||lec11-handout.pdf||Propositional logic, Invariants, Safety properties
|lec12-slides.pdf||lec12-WithoutOverlays.pdf||lec12-handout.pdf||Safety properties, Prefix closure
|lec13-slides.pdf||lec13-WithoutOverlays.pdf||lec13-handout.pdf||Prefix closure, Finite traces and trace inclusion, Liveness properties
||lec15-handout.pdf||Fairness, Finite automata (NFA), Regular safety properties
|Wed, December 7
||lec16-slides.pdf||lec16-WithoutOverlays.pdf||lec16-handout.pdf||Regular safety properties, Ultimate automata library
|lec17-slides.pdf||lec17-WithoutOverlays.pdf||lec17-handout.pdf||Checking regular safety properties
|Wed, December 14
||lec18-slides.pdf||lec18-WithoutOverlays.pdf||lec18-handout.pdf||ω-regular properties, Büchi automata (NBA)
|Mon, December 19
||lec19-slides.pdf||lec19-WithoutOverlays.pdf||lec19-handout.pdf||Equivalence of Büchi automata and ω-regular expressions.
|Wed, December 21
||lec20-slides.pdf||lec20-WithoutOverlays.pdf||lec20-handout.pdf||Nonemptiness for NBA, Generalized Büchi Automata (GNBA)
|Mon, January 9
||lec21-slides.pdf||lec21-WithoutOverlays.pdf||lec21-handout.pdf||Checking ω-regular properties|
|Wed, January 11
||lec22-slides.pdf||lec22-WithoutOverlays.pdf||lec22-handout.pdf||Intersection for GNBA, Syntax of LTL
|Mon, January 16
||lec23-slides.pdf||lec23-WithoutOverlays.pdf||lec23-handout.pdf||Semantics of LTL
|Wed, January 18
||lec24-slides.pdf||lec24-WithoutOverlays.pdf||lec24-handout.pdf||Weak Until, LTL-PNF
|Mon, January 23
||lec25-slides.pdf||lec25-WithoutOverlays.pdf||lec25-handout.pdf||Automata-based LTL model checking
|Wed, January 25||lec26-slides.pdf||lec26-WithoutOverlays.pdf||lec26-handout.pdf|
|Mon, January 30
||lec27-slides.pdf||lec27-WithoutOverlays.pdf||lec27-handout.pdf||Computation tree logic
|Wed, February 1
||lec28-slides.pdf||lec28-WithoutOverlays.pdf||lec28-handout.pdf||CTL model checking
|Mon, February 6
||Brief summary of course content up to Lecture 17
|Wed, February 8
||Brief summary of course content starting with Lecture 18. Ultimate LTL Automizer
Lecture 21: Automata Script file for trafficlight example
Lecture 22: Automata Script file for messages example
|sheet 1||Mon, October 24|
||Mon, October 31
||Mon, November 7
||Mon, November 14
||Mon, November 21
||Mon, November 28|
||Mon, December 5
||Mon, December 12
||Mon, December 19|
|sheet 10||Mon, January 9
|sheet 11||Mon, January 16
|sheet 12||Mon, January 23
||Mon, January 30
|sheet 14||Mon, February 6