User: Guest  Login
Title:

Verification Diagrams for Dataflow Properties

Document type:
Technical Report
Author(s):
Max Breitling; Jan Philipps
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 invarianc...     »
Keywords:
Verification; Proof Diagrams; theorem prover; state machines; distributed systems; Isabelle
Year:
2000
Year / month:
2000-03-01 00:00:00
Pages:
59
 BibTeX