Cyber-Physical Networks: Foundations, Correct-by-Construction Control Design, and Applications

未来的工程化系统将以其计算组件和物理组件之间日益紧密的交互为特征。这种类型的系统被称为网络物理系统(CP)，由于其对各种工业部门的潜在影响，在世界范围内引起了相当大的关注。虽然大多数目标CPS应用显然都是安全关键性质的，例如下一代交通系统、电网和医疗设备，但如何以负担得起的价格构建这些系统并有效地认证这些系统是安全、可靠和高性能的，仍然是CPS研究的重大挑战之一。目前的做法往往严重依赖事后核查来提供保证，这通常涉及广泛的测试和模拟，通常成本很高，对于复杂的设计可能很快变得难以处理。 在上述挑战的推动下，拟议的研究计划旨在促进此类系统设计的范式转换，从传统的“设计和验证”方法转变为“指定和综合”方法；即，从形式的系统级规范(例如，可以用时序逻辑描述的规范)开始，寻求通过构造来设计满足规范中所编码的期望属性的系统(称为按构造进行的正确设计)。 拟议的研究涉及控制工程、计算机科学和应用数学的广泛接口。长期目标(5-10年)是从根本上促进对CPS的理解，并为CPS提供新的设计范例。短期目标(1-5年)是：(1)通过互联混合系统的积木，为网络化控制系统的建模和分析奠定理论基础；(2)从严格的规范出发，为网络化控制系统的逐结构校正控制综合开发使能理论和可扩展的工具；以及(3)通过物理和数值实验，展示网络化自主机器人车辆和电力系统中的逐结构校正设计方法。 实现上述目标的计划包括三个技术主题，并为不同研究水平的HQP培训提供了大量的范围：1)CPS中混合动态网络的建模和分析(PHD 1)；2)网络化CPS的正确结构控制综合(PHD 2)；3)特定领域的CPS在机器人学(硕士1，本科生)和电力系统(硕士2，本科生)中的应用。跨上述技术主题的分析、计算和实验方法的集成将为拟议的计划和HQP培训计划带来显著的附加值。该计划中存在的跨学科挑战将提供跨越和推进混合系统、正式方法、机器人和电力系统四个技术领域的边界的机会。

Engineered systems of the future will feature increasingly tight interactions between their computational and physical components. Systems of this type are referred to as cyber-physical systems (CPS) and have attracted considerable attention worldwide for their potential impact on a variety of industrial sectors. While most targeted CPS applications are evidently of safety-critical nature, e.g., next-generation transportation systems, power grids, and medical devices, how to affordably build and efficiently certify these systems as safe, reliable, and high performance remains one of the grand challenges of CPS research. Current practice often heavily relies on ex-post verification to deliver assurance, which typically involves extensive testing and simulations, usually at a significant cost, and may rapidly become intractable for complex designs. Motivated by the above challenge, the proposed research program aims to contribute to a paradigm shift in the design of such systems, from the traditional "design and verify" approach to a "specify and synthesize" approach; that is, start with a formal, system-level specification (e.g. that can be described by temporal logics) and seek to design systems that satisfy desired properties encoded in the specification by construction (known as correct-by-construction design). The proposed research lies at the broad interface of control engineering, computer science, and applied mathematics. The long-term aim (5-10 years) is to fundamentally advance the understanding of and provide new design paradigms for CPS. The short-term objectives (1-5 years) are to: (1) lay a theoretical foundation for the modelling and analysis of networked CPS via the building blocks of interconnected hybrid systems; (2) develop enabling theories and scalable tools for the correct-by-construction control synthesis for networked CPS from rigorous specifications; and (3) demonstrate the correct-by-construction design methodology in networked autonomous robotic vehicles and electric power systems via physical and numerical experiments. The program for achieving the above objectives consists of three technical themes and provides plenty of scope for HQP training at various levels of research: 1) Modelling and analysis of hybrid dynamical networks in CPS (PhD 1); 2) Correct-by-construction control synthesis for networked CPS (PhD 2); 3) Domain-specific CPS applications in robotics (Master 1, Undergraduates) and power systems (Master 2, Undergraduates). The integration between analytical, computational, and experimental methods across the above technical themes will bring significant added value to the proposed program and HQP training plan. The inter-disciplinary challenges present in this program will provide opportunities to cross and push the boundaries of four technical areas of hybrid systems, formal methods, robotics, and power systems.