Trace-automata : a formal framework for using abstraction to verify hybrid systems

This dissertation presents a new framework, trace-automata, for verifying hybrid systems. In addition, a simple, general theory of abstraction is presented, based on the idea of approximations that are liberal or conservative with respect to an abstraction function. This theory gives rise to a sound technique whereby hybrid systems are verified by constructing discrete approximations of both the implementation and the specification, and verifying that the approximate implementation satisfies the approximate specification. Trace-automata are language accepting, infinite tape automata, extended to allow multiple tapes, and to allow tapes that consist of continuous traces over the reals, as well as tapes that consist of sequences of discrete symbols. Hybrid systems are represented by automata that read some continuous tapes and some discrete tapes. Trace-automata are used to represent both the implementation and the specification of the system to be verified. Verification corresponds to demonstrating that the language accepted by the implementation is contained in that accepted by the specification. Hybrid systems are verified by constructing and verifying discrete approximations. Abstraction functions map continuous traces to discrete sequences. A liberal approximation of the system implementation is verified against a conservative approximation of the system specification. From this verification, it can be concluded that the original hybrid model satisfies the original specification. The dissertation describes a general technique for constructing discrete, liberal approximations of trace-automata representing differential equations and inclusions. In addition, trace-automata themselves can encode abstraction functions, with the result that trace-automata language containment can also be used to establish that an approximation is liberal or conservative as the case may be. These techniques are illustrated with an example verification based upon the Philips Audio Control Protocol with two agents, each capable of both transmitting and receiving. The verification is novel in that it is based upon a detailed model of the analog electrical behaviour of the bus.Science, Faculty ofComputer Science, Department ofGraduat