|
|
|
Cyber-Physical Systems – Discrete Models - Wintersemester 14/15
Übersicht
The course provides an introduction to discrete models of cyberphysical 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 BDDbased 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.
The lectures will be recorded and published on the
ILIAS platform (https://ilias.uni-freiburg.de/goto.php?target=crs_277905&client_id=unifreiburg).
There is also a forum where questions related to the lecture or exercises can be discussed.
|
Vorlesung im Masterstudiengang ESE, Master Informatik, Bachelor Informatik, Lehramt Informatik (3+1 SWS, 6 ETCS)
|
|
