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.