Formal Methods for Control of Cyber-Physical Systems: Theory, Algorithms, and Implementations

信息物理系统（CPS）是由基于计算机的算法控制的物理工程系统。这样的系统正越来越多地渗透到我们的生活中：执行搜索和救援任务的无人驾驶飞行器（UAV），在忙碌交通中导航的自动汽车，以及执行救生操作的外科手术机器人-这些只是高级控制算法与物理系统集成如何导致重要应用的几个例子。许多CPS，包括上述激励应用程序，都是安全关键的：它们的故障可能导致灾难性的后果。例如，欧洲航天局花了10年时间和70亿美元生产的阿丽亚娜5号火箭，由于数字软件设计中的一个小错误，在不到一分钟的时间内坠毁。最近特斯拉自动驾驶仪的故障导致了致命的事故，这是另一个警告信号，表明我们仍然对信任自动化机器缺乏信心。机器学习算法的日益普及也提出了人工智能在控制安全关键CPS方面的信任这一根本性的重要问题。事实上，如何负担得起建立和有效地证明CPS是安全的，可靠的，值得信赖的仍然是学术界和工业界的一个根本挑战。有几个因素使得CPS的控制设计成为一个巨大的挑战：1）CPS通常具有包括连续和离散动态的混合动态。混合动力系统的分析和控制通常更具挑战性; 2）CPS通常具有复杂的要求，这超出了当前控制工程理论和工具的范围; 3）目前用于CPS控制的形式化方法的实践经常遭受维数灾难，并且需要非常精确的系统模型。 受这些挑战的激励，拟议的研究计划将开发CPS计算机辅助控制设计的理论基础和计算框架。通过这样做，所提出的计划将推进最先进的数学控制理论和设计方法的安全关键CPS。长期目标是系统地开发验证计算方法，用于CPS的稳健设计，并将其转化为实践。短期目标（在未来五年内）是：（O 1）探索CPS控制的有效计算和形式化方法的理论极限：（O2）设计有效的算法和工具，从严格的规范中为CPS设计鲁棒控制综合;（O3）利用控制理论，学习，并通过优化克服CPS控制中的维数灾难和模型灾难。拟议研究的成果可以使加拿大的几个CPS部门受益匪浅，包括汽车，航空航天和机器人。在该计划下培训的学生将获得具有竞争力的技能，如控制，机器学习和机器人技术，以进入蓬勃发展的机器人，人工智能和自动化领域。

Cyber-physical systems (CPS) are physical engineering systems controlled by computer-based algorithms. Such systems are increasingly penetrating our lives: unmanned air vehicles (UAVs) executing search and rescue missions, autonomous cars navigating through busy traffic, and surgical robots performing life-saving operations---these are just a few examples of how integrations of advanced control algorithms with physical systems can lead to important applications. Many CPS, including the above motivating applications, are safety-critical: their failure can lead to catastrophic consequences. For example, the Ariane 5 rocket, which took the European Space Agency 10 years and $7 billions to produce, crashed in less than one minute due to a small error in the numerical software design. The recent failures of Tesla's AutoPilot that caused fatal accidents is another warning sign that we still significantly lack confidence in trusting automated machines. The increasingly pervasive use of machine learning algorithms also raises the fundamentally important question of AI trust in control of safety-critical CPS. Indeed, how to affordably build and efficiently certify CPS as safe, reliable, and trustworthy remains a fundamental challenge in both academia and industry. There are several factors that make control design for CPS an enormous challenge: 1) CPS usually have hybrid dynamics involving both continuous and discrete dynamics. Hybrid systems are generally more challenging to analyze and control; 2) CPS typically have complex requirements, which are beyond what can be handled by the current theory and tools of control engineering; 3) Current practices of formal methods for control of CPS often suffer from curse of dimensionality and require very accurate system models.  Motivated by these challenges, the proposed research program will develop the theoretical foundations and computational frameworks for computer-aided control design for CPS. By doing so, the proposed program will advance the-state-of-the-art of mathematical control theory and design methods for safety-critical CPS. The long-term goal is to systematically develop validated computational methods for robust design of CPS and translate them to practice. The short-term objectives (within in the next five years) are to: (O1) Explore the theoretical limits of validated computation and formal methods for control of CPS; (O2) Design efficient algorithms and tools for robust control synthesis for CPS from rigorous specifications; (O3) Exploit the synergies of control theory, learning, and optimization to overcome the curse of dimensionality and curse of modelling in control of CPS. The outcomes of the proposed research can significantly benefit several CPS sectors in Canada, including automotive, aerospace, and robotics. Students trained under this program will gain competitive skills, such as control, machine learning, and robotics, to enter the booming fields of robotics, AI, and automation.