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.