Presentation slides are now available for download. See the schedule section below.
Embedded control systems are examples of more general cyber-physical systems that tightly coordinate discrete computation with the continuous control of physical resources. Advances in the design of cyber-physical systems hold the promise of bringing a sea of change in many different domains in which computation interacts with the physical world such as autonomous vehicles, robotic surgery, transportation networks, power-grids, etc. Unfortunately, design principles for such systems are still not understood. For this reason, formal verification of embedded control software is currently the only existing methodology capable to providing assurances of correct behavior and desired performance. Despite recent advances in hybrid systems, formal verification is only applicable to systems with relatively simple continuous dynamics. In this workshop we introduce a different paradigm, termed correct-by-design synthesis, that leads to provably correct embedded control software. Building on recent results on approximate abstractions of control systems, we will present a design methodology that is applicable to a large class of control systems including nonlinear and switched systems. We will also introduce the participants to the Matlab based tool Pessoa that automates the design process. The workshop includes a hands-on tutorial of Pessoa during which the participants will install Pessoa in their own computers and will synthesize several controllers enforcing a mix of continuous control requirements with logic requirements. This workshop is supported by the recently published book:
The objective of the tutorial is to introduce the participants to the recent research on correct-by-design synthesis of embedded control software. Its objectives are:
The intended audience consists of researchers, Ph.D. students, and practitioners interested in cyber-physical systems in general and in real-time, embedded, and networked control systems in particular.
Basic knowledge of linear control systems. The hands-on tutorial requires that each participant brings its own computer with an installation of Matlab and Simulink.