- Description:
-
Today, humankind has the ability to develop systems of incredible complexity (e.g., trains, microprocessors, airplanes, nuclear power plants). However, the costs of managing this complexity and of ensuring the correct behavior of a given system have become critical. A key technique for mastering this complexity is the usage of models that describe only those aspects of the systems that are important for the task at hand, and automated tools for analyzing those models. This subject will present theory and algorithms that form the basis for the modeling and analysis of complex systems.
- Contents:
-
1. System theory introduction.
2. Logical basics.
3. Systems and automata.
4. Interacting system components.
5. Temporal logics.
6. Testing and bounded model checking.
7. Boolean satisfiability (SAT).
8. Unbounded model checking.
9. Petri nets.
10. Timed automata.
11. Modeling the physical environment.
12. Probabilistic models.
13. Simulation and control of system models.
- Seminar contents:
-
Improving the understanding of the subject by solving example problems using pen and paper.
- Recommended literature:
-
1. Lee, E. A. - Seshia, S. A. : Introduction to Embedded Systems, A Cyber-Physical Systems Approach (2nd
Edition). MIT Press, 2017. ISBN 978-0-262-53381-2.
2. Clarke, E. M. - Henzinger, Th.A. - Veith, H. - Bloem, R. (Eds.) : Handbook of Model Checking. Springer,
2018. ISBN 978-3-319-10574-1.
3. Alur, R. : Principles of Cyber-Physical Systems. MIT Press, 2015. ISBN 978-0-262-02911-7.
- Keywords:
- modeling, formal verification
Abbreviations used:
Semester:
- W ... winter semester (usually October - February)
- S ... spring semester (usually March - June)
- W,S ... both semesters
Mode of completion of the course:
- A ... Assessment (no grade is given to this course but credits are awarded. You will receive only P (Passed) of F (Failed) and number of credits)
- GA ... Graded Assessment (a grade is awarded for this course)
- EX ... Examination (a grade is awarded for this course)
- A, EX ... Examination (the award of Assessment is a precondition for taking the Examination in the given subject, a grade is awarded for this course)
Weekly load (hours per week):
- P ... lecture
- C ... seminar
- L ... laboratory
- R ... proseminar
- S ... seminar