Formal Verification of Physical Systems

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

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.