Technical Report
A Denotational Model for Mobile Many-to-Many Data-flow Networks
Author(s): R. Grosu, K. St{\o}len
Year: 1996
Number: TUM-I 9622
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,
Specification, Timing
Abstract:We present a fully abstract, denotational model for mobile, timed,
nondeterministic data-flow
networks whose components communicate in a
many-to-many 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 guarded and generic. A stream
processing
function is strongly guarded if it is contractive with
respect to the standard
metric on
streams. This property guarantees the existence of unique fix-points.
The genericity property
can be thought of as an invariant, or alternatively, a
privacy
requirement, that is satisfied by any mobile system.
It guarantees
that a function never accesses, depends on or forwards a
port whose name it
does not already know.
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 mobile
telephone network.
Available as compressed Postscript
BibTeX-Entry:
<![CDATA[
@techreport{ grosuStoelenTUMI9622,
author = {R. Grosu and K. St{\o}len},
title = {A Denotational Model for Mobile Many-to-Many Data-flow Networks},
number = {TUM-I 9622},
institution = {Technische Univerit\"at M\"unchen},
year = {1996},
url = {http://www4.informatik.tu-muenchen.de/reports/grosuStoelenTUMI9622.html},
abstract = {We present a fully abstract, denotational model for mobile, timed,
nondeterministic data-flow
networks whose components communicate in a
many-to-many 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 guarded and generic. A stream
processing
function is strongly guarded if it is contractive with
respect to the standard
metric on
streams. This property guarantees the existence of unique fix-points.
The genericity property
can be thought of as an invariant, or alternatively, a
privacy
requirement, that is satisfied by any mobile system.
It guarantees
that a function never accesses, depends on or forwards a
port whose name it
does not already know.
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 mobile
telephone network.},
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