DE

Modul

Logical Foundations of Cyber-Physical Systems [M-INFO-106102]

Credits
6
Recurrence
Jedes Wintersemester
Duration
1 Semester
Language
English
Level
4
Version
3

Responsible

Organisation

  • KIT-Fakultät für Informatik

Part of

Bricks

Identifier Name LP
T-INFO-112360 Logical Foundations of Cyber-Physical Systems 6

Competence Certificate

See partial achievements (Teilleistung)

Competence Goal

In modeling and control, successful students will
– understand core principles behind CPS. A solid understanding of these principles is important for anyone who wants to integrate cyber and physical components to solve problems that no part could solve alone.
– develop models and controls. In order to understand, design, and analyze CPS, it is important to be able to develop models for the relevant aspects of a CPS design and to design controllers for the intended functionalities based on appropriate specifications, including modeling with differential equations.
– identify relevant dynamical aspects. It is important to be able to identify which types of phenomena influence a property of a system. These allow us to judge, for example, where it is important to manage adversarial effects, or where a nondeterministic model is sufficient.

In computational thinking, successful students should be able to
– identify safety specifications and critical properties. In order to develop correct CPS designs, it is important to identify what “correctness” means, how a design may fail to be correct, and how to make it correct.
– understand abstraction in system designs. The power of abstraction is essential for the modular organization of CPS, and the ability to reason about separate parts of a system independently.
– express pre- and post-conditions and invariants for CPS models. Pre- and post-conditions allow us to capture under which circumstance it is safe to run a CPS or a part of a CPS design, and what safety entails. They allow us to achieve what abstraction and hierarchies achieve at the system level: decompose correctness of a full CPS into correctness of smaller pieces. Invariants achieve a similar decomposition by establishing which relations of variables remain true no matter how long and how often the CPS runs.
– reason rigorously about CPS models. Reasoning is required to ensure correctness and find flaws in CPS designs. Both informal and formal reasoning in a logic are important objectives for being able to establish correctness, which includes rigorous reasoning about differential equations.

In CPS skills, successful students will be able to
– understand the semantics of a CPS model. What may be easy in a classical isolated program becomes very demanding when that program interfaces with effects in the physical world.
– develop an intuition for operational effects. Intuition for the joint operational effect of a CPS is crucial, e.g., about what the effect of a particular discrete computer control algorithm on a continuous plant will be.
– understand opportunities and challenges in CPS and verification. While the beneficial prospects of CPS for society are substantial, it is crucial to also develop an understanding of their inherent challenges and of approaches for minimizing the impact of potential safety hazards. Likewise, it is important to understand the ways in which formal verification can best help improve the safety of system designs.

Prerequisites

See partial achievements (Teilleistung)

Content

Cyber-physical systems (CPSs) combine cyber capabilities (computation and/or communication) with physical capabilities (motion or other physical processes). Cars, aircraft, and robots are prime examples, because they move physically in space in a way that is determined by discrete computerized control algorithms. Designing these algorithms to control CPSs is challenging due to their tight coupling with physical behavior. At the same time, it is vital that these algorithms be correct, since we rely on CPSs for safety-critical tasks like keeping aircraft from colliding. In this course we will strive to answer the fundamental question posed by Jeannette Wing:

“How can we provide people with cyber-physical systems they can bet their lives on?”

The cornerstone of this course design are hybrid programs (HPs), which capture relevant dynamical aspects of CPSs in a simple programming language with a simple semantics. One important aspect of HPs is that they directly allow the programmer to refer to real-valued variables representing real quantities and specify their dynamics as part of the HP.

This course will give you the required skills to formally analyze the CPSs that are all around us—from power plants to pacemakers and everything in between—so that when you contribute to the design of a CPS, you are able to understand important safety-critical aspects and feel confident designing and analyzing system models. It will provide an excellent foundation for students who seek industry positions and for students interested in pursuing research.

Recommendation

The course assumes prior exposure to basic computer programming and mathematical reasoning. This course covers the basic required mathematical and logical background of cyber-physical systems. You will be expected to follow the textbook as needed: André Platzer. Logical Foundations of Cyber-Physical Systems. Springer 2018. DOI:10.1007/978-3-319-63588-0

Workload

6 ECTS from 180h of coursework consisting of
- 22.5h = 15 * 1.5h from 3 SWS lectures
- 12h = 8 * 1.5h from 1 SWS exercises
- 90h preparation, reading textbook, studying - 40h solving exercises
- 15h exam preparation