Formal Verification of 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.