Overview

In this workshop, the DFG research training group on Continuous Verification of CYber-Physical Systems (ConVeY) presents and discusses its latest research. The workshop is organized as a satellite event of ETAPS, before the main conference.

Networks, computers, sensors, and actuators are being increasingly integrated into cyber-physical systems, i.e., software systems that interact with the physical world and must cope with its continuous behavior. An increasing number of cyber-physical systems operate in safety-critical domains, e.g., autonomous vehicles, robotic surgery, traffic control, human-robot collaboration, and smart grids. For this reason, their design and deployment should ideally be accompanied by a formal check of correct behavior. A fundamental challenge in the verification of cyber-physical systems is the fact that they are subject to change. The physical environment changes continuously, at runtime, and in ways that cannot be completely foreseen at the design stage. At the same time, the requirements may change. Sought-after aspects include more functionality, lower power consumption, or faster response. In many cases, the system should be migrated to a different hardware platform. To face this multi-level continuous change, the DFG research training group on Continuous Verification of CYber-Physical Systems (ConVeY) performs research in the following fields:

Robust System Design

We will develop techniques to guarantee correct behavior under changes in plant parameters, under certain classes of perturbations including sensor measurement errors, and under uncertainties introduced by the implementation platform. In particular, we will investigate the design of controllers that are robust by construction against those changes.

Evolving Systems

Novel construction and verification techniques shall be investigated that adapt to offline changes in the specification, the hardware, or the implementation of control software, and reuse efforts from earlier stages as much as possible.

On-the-fly Synthesis and Verification

We will develop techniques for the online verification and synthesis of controllers that operate—and provide a correctness guarantee—only within a given time horizon. Repeated execution of this procedure, combined with availability of a fail-safe strategy, ensures safe operation.