Black Box Views of State Machines

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, embedded systems and communication protocols. The techniques to reason about the dataflow within a system, however, are less well developed. This report adapts a UNITY-like formalism for specification and verification to systems of asynchronously communicating components. The components themselves are specified as state machines. The resulting proof techniques allows abstract and compositional reasoning about dataflow properties of systems.     «

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, embedded systems and communication protocols. The techniques to reason about the dataflow within a system, however, are less well developed. This report adapts a UNITY-like formalism for specification and verification to systems of asynchronously communicating components. The components themselves a...     »