CodeCPS: Correct-by-Design Estimation and Control of Cyber-Physical Systems

网络物理系统（CPS）可以在所有应用领域中找到，包括智能电网、机器人系统、自动驾驶汽车和医疗监控系统。CPS是一个在物理组件和计算元素（网络部件）之间具有紧密交互的系统。由于计算、通信和存储的快速发展，CPS变得无处不在。CPS的设计和实现见证了源于系统中嵌入的控制软件与物理元素交互的关键问题。此类不良行为的例子包括电网频率偏离标称值过多导致停电，由于软件错误导致飞机坠毁，或自动驾驶汽车撞上行人。例如，2019年，剑桥郡的停电影响了英国100多万客户；2019年，波音737 Max客机在全球范围内停飞，此前两起坠机事故造成346人死亡，给航空业造成141亿英镑的损失；2015年，丰田因软件漏洞召回了6.5万辆汽车。在系统中运行的核心控制软件的开发仍然是临时的和容易出错的，并且今天的大部分工程成本都用于确保控制软件正确工作。设计可靠的CPS需要结合多个学科的方法，包括计算机科学、工程和控制理论，这些学科使用数学模型研究系统的分析和设计。开发CPS的一个主要挑战是所涉及的学科之间设计实践的巨大差异。解决这样的挑战需要研究人员了解系统的复杂性作为一个整体，分析网络和物理部分之间的相互作用，并确保CPS在设计阶段不会显示出不希望的行为。设计校正综合是一种新颖的新兴方法，它使用CPS的“数学描述”或“模型”，并设计控制软件，保证在被控制的CPS在现实世界中实现之前在其中缺乏不良行为。然而，由于分析模型需要极大的计算能力，设计正确的方法目前仅限于小型和简单的（线性）数学模型。它们还依赖于系统的精确数学模型，而这些模型通常是不可用的，也很难构建。这些限制阻碍了在不确定环境中工作的大型复杂CPS的正确设计方法的应用。CodeCPS项目将提供一组技术和工具来克服这些限制，并推动由设计正确方法处理的CPS的边界。我的新研究者项目旨在推进正确设计合成CPS的理论基础。特别地，我将讨论这种系统的三个具体挑战：复杂的动力学，大规模的，不确定性的存在（在模型，环境和状态信息中）。我将首次提供设计校正技术，这些技术对模型不确定性具有鲁棒性，可以处理具有非线性行为的系统，并且是组合的，因此适用于具有大量组件的CPS。我将专门将这些技术应用于智能能源系统，以设计控制软件，通过集成响应性负载（例如，智能建筑和电动汽车）确保能源系统频率的安全运行。CodeCPS将对CPS的可靠性产生重大影响，例如为设计无停电的智能能源系统或可靠的无人驾驶汽车提供新的方法作为跳板。该项目的成功完成将为控制软件的自动化设计提供一种方法，使开发复杂但可靠的CPS应用成为可能，同时大大降低了工程成本。

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.