| Summary: | 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.
|
|---|
