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. The design and implementation of CPS have witnessed critical issues originating 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, the crash of an aeroplane 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.