Pragmatic Verification for Hybrid and Real-Time Designs

Hybrid and real-time designs are ubiquitous in computing and control systems. There are three prevalent methods for verifying real-time and hybrid systems: simulation, model checking, and theorem proving. NOne of these approaches are ideal: simulation can never verify a design for all possible inputs and parameters when these are continuous quantities; model checking methods are typically applicable for only relatively small and inexpressive models; and theorem proving requires substantial manual effort from highly skilled logicians.

This paper presents a verification approach based on refinement. In our refinement framework, we first establish safety properties for a simplified, abstract model of the design and then show that these are inhereited by progressively more detailed models. In this approach, we see a hybrid system as a hybrid model: part of the system is modeled with discrete time and state, and other parts are modeled with continuous quantities. This paper illustrates this approach with the design of a simple state-machine for a traffic light.