- Library Home /
- Search Collections /
- Open Collections /
- Browse Collections /
- UBC Theses and Dissertations /
- Trace-automata : a formal framework for using abstraction...
Open Collections
UBC Theses and Dissertations
UBC Theses and Dissertations
Trace-automata : a formal framework for using abstraction to verify hybrid systems Martin, Andrew Kenneth
Abstract
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.
Item Metadata
Title |
Trace-automata : a formal framework for using abstraction to verify hybrid systems
|
Creator | |
Publisher |
University of British Columbia
|
Date Issued |
1996
|
Description |
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.
|
Extent |
8713850 bytes
|
Genre | |
Type | |
File Format |
application/pdf
|
Language |
eng
|
Date Available |
2009-03-27
|
Provider |
Vancouver : University of British Columbia Library
|
Rights |
For non-commercial purposes only, such as research, private study and education. Additional conditions apply, see Terms of Use https://open.library.ubc.ca/terms_of_use.
|
DOI |
10.14288/1.0051028
|
URI | |
Degree | |
Program | |
Affiliation | |
Degree Grantor |
University of British Columbia
|
Graduation Date |
1996-11
|
Campus | |
Scholarly Level |
Graduate
|
Aggregated Source Repository |
DSpace
|
Item Media
Item Citations and Data
Rights
For non-commercial purposes only, such as research, private study and education. Additional conditions apply, see Terms of Use https://open.library.ubc.ca/terms_of_use.