Cyber Physical Systems - Discrete Models
Due to a scheduling conflict, the time slot for the exercise is moved to Monday and the lecture time on Thurday needs to be adjusted slightly. See the new dates/times below. The new lecturing schedule is effective from 9 January.
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 of such systems. The course covers different mechanisms to specify temporal properties including linear time properties and branching time properties using logical formalisms such as LTL, CTL, and CTL*.
Finally, the course demonstrates how to develop algorithms for checking whether these properties hold.
Lecturer | Prof. Dr. Peter Thiemann |
Time and Place | Mo 16-16:45 (s.t.!),SR 01-009/13, Geb. 101 |
Do 12-13:45 (s.t.!), SR 01-009/13, Geb. 101 | |
Assistants |
Manuel Geffken Robert Jakob |
Exercise
Time and Place | Mo 17-17:45 (s.t.!) SR 01-009/13, Geb. 101 |
In addition to the lecture, we will publish exercise sheets. These exercise sheets are mandatory and ensure that you work on and understand the topics presented in the lecture. If you were not able to do the exercise, please hand in your partial results with a statement why you couldn't do it.
Exercise sheets are published on the Piazza course homepage.
Exam
Details about the exam (either oral or written) are yet to be announced.
Form and Questions
This course uses the learning and teaching platform Piazza (similar to a forum).
Please enroll there using the following link https://piazza.com/uni-freiburg.de/winter2014/11le13vid120948.
The course homepage of Piazza can be seen here: https://piazza.com/uni-freiburg.de/winter2014/11le13vid120948/home.
Literature
The lecture's main source is the well-known model checking book (there are 10 copies in the library) of Baier and Katoen.
- Baier, C., & Katoen, J. (2008). Principles of Model Checking. MIT Press (Vol. 950, p. 975).
- Bérard, B., Bidoit, M., Finkel, A., & Laroussinie, F. (2010). Systems and software verification. Springer.
- Clarke, E. M., Grumberg, O., & Peled, D. (1999). Model Checking. MIT Press.
- Kropf, T. (1999). Introduction to Formal Hardware Verification. Springer.