Technical Report
A Denotational Model for Mobile Point-to-Point Data-flow Networks with Channel Sharing
Author(s): R. Grosu, K. Stølen, M. Broy
Year: 1997
Number: TUM-I 9724
Editor:
CR Classification: C.2.1, D.1.3, D.1.7, D.2.1, D.2.2, D.2.4, D.3.2, D.4.1,
F.1.1, F.1.2, F.3.2
CR General Terms: Design, Languages, Theory
Keywords: Denotational Model, Data-flow, Input/Output Relation,
Mobile System, Many-to-many Communication,
Point-to-point communication, Specification, Timing
Abstract:We present a fully abstract, denotational model for mobile, timed,
nondeterministic data-flow
networks whose components communicate in a
point-to-point fashion. In this model components and
networks of components are
represented by sets of stream processing functions. Each stream
processing
function is required to be strongly pulse-driven and
privacy preserving.
A
function is strongly pulse-driven if it is contractive with respect
to the
metric on streams. This property guarantees the existence of
unique fix-points.
The privacy preservation property can be thought of
as an invariant specific to
mobile point-to-point systems.
Firstly, it guarantees
that a function never
accesses, depends on or forwards a port whose
name it does not already
know.
Secondly, it guarantees that at the same point in time
no port is known to
more than two components, namely the
sender and the receiver.
Our model
allows the description of a wide variety of networks - in
particular, the
description of unbounded nondeterministic networks. We
demonstrate some
features of
our model by specifying a communication central.
Available as compressed Postscript
BibTeX-Entry:
<![CDATA[
@techreport{ grosuStoelenBroyTUMI9724,
author = {R. Grosu and K. St\olen and M. Broy},
title = {A Denotational Model for Mobile Point-to-Point Data-flow Networks with Channel Sharing},
number = {TUM-I 9724},
institution = {Technische Univerit\"at M\"unchen},
year = {1997},
url = {http://www4.informatik.tu-muenchen.de/reports/grosuStoelenBroyTUMI9724.html},
abstract = {We present a fully abstract, denotational model for mobile, timed,
nondeterministic data-flow
networks whose components communicate in a
point-to-point fashion. In this model components and
networks of components are
represented by sets of stream processing functions. Each stream
processing
function is required to be strongly pulse-driven and
privacy preserving.
A
function is strongly pulse-driven if it is contractive with respect
to the
metric on streams. This property guarantees the existence of
unique fix-points.
The privacy preservation property can be thought of
as an invariant specific to
mobile point-to-point systems.
Firstly, it guarantees
that a function never
accesses, depends on or forwards a port whose
name it does not already
know.
Secondly, it guarantees that at the same point in time
no port is known to
more than two components, namely the
sender and the receiver.
Our model
allows the description of a wide variety of networks - in
particular, the
description of unbounded nondeterministic networks. We
demonstrate some
features of
our model by specifying a communication central.},
CRClassification = {C.2.1, D.1.3, D.1.7, D.2.1, D.2.2, D.2.4, D.3.2, D.4.1,
F.1.1, F.1.2, F.3.2},
CRGenTerms = {Design, Languages, Theory}
grosu@informatik.tu-muenchen.de
}
]]>
http://www4.informatik.tu-muenchen.de/~grosu