CDC 2010 Workshop

Presentation slides are now available for download. See the schedule section below.

Correct-by-design embedded control software synthesis

Workshop Abstract

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:

Verification and Control of Hybrid Systems: A Symbolic Approach

Organizers

The workshop is organized by Antoine Girard (Universite Joseph Fourier), Giordano Pola (University of l'Aquila), and Paulo Tabuada (UCLA).

List of presenters

The workshop will be presented by the organizers. In addition, the Pessoa tutorial will be given by Manuel Mazo Jr. (UCLA) and by Dr. Pritam Roy (UCLA).

Workshop goals and major topics

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:

• • Introduce the participants to the recent results on approximate abstractions of control systems;

  • Discuss how the theory of approximate abstractions can be used to construct finite-state models of control systems described by differential equations;

  • Discuss how to algorithmically synthesize finite-state descriptions of control software;

  • Discuss how to algorithmically refine finite-state descriptions of control software to hybrid systems implementations and to software implementations;

  • Illustrate all these concepts on the Matlab based tool Pessoa through a hands-on tutorial and how to simulate the synthesized controllers in Simulink.

Brief description of the intended audience

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.

Schedule (Room 213)

• • 09:00 - 09:30 Overview (Paulo Tabuada)

  • 09:30 - 10:30 Discrete synthesis (Paulo Tabuada)

• 10:30 - 11:00 Coffee Break

  • 11:00 - 12:00 Discrete abstractions of continuous control systems (Giordano Pola)

  • 12:00 - 13:30 Lunch Break

  • 13:30 - 14:30 Refinement of discrete controllers to hybrid controllers and software implementations (Antoine Girard)

• 14:30 - 15:00 Coffee Break

  • 15:00 - 16:30 Hands-on Pessoa tutorial (Manuel Mazo Jr.)

  • 16:30 - 17:00 Open problems, future challenges, and discussion (All)

Pre-requisites

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.