Technical Report
Transitions into Black Box Views - The NetBill Protocol revisited -
Author(s): Max Breitling, Jan Philipps
Year: 2000
Number: TUM-I0013
Editor:
CR Classification: F.3.1
CR General Terms: Verification
Keywords: Netbill
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 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.
Available as compressed Postscript
BibTeX-Entry:
<![CDATA[
@techreport{BP00a,
author = {Max Breitling and Jan Philipps},
title = {Transitions into Black Box Views - The NetBill Protocol revisited -},
number = {TUM-I0013},
institution = {Technische Univerit\"at M\"unchen},
year = {2000},
url = {http://www4.informatik.tu-muenchen.de/reports/BP00a.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 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.},
CRClassification = {F.3.1},
CRGenTerms = {Verification}}
]]>