Formal verification of physical systems and devices

物理系统和设备的形式验证

• 批准号: 194302-2010
• 负责人: Tahar, Sofiène
• 金额: $ 3.72万
• 依托单位: Concordia University
• 依托单位国家: 加拿大
• 项目类别: Discovery Grants Program - Individual
• 财政年份: 2014
• 资助国家: 加拿大
• 起止时间: 2014-01-01 至 2015-12-31
• 项目状态: 已结题
• 来源: https://www.nserc-crsng.gc.ca/ase-oro/Details-Detailles_eng.asp?id=546096
• 关键词: Formal; verification; physical; systems; devices

Physical systems and devices are increasingly being used in safety-critical domains, such as electronic medicine equipment and automated transportation. The verification of such systems has predominantly been accomplished by analytical techniques or simulation testing. However, as engineering systems are getting more complex the confidence level in such traditional verification techniques is rapidly decreasing. These limitations can, however, be overcome by using formal methods for the modeling and validation of physical systems through deductive reasoning. In this research program, we aim in particular at using higher-order logic based theorem proving to formally analyze and verify physical 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. Theorem proving is the field of computer science and mathematical logic concerned with precise computer based formal proof tools that require some sort of human assistance. In the proposed research, we are interested in analyzing the probabilistic and statistical behavior of systems by formalizing in higher-order logic queuing and information theory fundamentals. Immediate applications include the analysis of telecommunications systems performance, roundoff errors of arithmetic computing or error coding in digital media. We also plan to formalize specific mathematical theories widely used in the target domains of optics and aeronautics to be able to reason about properties of optical interconnects and flight control stability, respectively. Finally, we aim at investigation prospects of using numerical analysis with automated theorem proving for checking the reliability of nanoelectronics circuits. We believe that our approaches will advance the state-of-the-art in systems specification and verification, thus significantly enhancing the confidence level in the correctness of safety critical products. The direct beneficiary of this research will be the Canadian telecommunications, optics, microelectronics and aeronautics industry. Furthermore, this proposal will contribute towards the training of a number of skilled personnel available to Canadian industry and academia.

物理系统和设备越来越多地用于安全关键领域，例如电子医疗设备和自动化运输。这种系统的验证主要是通过分析技术或模拟测试来完成的。然而，随着工程系统变得越来越复杂，这种传统验证技术的置信度正在迅速下降。然而，这些局限性可以通过使用形式化的方法，通过演绎推理的物理系统的建模和验证来克服。在这项研究计划中，我们的目标是特别是在使用高阶逻辑为基础的定理证明，正式分析和验证物理系统。高阶逻辑是一个具有精确语义的演绎系统，它的表达能力足以用于几乎所有经典数学理论的规范。定理证明是计算机科学和数理逻辑的领域，涉及精确的基于计算机的形式证明工具，需要某种人类的帮助。在拟议的研究中，我们感兴趣的是通过高阶逻辑排队和信息论基础的形式化来分析系统的概率和统计行为。直接应用包括电信系统性能分析、算术计算的循环误差或数字媒体中的错误编码。我们还计划将广泛用于光学和航空目标领域的特定数学理论形式化，以便能够分别推理光学互连和飞行控制稳定性的属性。最后，我们的目的是调查前景，使用数值分析与自动定理证明，检查纳米电子电路的可靠性。我们相信，我们的方法将推进系统规范和验证的最新发展，从而显著提高安全关键产品正确性的置信水平。这项研究的直接受益者将是加拿大的电信、光学、微电子和航空工业。此外，这项建议将有助于培训加拿大工业界和学术界现有的一些技术人员。