From States to Histories Manfred Broy broy@informatik.tu-muenchen.de Institut für Informatik Technische Universität München D-80290 München, Germany

WADT'99

We outline a modular method for the specification and for proving safety properties of distributed systems cooperating by asynchronous message passing. Safety properties are captured by logical formulas that are system invariants. We study systems represented by data flow networks of stream processing functions and state transition machines. The components are data flow nodes with a behavior described by a relational specification for the input/output channels or by state transition rules with input and output. We work with two kind of invariants, one for state machines and one for I/O-relations. While I/O-relations are an abstraction of state machines, state machines provide implementations of I/O-relations. This way we provide a bridge between the glass box views given by state-based system models defined by state transitions and the more abstract black box views on systems and their components for which we describe their behavior exclusively in terms of relations between the communication histories.