Technical Report
Black Box Views of State Machines
Author(s): Max Breitling, Jan Philipps
Year: 1999
Number: TUM-I9916
Editor:
CR Classification: D2.4, D3.1, F3.1
CR General Terms: Theory, Verification
Keywords: state machines, communication histories, verification,
compositionality
Abstract: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.
Available as compressed Postscript
BibTeX-Entry:
<![CDATA[
@techreport{BP99,
author = {Max Breitling and Jan Philipps},
title = {Black Box Views of State Machines},
number = {TUM-I9916},
institution = {Technische Univerit\"at M\"unchen},
year = {1999},
url = {http://www4.informatik.tu-muenchen.de/reports/BP99.html},
abstract = {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.},
CRClassification = {D2.4, D3.1, F3.1},
CRGenTerms = {Theory, Verification}}
]]>