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

未来的工程系统将以其计算和物理组件之间日益紧密的相互作用为特征。这种类型的系统被称为网络物理系统（CPS），并因其对各种工业部门的潜在影响而引起了全世界的广泛关注。虽然大多数目标CPS应用显然具有安全关键性质，例如下一代运输系统，电网和医疗设备，但如何经济地构建和有效地认证这些系统安全，可靠和高性能仍然是CPS研究的重大挑战之一。当前的实践通常严重依赖于事后验证来提供保证，这通常涉及大量的测试和模拟，通常成本很高，并且可能很快变得难以处理复杂的设计。

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.