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芯片有大量传感器来测量温度、电源电压、时钟时序细节。 专用处理器使用它们来调整芯片上的模拟电路，以保持其正常运行。 在更高层次上，专用计算机用于控制从厨房用具到汽车发动机和制动器以及飞机自动驾驶仪的各种设备。 这些控制系统和模拟电路的相关性在于它们的模型基于连续数学，特别是微分方程。 仿真仍然是此类系统的主要设计工具。 然而，仿真只能考虑一小部分可能的输入或操作条件，设计良好的测试用例来进行仿真是一项耗时且容易出错的任务。 这项研究旨在使这些设计的验证更加完整和自动化。 在问题变得昂贵或造成严重危害之前，形式验证在发现计算机硬件和软件中的错误方面发挥着重要作用。 这些验证方法构建了严格的数学证明，证明设计满足所有可能的输入和操作条件的关键规范。 形式验证算法的进步导致形式技术广泛应用于硬件设计，并越来越多地用于验证低级软件。 拟议的研究将数值方法与形式验证技术相结合，以实现对控制系统、模拟电路和其他使用常微分方程自然建模的领域的验证。 这项工作的根本挑战是数值计算和形式验证主要是使用不同的数学基础来开发的。 我们建议通过确定可以分析实际电路和控制系统关键属性的数值方法来实现这一目标。 其中包括优化、自动微分和基于区间算术的“验证算法”。 在每种情况下，我们都需要以一种可以在形式验证上下文中理解为引理和定理的方式来制定数值计算。 目标是创建一个逻辑严格的框架，将数值方法集成到形式验证工具中。 该框架应该足够灵活，以允许其他人结合特定于其问题领域的其他数值方法。 这些工具可以让设计人员免去当前方法的大部分繁琐的模拟工作，并在错误纠正或造成严重损害之前发现错误。