System specification by state machines together with property specification and verification by temporal logics are by now standard techniques to reason about the control flow of hardware components and embedded systems. The techniques to reason about the dataflow within loosely coupled systems, however, are less well developed. In this contribution, we propose a formalism for the verification of systems with asynchronously communicating components. The components themselves are specified as state machines, while the dataflow between components is described as a relation over the input and output histories of a system. Communication history properties are derived from temporal logic properties of the component state machines. The history properties can then be used to deduce global properties of a complete system. To demonstrate our approach, we model the Netbill protocol for micro-payments in the Internet and prove some correctness properties.     «

System specification by state machines together with property specification and verification by temporal logics are by now standard techniques to reason about the control flow of hardware components and embedded systems. The techniques to reason about the dataflow within loosely coupled systems, however, are less well developed. In this contribution, we propose a formalism for the verification of systems with asynchronously communicating components. The components themselves are specified as sta...     »