Formal Verification of Physical Systems

物理系统的形式验证

• 批准号: RGPIN-2020-05545
• 负责人: Tahar, Sofiene
• 金额: $ 2.99万
• 依托单位: 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=716441
• 关键词: Formal; Verification; Physical; Systems

Modern age embedded systems are characterized by mechanisms that make smart decisions by computationally manipulating the data collected through sensors and other physical devices to intelligently communicate this information with humans and other smart systems. These physical devices are increasingly being used in safety-critical domains, such as transportation, healthcare, power distribution, and military, and hence must rigorously ensure (1) functional correctness (2); required performance (timing, weight, power, cost); and (3) necessary dependability, comprising of reliability, availability, maintainability and safety constraints. These assurances are traditionally established by mathematically modeling the physical properties of the given device along with dynamic and randomized aspects, and then using paper-and-pencil proof methods or computer simulations for analyzing the functional correctness, performance and dependability of the device model. However, as these physical devices are getting smaller and more complex, the confidence level in such traditional verification techniques is rapidly decreasing due to the error-prone nature of paper-and-pencil based analysis and incompleteness of simulation. We propose to overcome these limitations by using higher-order-logic theorem proving as a unified framework to formally analyze the functional correctness, performance and dependability of physical components of embedded systems. Higher-order logic is a system of deduction with a precise semantics and is expressive enough to be used for the specification of almost all classical mathematics theories and henceforth mathematical physics. In particular, we plan to develop formal reasoning support for partial differential equations based on the formalization of transform methods, like Laplace, Fourier and Z, as well as the formalization of multi-dimensional transform methods. For performance analysis, we aim to provide formal reasoning support in higher-order logic for intrinsic probabilistic and stochastic behaviors like tolerance to noise and error rates by extending the formalization of continuous-time Markov chains (CTMC) in higher-order logic to handle Queuing theory, which is a widely used mathematical tool for performance analysis. Finally, for dependability, we plan to formalize dynamic reliability models based on Markov chains as well as the multistate reliability theory, which will allow us to formally reason about availability and maintainability as well as the impact of change in time on the reliability of physical system. Immediate applications of the proposed research include autonomous vehicles, e-health apparatus and avionics image processing. The direct beneficiary of this multidisciplinary research will be the Canadian automotive, aeronautics, e-health and telecommunications industry. Furthermore, this proposal will contribute towards the training of a number of highly skilled personnel available to Canadian industry and academia.

现代嵌入式系统的特征在于通过计算操纵通过传感器和其他物理设备收集的数据以智能地与人类和其他智能系统通信该信息来做出智能决策的机制。这些物理设备越来越多地用于安全关键领域，例如运输，医疗保健，配电和军事，因此必须严格确保（1）功能正确性（2）;所需性能（时序，重量，功率，成本）;以及（3）必要的可靠性，包括可靠性，可用性，可维护性和安全约束。这些保证传统上是通过对给定器件的物理特性沿着动态和随机方面进行数学建模来建立的，然后使用纸笔证明方法或计算机模拟来分析器件模型的功能正确性、性能和可靠性。然而，随着这些物理设备变得越来越小和越来越复杂，由于基于纸和笔的分析的易出错性质和模拟的不完整性，这种传统验证技术中的置信度水平正在迅速降低。我们建议克服这些限制，使用高阶逻辑定理证明作为一个统一的框架，正式分析嵌入式系统的物理组件的功能正确性，性能和可靠性。高阶逻辑是一个具有精确语义的演绎系统，它的表达能力足以用于几乎所有经典数学理论和数学物理的规范。特别是，我们计划开发形式化的推理支持偏微分方程的基础上的形式化的变换方法，如拉普拉斯，傅立叶和Z，以及多维变换方法的形式化。对于性能分析，我们的目标是提供正式的推理支持，在高阶逻辑的内在概率和随机行为，如容忍噪声和错误率，通过扩展的形式化的连续时间马尔可夫链（CTMC）在高阶逻辑处理的马尔可夫理论，这是一个广泛使用的数学工具，性能分析。最后，对于可靠性，我们计划形式化的动态可靠性模型的基础上，马尔可夫链以及多态可靠性理论，这将使我们能够正式原因的可用性和可维护性，以及在时间上的变化对物理系统的可靠性的影响。拟议研究的直接应用包括自动驾驶汽车，电子健康设备和航空电子图像处理。这项多学科研究的直接受益者将是加拿大的汽车、航空、电子保健和电信行业。此外，这项建议将有助于为加拿大工业界和学术界培训一些高技能人员。