Cyber-physical systems (CPS) can be found in all application domains, including smart power grids, robotics systems, autonomous cars and medical monitoring systems. A CPS is a system that has a tight interaction between physical components and computing elements (cyber parts). CPS are becoming ubiquitous due to rapid advances in computation, communication, and memory. Design and implementation of CPS have witnessed critical issues originated from the control software embedded in the system interacting with the physical elements. Examples of such undesired behaviours include the frequency of the power network deviating too much from its nominal value causing an electricity blackout, crash of an airplane due to software bugs, or an autonomous car hitting a pedestrian. For instance, Cambridgeshire's power cut affected over one million customers in the UK in 2019, the Boeing 737 Max airliner was grounded in 2019 worldwide after 346 people died in two crashes causing a loss of £14.1 billion to the aviation industry, and Toyota recalled 65,000 cars in 2015 over a software bug.

The development of core control software running in the system is still ad hoc and error-prone and much of the engineering costs today go into ensuring that control software works correctly. Design of reliable CPS requires combining approaches from multiple disciplines including computer science, engineering and control theory that studies analysis and design of systems using their mathematical models. A major challenge in the development of CPS is the large differences in the design practices between the involved disciplines. Addressing such a challenge requires researchers who understand the system complexity as a whole, analyse the interaction between the cyber and the physical parts, and ensure that the CPS does not show undesired behaviours at the design stage.

Correct-by-design synthesis is a novel and emerging approach that uses a "mathematical description" or "model" of the CPS and designs control software with guarantees on the lack of undesired behaviours in the controlled CPS before it is implemented in the real world. Correct-by-design approaches, however, are currently limited to small and simple (linear) mathematical models due to the need for extremely large computational power for analysing the model. They also rely on exact mathematical models of the system, which is often not available and hard to construct. These limitations prevent the application of correct-by-design approaches to large complex CPS working in an uncertain environment. The CodeCPS project will provide a set of techniques and tools to overcome such limitations and push the boundaries of the CPS handled by correct-by-design approaches.

My New Investigator project aims to advance the theoretical foundations of correct-by-design synthesis for CPS. In particular, I will address three specific challenges of such systems: complex dynamics, being large-scale, and presence of uncertainty (in the model, environment, and state information). I will provide, for the first time, correct-by-design techniques that are robust with respect to model uncertainties, can handle systems with non-linear behaviours, and are compositional, thus applicable to CPS with large number of components. I will apply these techniques specifically to smart energy systems for designing control software that ensures safe operation of the frequency of the energy system by integrating responsive loads (e.g., Smart Buildings and Electric Vehicles).

CodeCPS will strongly impact the reliability of CPS, such as by providing new methodologies as stepping stones for designing smart energy systems that are blackout free or trustworthy autonomous cars with no fatalities. Successful completion of this project will give a method for automated design of control software that makes it finally possible to develop complex, yet reliable CPS applications while considerably reducing the engineering cost.