Technical Report
Verification Diagrams for Dataflow Properties
Author(s): Max Breitling, Jan Philipps
Year: 2000
Number: TUM-I0005
Editor:
CR Classification: D.2.1, D.2.4, F.3.1
CR General Terms: Verification
Keywords: Verification, Proof Diagrams, theorem prover, state machines, distributed systems, Isabelle
Abstract:State-based specification and verification techniques can be used to
derive
properties of the data flow I/O relation of distributed
systems. Safety
properties of the I/O relation are typically expressed
as a prefix relation on
streams; they can be derived from state
machine invariants. Liveness properties
are typically formulated as a
lower bound for the length of output streams;
they can be derived from
response or leadsto properties of state machines.
While the proof principles for invariance and leadsto properties are
well
known, proofs for larger systems tend to be rather complex: It is
often
difficult to get an overview over the complete proof structure,
although each
single proof step itself is quite simple and usually
consists only of the
verification of a predicate logic formula. This
report shows how verification
diagrams can be used to structure the
proofs of invariance and leadsto
properties. To provide some tool
support, the approach is formalized in the
theorem prover Isabelle.
Available as compressed Postscript
BibTeX-Entry:
<![CDATA[
@techreport{BP00,
author = {Max Breitling and Jan Philipps},
title = {Verification Diagrams for Dataflow Properties},
number = {TUM-I0005},
institution = {Technische Univerit\"at M\"unchen},
year = {2000},
url = {http://www4.informatik.tu-muenchen.de/reports/BP00.html},
abstract = {State-based specification and verification techniques can be used to
derive
properties of the data flow I/O relation of distributed
systems. Safety
properties of the I/O relation are typically expressed
as a prefix relation on
streams; they can be derived from state
machine invariants. Liveness properties
are typically formulated as a
lower bound for the length of output streams;
they can be derived from
response or leadsto properties of state machines.
While the proof principles for invariance and leadsto properties are
well
known, proofs for larger systems tend to be rather complex: It is
often
difficult to get an overview over the complete proof structure,
although each
single proof step itself is quite simple and usually
consists only of the
verification of a predicate logic formula. This
report shows how verification
diagrams can be used to structure the
proofs of invariance and leadsto
properties. To provide some tool
support, the approach is formalized in the
theorem prover Isabelle.},
CRClassification = {D.2.1, D.2.4, F.3.1},
CRGenTerms = {Verification}}
]]>