Formal Analysis of Physical Systems

点击翻译按钮获取中文摘要

With the advent of smart technologies, most of the engineered physical systems can now be characterized as computational systems composed of software and digital and/or analog hardware components, which closely interact with their continuously changing physical surroundings. The continuous and randomized nature of the analog components and physical surroundings of these (cyber) physical systems makes their computer-based analysis very challenging due to the inherent imprecision of computer arithmetic while dealing, for example, with real numbers. Thus, the accuracy of the analysis is compromised, which is extremely undesirable when systems are used in safety-critical applications, such as medicine or transportation, where an undetected bug in the system design phase may even lead to the loss of human life. The main focus of the proposed program is to overcome the above-mentioned limitations by using formal methods for analyzing physical systems. Formal methods are primarily based on using deductive reasoning or rigorous state-space evaluation for verifying system characteristics and thus can be used to analyze systems without compromising the precision and soundness of the analysis process. There is a plethora of research available for formal modeling and verification of digital and software systems. However, very few physical systems have been formally verified mainly because of lack of formalized mathematics to model and then analyse their behavior. What distinguishes the proposed research from existing work is the focus on formalizing foundational theories of Physics like Electromagnetics, Quantum or Stochastic Processes and use them to model and reason about the correctness of continuous and randomized physical systems. Moreover, besides functional analysis, we also want to focus upon performance aspects of physical systems. The ultimate goal of this research program is to provide a platform for the formal analysis of a variety of physical systems using a combination of formal technologies. The objective of the current proposal, however, is the formalization in higher-order logic of the concepts of queueing, control, electromagnetics and quantum theories to facilitate the formal reasoning about the corresponding systems within the core of a theorem prover. In order to illustrate the practical effectiveness of our results, we plan to use our formalizations for the analysis of various engineering systems in the domains of optics, photonics, electronics and avionics. The direct beneficiary of this multidisciplinary research will be the Canadian microelectronics, telecommunications and transportation industry as already shown in past and on-going collaborative projects. Furthermore, this proposal will contribute towards the training of a number of highly skilled personnel available to Canadian industry and academia in these emerging fields of science and engineering.**