Integrating Numerical Methods into Formal Verification

这项研究试图改变模拟电路和基于计算机的控制系统的设计方式。这样的设计随处可见。例如，手机包含芯片上的加速计，允许它们感知手机的方向并相应地设置屏幕图像的方向。更多的模拟电路用于摄像机、音频和无线通信。一个典型的CPU芯片有大量的传感器来测量温度、电源电压、时钟时序的细节。它们由专用处理器用来对芯片上的模拟电路进行调整，以保持其正常运行。在更高的层面上，专用计算机被用来控制从厨房电器到汽车发动机、刹车和飞机自动驾驶仪的各种设备。这些控制系统和模拟电路是相关的，因为它们的模型是基于连续数学，特别是微分方程式。模拟仍然是这类系统的主要设计工具。然而，仿真只能考虑可能的输入或运行条件中的一小部分，设计好的测试用例进行仿真是一项耗时且容易出错的任务。本研究旨在使这些设计的验证更加完整和自动化。在问题变得昂贵或造成严重危害之前，形式验证在发现计算机硬件和软件中的错误方面发挥着重要作用。这些验证方法构建了严格的数学证明，证明设计满足所有可能的输入和运行条件的关键规格。形式化验证算法的进步使得硬件设计的形式化技术得到了广泛的采用，并越来越多地用于验证底层软件。拟议的研究将把数值方法与形式化验证技术相结合，以实现对控制系统、模拟电路和其他自然地使用常微分方程式建模的领域的验证。这项工作的根本挑战是，数值计算和形式验证在很大程度上是利用不同的数学基础开发的。我们建议通过确定能够分析实际电路和控制系统的关键特性的数值方法来实现这一点。这些算法包括优化、自动微分和基于区间算术的“验证算法”。在每种情况下，我们都需要以一种可以理解为形式验证背景下的引理和定理的方式来表示数值计算。目标是创建一个逻辑上严格的框架，以便将数值方法整合到正式的验证工具中。这个框架应该足够灵活，以允许其他人结合其他特定于其问题领域的数值方法。这些工具应该会让设计人员省去当前方法的大量繁琐的模拟工作，并在纠正错误或造成严重损害之前捕获错误。

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.