User: Guest  Login
Document type:
Technical Report 
Author(s):
Max Breitling; Jan Philipps 
Title:
Verification Diagrams for Dataflow Properties 
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