Integrating Numerical Methods into Formal Verification

将数值方法集成到形式验证中

• 批准号: RGPIN-2014-03926
• 负责人: Greenstreet, Mark
• 金额: $ 2.33万
• 依托单位: University of British Columbia
• 依托单位国家: 加拿大
• 项目类别: Discovery Grants Program - Individual
• 财政年份: 2015
• 资助国家: 加拿大
• 起止时间: 2015-01-01 至 2016-12-31
• 项目状态: 已结题
• 来源: https://www.nserc-crsng.gc.ca/ase-oro/Details-Detailles_eng.asp?id=587498
• 关键词: Integrating; Numerical; Methods; into; Formal

This research seeks to change the way that analog circuits and computer-based control systems are designed. Such designs are ubiquitous. For example, cell phones contain on-chip accelerometers that allow them to sense the orientation of the phone and set the orientation of the image of the screen accordingly. More analog circuitry is used for cameras, audio, and wireless communication. A typical CPU chip has an large number of sensors to measure temperature, power-supply voltage, details of clock timing. These are used by a dedicated processor to make adjustments to analog circuits on the chip to keep it operating correctly. At a higher level, dedicated computers are used to control a wide range of devices from kitchen appliances to automobile engines and brakes and aircraft autopilots. These control systems and analog circuits are related in that their models are based on continuous mathematics, especially differential equations. Simulation remains the main design tool for such systems. However, simulation can only consider a small fraction of the possible inputs or operating conditions, and devising good test cases to simulate is a time-consuming and error-prone task. This research seeks to make verification of these designs much more complete and automatic. Formal verification plays an important role in finding errors in computer hardware and software before the problems become expensive to correct or have caused serious harm. These verification methods construct rigorous mathematical proofs that the design satisfies key specifications for all possible inputs and operating conditions. Advances in algorithms for formal verification have led to the widespread adaptation of formal techniques for hardware design and a growing use for verifying low-level software. The proposed research will combine numerical methods with formal verification techniques to enable verification for control systems, analog circuits, and other domains that are naturally modeled using ordinary differential equations. The fundamental challenge for this work is that numerical computing and formal verification have been developed largely using different mathematical underpinnings. We propose to do this by identifying numerical methods that can analyse key properties of real circuits and control systems. These include optimization, automatic differentiation, and interval arithmetic based "verification algorithms". In each case, we need to formulate the numerical computations in a way that can be understood as lemmas and theorems in the formal verification context. The goal is to create a logically rigorous framework for integrating numerical methods into formal verification tools. This framework should be flexible enough to allow others to incorporate other numerical methods specific for their problem domains. These tools should spare designers much of the tedious simulation work of current approaches and catch errors before they are expensive to correct or cause serious harm.

这项研究试图改变模拟电路和基于计算机的控制系统的方式。 这样的设计无处不在。 例如，手机包含芯片加速度计，使他们能够感知手机的方向并相应地设置屏幕图像的方向。 更多模拟电路用于相机，音频和无线通信。 典型的CPU芯片具有大量传感器，可测量温度，电源供应电压，时钟正时的细节。 这些专用处理器使用这些调整，以调整芯片上的模拟电路以使其正确运行。 在更高级别上，专用计算机用于控制从厨房电器到汽车发动机，制动器和飞机自动驾驶仪的各种设备。 这些控制系统和模拟电路是相关的，因为它们的模型基于连续数学，尤其是微分方程。 模拟仍然是此类系统的主要设计工具。 但是，仿真只能考虑可能的输入或操作条件的一小部分，并且设计良好的测试用例模拟是一项耗时且容易出错的任务。 这项研究旨在使这些设计的验证更加完整和自动。 在问题变得昂贵或造成严重伤害之前，正式验证在查找计算机硬件和软件中的错误中起着重要作用。 这些验证方法构建了严格的数学证明，即该设计满足所有可能的输入和操作条件的关键规格。 正式验证算法的进步导致了用于硬件设计的正式技术的广泛适应，并越来越多地用于验证低级软件。 拟议的研究将将数值方法与形式验证技术相结合，以验证控制系统，模拟电路和其他使用普通微分方程自然建模的域。 这项工作的基本挑战是数值计算和形式验证主要是使用不同的数学基础开发的。 我们建议通过识别可以分析实际电路和控制系统的关键特性的数值方法来做到这一点。 这些包括优化，自动分化和基于间隔算术的“验证算法”。 在每种情况下，我们都需要以一种可以理解为正式验证环境中的引理和定理的方式来制定数值计算。 目标是创建一个在逻辑上进行严格的框架，以将数值方法集成到正式验证工具中。 该框架应足够灵活，以允许其他人合并针对其问题域的其他数值方法。 这些工具应保留设计人员的许多乏味的模拟工作，并在纠正或造成严重伤害之前捕获错误。