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的安全性提供强大的理论保证。将研究并进行几种用例，以验证我们提出的方法。