基于定理证明的信息物理系统的形式化验证（邀请论文）
Formal Verification of Cyber-Physical Systems using Theorem Proving (Invited Paper)
摘要：
由于软件和工程技术的重大突破，嵌入式系统越来越多地用于航空航天和下一代交通系统，智能电网和智能城市，医疗保健系统，以及广义上的网络物理系统（CPS）。CPS主要由几个电子、通信和控制器模块以及一些致动器和传感器组成。异构底层智能技术的混合对设计提出了许多技术挑战，更严重的是对这种复杂基础设施的验证。事实上，CPS应遵守严格的安全性，可靠性，性能和安全性要求，其中需要捕获各种CPS模块的物理和随机方面，然后分析它们在相互关联的连续和离散动态中的相互关系。然而，通常情况下，系统错误在分析过程中不会被发现，从而导致不必要的情况，这些情况可能在安全关键应用中产生严重后果。在本文中，我们介绍了一些挑战，围绕当代CPS的设计和验证与智能技术的出现。特别是，我们调查最近的事态发展中使用的定理证明，一种正式的方法，CPS的建模，分析和验证，并概述了一些现实世界的CPS案例研究，从汽车，航空电子和健康技术领域从系统级的物理组件。
英文摘要：
Due to major breakthroughs in software and engineering technologies, embedded systems are increasingly being utilized in areas ranging from aerospace and next-generation transportation systems, to smart grid and smart cities, to health care systems, and broadly speaking to what is known as Cyber-Physical Systems (CPS). A CPS is primarily composed of several electronic, communication and controller modules and some actuators and sensors. The mix of heterogeneous underlying smart technologies poses a number of technical challenges to the design and more severely to the verification of such complex infrastructure. In fact, a CPS shall adhere to strict safety, reliability, performance and security requirements, where one needs to capture both physical and random aspects of the various CPS modules and then analyze their interrelationship across interlinked continuous and discrete dynamics. Often times however, system bugs remain uncaught during the analysis and in turn cause unwanted scenarios that may have serious consequences in safety-critical applications. In this paper, we introduce some of the challenges surrounding the design and verification of contemporary CPS with the advent of smart technologies. In particular, we survey recent developments in the use of theorem proving, a formal method, for the modeling, analysis and verification of CPS, and overview some real world CPS case studies from the automotive, avionics and healthtech domains from system level to physical components.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
