Formal verification of physical systems and devices

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

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

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