Verification Diagrams for Dataflow Properties

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.     «

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 invarianc...     »