zbMATH — the first resource for mathematics

From states to histories relating state and history views onto systems. (English) Zbl 0989.68091
Hoare, Tony (ed.) et al., Engineering theories of software construction. Proceedings of the NATO ASI, Marktoberdorf, Germany, July 25 - August 6, 2000. Amsterdam: IOS Press. NATO Sci. Ser. III, Comput. Syst. Sci. 180, 149-186 (2001).
Summary: We present a method for the modular specification and abstract implementation of distributed systems as well as for proving their safety and liveness properties. We represent systems by data flow nets. These systems consist of encapsulated subsystems called components cooperating by asynchronous message passing. The components of such nets are data flow nodes. Their black box behavior is specified by relational specifications. Relational specifications describe relations, called history relations, on the communication histories of the input/output channels. State machines are described by state transition rules with input and output. State machines implement systems. History relations are an abstraction of state machines. State machines provide implementations of history relations. Safety properties are captured by logical formulas called system invariants. We work with such invariants to prove safety properties about state machines. Liveness properties of state machines are represented by formulas of linear time temporal logic. This way we provide a methodological bridge from state-based system models defined by state transitions to the more abstract history-based models.
For the entire collection see [Zbl 0972.00060].
68Q60 Specification and verification (program logics, model checking, etc.)
68M14 Distributed systems