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.