Special Seminar: Ruediger Ehlers "Engineering Correct-by-construction Cyber-Physical Systems"

Department of Computer Science

Thursday 5.4.2018 at 13:00 in T5, CS building

Ruediger Ehlers

Title: Engineering Correct-by-construction Cyber-Physical Systems

Abstract:

Safety-critical systems need to behave according to their specification in order to avoid catastrophic failures. Unfortunately, designing such systems is difficult, which induces a need to support their engineering process by verification and synthesis approaches.

In this talk, I will present a selection of recent results on supporting the engineering process of correctly behaving cyber-physical systems. The starting point will be a classical problem in distributed systems, namely determining whether a system can be implemented symmetrically, i.e., such that it consists of multiple instances of the same process implementation. I will show that for omega-regular specifications, the problem is decidable if all processes are arranged in a ring structure and receive all input to the overall system. However, even for a very simple architecture in which two processes are chained, the problem is shown to be undecidable.

We then turn towards the problem of enforcing the correctness of systems that include a machine learning component. I will present a novel approach to verifying properties of the input/output behavior of artificial neural networks. Given the recent trend to employ neural networks in safety-critical contexts, this approach is useful for the safety certification of a system that uses a learned network as a component.

Finally, we will discuss a control problem for cyber-physical systems in which failure probabilities for the system's actions can be estimated. I will show how to synthesize good policies for enforcing complex temporal specifications in a physical system that can be modeled as a Markov Decision Process, where due to the non-zero failure probability of every action, almost sure eventual violation of the specification is unavoidable. While classical control algorithms do not allow to compute a reasonable controller in this setting (as all controllers almost surely eventually fail), I will show how to obtain controllers that are risk-averse in that they try avoiding to use actions with a high probability of failure, but at the same time are also optimistic in that a failure will not happen. An interactive demonstration will show that this approach computes controllers that exhibit reasonable behavior in the physical world. Abstract: