PROCSYS

Towards programmable cyber-physical systems: a symbolic control approach

Context: Autonomous vehicles, intelligent buildings or robots promise to transform the everyday life of our society in all its dimensions (transport, housing, industry, health, assistance to the elderly ...). These systems are examples of cyber-physical systems (CPS) resulting from the integration of computer components and physical processes. The development of CPS is often time-consuming and costly, due to complex cyber-physical interactions and to critical safety requirements.

Objective: The primary objective of the PROCSYS project is to provide a new framework for CPS programming that enables fast and dependable development of advanced functionalities through a high-level language. The originality of our approach is to consider that the execution platform does not only consist of the computer components but also of the physical part of the CPS. Hence, CPS programs do not specify the behavior of computer components (as in the classical approach) but directly that of the CPS. This is a paradigm shift in CPS programming.

Approach: In our framework, a CPS compiler automatically synthesizes feedback controllers (i.e. low-level reactive programs that compute actions to be taken based on the available measurements) that enforce the behavior specified in the CPS program. The compiler relies on a model of the CPS including a description of the involved physical processes. Correctness of the controllers is guaranteed by following the correct by construction synthesis paradigm through the use of symbolic control techniques: the continuous physical dynamics is abstracted by a symbolic model, which is an ``abstraction’’ of the physical dynamics by a discrete dynamical system; a symbolic controller is synthesized automatically from the high-level CPS program and the symbolic model; an interface allows to refine the symbolic controller back to the physical world. 

Work description: In the PROCSYS project, we develop a high-level language for CPS, based on the formalism of hybrid automata, which makes it possible to specify a rich set of behaviors while enabling the development of efficient controller synthesis algorithms. The project also tackles two of the main bottlenecks of the symbolic control approach. Firstly, scalability of symbolic control is achieved by the combination of parsimonious symbolic models and lazy controller synthesis algorithms. Secondly, robustness is ensured by developing novel approaches for the synthesis of robust symbolic controllers. The project also contributes to emerging topics in symbolic control such as contract-based design for distributed CPS, data-driven abstraction for learning-enabled CPS, or symbolically guided model predictive controllers for high performance CPS. The algorithms developed in the project are implemented in a symbolic control toolbox, which will enable the use of our approach by systems engineers.