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

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

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.