Integrating Numerical Methods into Formal Verification

点击翻译按钮获取中文摘要

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.