From states to histories

Abstract

We outline a modular method for specifying and proving safety properties about distributed systems. Data flow networks represent such systems. They are composed of encapsulated units cooperating by asynchronous message passing. The components of such networks are data flow nodes with a black box behavior specified by relations on the communication histories formed by the streams of the input/output channels. State machines described by state transition rules with input and output implement system components. Vice versa, history relations provide an abstraction of state machines. Safety properties are captured by system invariants that help to prove properties about state machines. Our approach provides a bridge from state-based system models defined by state transitions to the more abstract history views on systems and their components.