Practical, Efficient and Scalable Modeling, Verification and Validation of Safety-Critical Cyber-Physical Systems

典型的信息物理系统（CPS）包括由传感器监测和执行器控制的物理设备。这些传感器和执行器可以通过网络连接到各种不同的计算资源。这些系统需要仔细和紧密地集成计算、通信和控制技术，以在物理系统和许多应用领域设想的网络模块中实现严格的性能、稳定性、可靠性、效率和鲁棒性。cps已经成功地应用于我们日常生活的几乎每个方面，包括医疗设备、智慧城市、移动设备、工业4.0、智能交通、智能电网和能源系统。然而，许多cps本质上是安全关键的，必须经过认证并确保即使在未知和恶劣的环境下也是高度可靠的。计算的精度必须与物理世界的不确定性和噪声相结合。这需要强大的故障检测、诊断和恢复方法，以确保可靠和正确的系统运行。我们在这个研究项目中的目标是开发一个验证框架流程，以正式、组合和有效地推理它们的可靠性、安全性和安全性。我们将利用混合系统模型，例如动态微分逻辑，对CPS的确定性子系统进行模块化推理，并将概率建模为不确定性。我们将开发可扩展的和合理的探索方法来在更高的抽象层次上分析cps。我们的最终目标是开发一种全面而又组合的方法来验证和验证CPS，并为CPS的安全性和安全性提供强有力的理论保证。几个用例将被调查和执行，以验证我们提出的方法。

A typical Cyber-Physical System (CPS) comprehends physical devices monitored by sensors and controlled by actuators. These sensors and actuators may be interconnected via a network to a variety of different computational resources. These systems require a careful and tight integration of computing, communication, and control technologies to achieve stringent performance, stability, reliability, efficiency and robustness in both the physical systems as well as the cyber modules that are envisaged in many application domains. CPSs have been successfully employed and considered in almost every aspect of our daily lives, ranging from medical devices, smart cities, mobile devices, Industry 4.0, intelligent transportation, smart grid and energy systems. However, many CPSs are safety critical in nature and must be certified and ensured to be highly dependable even under unknown and hostile environments. The precision of computing must interface with the uncertainty and noise of the physical world. This requires powerful methods of failure detection, diagnosis, and recovery to ensure a reliable and correct system operation. Our goal in this research program is to develop a verification framework flow to formally, compositionally and efficiently reason about their reliability, safety and security. We will leverage hybrid system models, e.g. dynamic differential logic to modularly reason about the deterministic subsystems of the CPS with capabilities to model probabilities as uncertainties. We will develop scalable and sound exploration methods to analyze CPSs at higher level of abstraction. Our ultimate goal is to develop a holistic yet compositional approach for verification and validation of CPS and enable strong theoretical guarantees regarding the safety and security of CPSs. Several use cases will be investigated and performed to validate our proposed methodologies.