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.