ppt - Dipartimento di Informatica
Download
Report
Transcript ppt - Dipartimento di Informatica
Agile Meeting, 8-9 July 2004
CommUnity, Tiles and
Connectors
Ivan Lanese
Dipartimento di Informatica
Università di Pisa
joint work with
Roberto Bruni
José Luiz Fiadeiro
Antónia Lopes
Ugo Montanari
Roadmap
Motivation
From CommUnity to
Tiles
Connectors
Concluding remarks
CommUnity, Tiles and Connectors
Roadmap
Motivation
From CommUnity to
Tiles
Connectors
Concluding remarks
CommUnity, Tiles and Connectors
General motivation I
Comparing the categorical and the algebraic
approach to systems
Categorical approach
Algebraic approach
CommUnity, Tiles and Connectors
General motivation II
Comparing the categorical and the algebraic
approach to systems
Categorical approach
objects are system components
morphisms express simulation, refinement, …
complex systems are modeled as diagrams
composition via universal construction (colimit)
Algebraic approach
CommUnity, Tiles and Connectors
General motivation III
Comparing the categorical and the algebraic
approach to systems
Categorical approach
Algebraic approach
System represented by an algebra
constants are basic components
operations compose smaller systems into larger ones
structural axioms collapse structurally equivalent systems
operational semantics (SOS style)
abstract semantics (bisimilarity)
CommUnity, Tiles and Connectors
Specific aim
Reconcile two selected representatives
CommUnity (categorical)
architectural description language
distinction between computation and coordination
Tile Model (algebraic)
operational model for concurrent systems
co-existence of horizontal (space) and vertical (time)
dimensions
CommUnity, Tiles and Connectors
Specific aim: advantages
Advantage: transfer of concepts and
techniques
Semantics model for CommUnity
Observational equivalence of CommUnity
configurations
CommUnity-like connectors in the tile model
Separation between computation and
coordination for tiles
CommUnity, Tiles and Connectors
Roadmap
Motivation
From CommUnity to
Tiles
Connectors
Concluding remarks
CommUnity, Tiles and Connectors
From CommUnity to Tiles
Aim:
To define the operational and abstract semantics of
CommUnity diagrams by translating them to tiles
First step
Standard decomposition of programs and diagrams
identify basic building blocks
make the translation easier
Second step
From standard diagrams to tiles
basic programs to basic boxes
cables, glues and morphisms (coordination) modeled as
connectors
CommUnity, Tiles and Connectors
Results
The translation of a diagram is tile bisimilar to the
translation of its colimit [IFIP-TCS 2004]
Corollary: Diagrams with the same colimit are mapped
to tile bisimilar configurations
Colimit axiomatization [Ongoing work!]
add suitable axioms for connectors
the translation of a diagram is equal up-to-axioms to
the translation of its colimit
axioms bisimulate (correctness)
existence of normal forms … hopefully!
CommUnity, Tiles and Connectors
Why Standard Decomposition
Decomposition is part of the translation
Decomposition is necessary to achieve
colimit axiomatization
the axiomatization of connectors cannot change
the number of computational entities
decomposition allows to have the same number
of computational entities in the diagram and in
the colimit
CommUnity, Tiles and Connectors
Standard Decomposition
Illustrated
P
glue
cables
Channel / guard
managers
CommUnity, Tiles and Connectors
Standard Decomposition
Illustrated
• n output channels
• m actions
P
•
•
•
•
n channel managers
m guard managers
n+m cables
1 glue
CommUnity, Tiles and Connectors
Channel Manager
one channel manager for each output variable x of P
variables needed
in assignments
input channels
i
i
i
i
i
i
channel
manager
for x
channel for x
output channel
o
CommUnity, Tiles and Connectors
actions
one action
true x:= …
for each
assignement
Guard Manager
one guard manager for each action a of P
variables needed
in the guard
input channels
i
i
i
i
i
i
guard
manager
for a
no output channel
CommUnity, Tiles and Connectors
one action
Q skip
Glue
one glue
all channels of P
i
i
input channels
i
i
i
i
no output channel
CommUnity, Tiles and Connectors
actions
one action
true skip
for each
action of P
Cables
one cable for each manager
one input channel
for each
channel of the role
input channels
i
i
i
i
i
i
no output channel
Morphisms are obvious
CommUnity, Tiles and Connectors
actions
one action
true skip
for each
action of the role
Scheme of the translation
channel
manager
…
state
channel
fusion
channel
manager
guard
manager
…
guard
manager
CommUnity, Tiles and Connectors
action
synchronization
through
connectors
Notation
Since:
In CommUnity initial and final configuration are always
equal (apart from values in state)
We shall consider only two kinds of observations
1
action performed / action not performed
We use a “flat” notation for tiles
CommUnity, Tiles and Connectors
0
Tiles for components
actions of managers are mutually exclusive, but
at least one action (e.g. ) must be executed
i
i
i
i
i
i
i
i
i
i
i
i
o
channel
manager
for x
i
i
i
channel
manager
for x
i
…
o
i
i
o
CommUnity, Tiles and Connectors
channel
manager
for x
Roadmap
Motivation
From CommUnity to
Tiles
Connectors
Concluding remarks
CommUnity, Tiles and Connectors
Connectors
Connectors are used to model diagram
morphisms, cables and glues
Connectors with the same abstract
semantics should be identified
they express constraints on local choices
different ways of modeling the same constraint
How?
Axioms + reduction to normal form
CommUnity, Tiles and Connectors
Abstract semantics
Connectors can be seen as black boxes
input interface
2
3
output interface
4
admissible signals on interfaces
1
1
2
3
CommUnity, Tiles and Connectors
1
2
3
4
1
2
3
Abstract semantics
Connectors can be seen as black boxes
input interface
2
3
output interface
4
admissible signals on interfaces
1
…
001
111
…
…
cells are filled with empty/id copies of matrices
CommUnity, Tiles and Connectors
3
4
n inputs
rows
0010
0101
m outputs 2m columns
…
input/output swap is transposition
sequential composition is matrix multiplication
parallel composition is matrix expansion
2n
1
2
3
3
Abstract semantics is just a matrix
1
2
1
2
domain is
{input 3, outputs 1,2,3}
An example: Symmetries
connectors boxes
are immaterial
00
00
01
11
11
=
01
10
10
CommUnity, Tiles and Connectors
AND-Connectors
=
00
0
1
01
10
11
=
CommUnity, Tiles and Connectors
AND-Tables and
Normal Form
n = m = 0 or 0 < n m
entry with empty domain is enabled
entries are closed under (domains)
only one entry with empty input/output is enabled
union
intersection
difference
complementation
…
…
at most one entry enabled for every row/column
exactly one entry for every row
CommUnity, Tiles and Connectors
co-AND-Connectors
=
0
00
1
01
(transposition
of AND table)
=
10
11
CommUnity, Tiles and Connectors
Mixed-AND-Connectors
=
=
CommUnity, Tiles and Connectors
Mixed-AND-Connectors
=
=
CommUnity, Tiles and Connectors
Mixed-AND-Connectors
=
=
=
CommUnity, Tiles and Connectors
Mixed-AND-Connectors
=
=
=
CommUnity, Tiles and Connectors
Mixed-AND-Connectors
=
=
=
CommUnity, Tiles and Connectors
Mixed-AND-Tables and
Normal Form
n = m = 0 or 0 < n,m
entry with empty domain is enabled
entries are closed under (domains)
only one entry with empty input/output is enabled
union
intersection
difference
complementation
…
…
…
at most one entry enabled for every row/column
exactly one entry for every row
CommUnity, Tiles and Connectors
HIDE-Connectors (and co-)
!
!
!
=
!
.
0
1
=
!
!
!
.
0
1
=
!
CommUnity, Tiles and Connectors
.
A Relevant Difference
.
00
01
10
11
.
!
00
!
01
10
!
11
!
!
!
CommUnity, Tiles and Connectors
A Sample Proof
!
=
!
!
=
!
=
!
CommUnity, Tiles and Connectors
SYNC-Tables and
Normal Form
n = m = 0 or 0 < n,m
entry with empty domain is enabled
entries are closed under (domains)
only one entry with empty input/output is enabled
union
intersection
difference
complementation
…
…
…
!
!
…
at most one entry enabled for every row/column
exactly one entry for every row
CommUnity, Tiles and Connectors
MEX-Connectors
=
00
0
1
01
10
11
=
CommUnity, Tiles and Connectors
co-MEX-Connectors
Transposed tables
Symmetric axioms
CommUnity, Tiles and Connectors
Mixed-MEX-Connectors
=
CommUnity, Tiles and Connectors
Mixed-MEX-Connectors
=
CommUnity, Tiles and Connectors
Mixed-MEX-Connectors
=
CommUnity, Tiles and Connectors
Mixed-MEX-Connectors
=
CommUnity, Tiles and Connectors
Mixed-MEX-Connectors
=
CommUnity, Tiles and Connectors
ZERO-Connectors
=
0
00
01
10
11
00
x
0
1
1
01
10
=
0
0
1
1
11
0
0
def
=
0
!
.
CommUnity, Tiles and Connectors
1
Some Axioms About ZERO
0
=
0
=
.
=
0
!
0
0
=
=
0
0
0
=
=
0
!
CommUnity, Tiles and Connectors
0
A Sample Proof
0
0
=
!
0
0
=
!
0
=
!
0
=
.
CommUnity, Tiles and Connectors
Some Axioms About MEX-AND
=
=
CommUnity, Tiles and Connectors
Key Axioms
CommUnity, Tiles and Connectors
Key Axioms
=
!
!
!
=
!
!
CommUnity, Tiles and Connectors
An Axiom Scheme
!
n
=
!
CommUnity, Tiles and Connectors
……
……
!
!
n
!
Finally (almost) FULL-Tables
n = m = 0 or 0 < n,m
entry with empty domain is enabled
entries are closed under (domains)
only one entry with empty input/outputs
union
intersection
difference
complementation
at most one entry enabled for every row/column
exactly one entry for every row
CommUnity, Tiles and Connectors
FULL-Tables and
Normal Form
!
!
…
…
!
CommUnity, Tiles and Connectors
…
!
…
!
…
!
…
ONE-Connector
!
1
def
0
1
.
1
All tables can now be defined, but
=
“negation” is introduced…
… and “inconsistent” connectors with it!
ONE is not needed for CommUnity
CommUnity, Tiles and Connectors
Roadmap
Motivation
From CommUnity to
Tiles
Connectors
Concluding remarks
CommUnity, Tiles and Connectors
Concluding Remarks
We have learned that reconciling the
categorical and algebraic approach is not an
easy task…
We got some insights on further extensions
more labels, weights
Related to constraint solving
CommUnity, Tiles and Connectors
Future work
Still one open problem
On the mapping from CommUnity to tiles
is the axiom schema really needed?
locations
reconfigurations
refining
More in general
what happens if we choose other algebraic and
categorical formalisms?
CommUnity, Tiles and Connectors