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

安全关键网络物理系统的实用、高效和可扩展的建模、验证和确认

• 批准号: RGPIN-2020-06751
• 负责人: AitMohamed, Otmane
• 金额: $ 1.75万
• 依托单位: Concordia University
• 依托单位国家: 加拿大
• 项目类别: Discovery Grants Program - Individual
• 财政年份: 2020
• 资助国家: 加拿大
• 起止时间: 2020-01-01 至 2021-12-31
• 项目状态: 已结题
• 来源: https://www.nserc-crsng.gc.ca/ase-oro/Details-Detailles_eng.asp?id=718172
• 关键词: Practical; Efficient; Scalable; Modeling; Verification

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.

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