Loading presentation...

Present Remotely

Send the link below via email or IM

Copy

Present to your audience

Start remote presentation

  • Invited audience members will follow you as you navigate and present
  • People invited to a presentation do not need a Prezi account
  • This link expires 10 minutes after you close the presentation
  • A maximum of 30 users can follow your presentation
  • Learn more about this feature in our knowledge base article

Do you really want to delete this prezi?

Neither you, nor the coeditors you shared it with will be able to recover it again.

DeleteCancel

Make your likes visible on Facebook?

Connect your Facebook account to Prezi and let your likes appear on your timeline.
You can change this under Settings & Account at any time.

No, thanks

On Recovering from Run-time Misbehaviour in ADR*

Paper for ICE2013 by Kyriakos Poyias and Emilio Tuosto
by

Kyriakos Poyias

on 2 August 2013

Comments (0)

Please log in to add your comment.

Report abuse

Transcript of On Recovering from Run-time Misbehaviour in ADR*

On Recovering from Run-time Misbehaviour in ADR
Kyriakos Poyias and Emilio Tuosto
Department of Computer Science
That's me!
station:
cluster:
noChain:
chain:
shipOFF:
shipON:
ship:
manyShips:
[cl(u1,u2): ,
cluster
]
[cl1(u3,u2): ,
station
]
[cl2(u1,u3): , ]
[ap1(u1,u3): , ]
[ch1(u7,u4): , ]
[ch3(u9,u6): , ]
[ch2(u8,u5): ,
chain
]
[sh1(u10,u5): , ]
[ms1(u8,u10): , ]
[cl(u1,u2): ,
cluster
]
[cl1(u3,u2): ,
station
]
[cl2(u1,u3): , ]
[ap1(u1,u3): , ]
[ch1(u7,u4): , ]
[ch3(u9,u6): , ]
[ch2(u8,u5): , ]
[cl(u1,u2): ,
cluster
]
[cl1(u3,u2): , ]
[cl2(u1,u3): , ]
[cl(u1,u2): , ]
u1
u2
u3
u2
u1
u1
u3
u2
u4
u7
u5
u6
u9
u8
u2
u4
u5
u6
u7
u10
u9
u8
u3
u1
cluster:
station:
chain:
connectShip(x3):
manyShips
(x1,x2)
manyShips
(x1,
manyShips
(x2,x3))
manyShips
manyShips
manyShips
x1
x2
x1
x2
x3
u2
u4
u5
u6
u7
u10
u9
u8
u3
u1
u11
[cl(u1,u2): ,
cluster
]
[cl1(u3,u2): ,
station
]
[cl2(u1,u3): , ]
[ap1(u1,u3): , ]
[ch1(u7,u4): , ]
[ch3(u9,u6): , ]
[ch2(u8,u5): ,
chain
]
[sh1(u10,u5): , ]
[ms1(u8,u10): ,
manyShips
]
[ms2(u8,u10): , ]
[ms3(u11,u10): , ]
manyShips:
u2
u4
u5
u6
u7
u10
u9
u11
u3
u1
u12
[cl(u1,u2): ,
cluster
]
[cl1(u3,u2): ,
station
]
[cl2(u1,u3): , ]
[ap1(u1,u3): , ]
[ch1(u7,u4): , ]
[ch3(u9,u6): , ]
[ch2(u8,u5): ,
chain
]
[sh1(u10,u5): , ]
[ms1(u8,u10): ,
manyShips
]
[ms2(u8,u10): , ]
[ms3(u11,u10): ,
manyShips
]
u8
[ms5(u12,u10): , ]
[ms4(u11,u10): , ]
manyShips:
cl:
cl1:
cl2:
cl2:
cl2:
ap1:
ch1:
ch2:
ch3:
ch1:
cl2:
ap1:
ch3:
sh1:
ms1:
ch1:
cl2:
ap1:
ch3:
sh1:
ms2:
ms3:
ch1:
cl2:
ap1:
ch3:
sh1:
ms2:
ms4:
ms5:
[ms1(u8,u10): ,
manyShips
]
[ms2(u8,u10): , ]
[ms3(u11,u10): ,
manyShips
]
[ms5(u12,u10): , ]
[ms4(u11,u10): , ]
u10
u11
u12
u8
ms2:
ms4:
ms5:
G :
L
v1
v3
v2
v4
e3:
e2:
e1:
u10
u11
u12
u8
ms2:
ms4:
ms5:
G :
R
u13
u2
u4
u5
u6
u7
u9
u3
u1
ch1:
cl2:
ap1:
ch3:
sh1:
u10
u11
u12
u8
ms2:
ms4:
ms5:
u13
[cl(u1,u2): ,
cluster
]
[cl1(u3,u2): ,
station
]
[cl2(u1,u3): , ]
[ap1(u1,u3): , ]
[ch1(u7,u4): , ]
[ch3(u9,u6): , ]
[ch2(u8,u5): ,
chain
]
[sh1(u10,u5): , ]
[ms1(u8,u10): ,
manyShips
]
[ms2(u8,u10): , ]
[de1(u11,u10): ,
manyShips
]
[ms6(u13,u10): , ]
[ms3(u11,u10): ,
manyShips
]
[ms5(u12,u10): , ]
[ms4(u11,u10): , ]
Last Year
u2
u4
u3
u6
u7
u9
u1
ch1:
ap1:
ch3:
sh1:
u9
sh2:
sh3:
u12
u8
u2
u4
u6
u7
u9
u1
ch1:
ap1:
ch3:
bs1:
u9
sh2:
sh3:
u12
u8
u3
Check if a given graph satisfies a given invariant
invariant: (For Every AND For Every ) There should Exist a OR a connected to them on their second tentacle
For every production
p
If graph* satisfies weakestPre(
p
,
inv
) then
Apply
tmpP
to graph
break
end if
end for
class void FixGraph (SequenceOfProductions
P

, invariant
inv
)
tmpP
+=
p
else
FixGraph(
tmpP
, weakestPre(
p
,
inv
))
tmpP
=
P
end
cluster:
Design Productions:
Run-time Reconfigurations:
transfer:
cluster
(
cluster
(x1,x2),x3)
cluster
(x1,
cluster
(x3,x2))
add(x4):
cluster
(
cluster
(x1,x2),x3)
cluster
(
cluster
(x1,x2),
cluster
(x3,x4))
reconfiguration: LHS RHS
Pre-condition
Post-condition
Weakest pre-condition ( cluster , Post-condition)
L. Lambrinos and C. Djouvas, "Creating a maritime wireless mesh infrastructure for real-time applications" in the Mobile Computing and Emerging Communication Networks workshop, 2011
u9
bs2:
sh3:
u12
u8
u3
u9
u12
u8
u3
No more assumptions.
Identify the graph using the derivation tree
Now we can:
Identify which part of the graph has been reconfigured
therefore: which part if any caused the violation
Use the derivation tree to parse the graph
bs1:
bs2:
bs3:
bs1:
[ch2(u8,u3): ,chain]
[sh1(u8,u3): , shipOFF ]
[ms1(u9,u8): , manyShips ]
[ms2(u9,u8): , ship ]
[ms3(u12,u8): , ship ]
[sh2(u9,u8): , ]
[sh3(u12,u8): , ]
[bs1(u8,u3): , ]
bs1:
u9
ms1:
u8
u3
bs1:
u9
ms1:
u8
u3
Use last year's methodology on the parsed graph
Use last year's methodology on the affected area
If graph is not fixed:
Wireless mesh infrastructure for real-time applications
Thank You
u
G
0
G
1
G
n-1
G
n
P
1
P
2
P
n-1
P
n
T
0
T
1
T
n-1
T
n
G
n+1
R
1
T
n+1
G
n+2
R
2
T
n+2
The Big Picture
G :
1
G :
0
T :
0
T :
1
G :
2
T :
2
G :
3
T :
3
G :
4
T :
4
G :
5
T :
5
G
0
G
1
G
n-1
G
n
P
1
P
2
P
n-1
P
n
T
0
T
1
T
n-1
T
n
G
n+1
R
1
T
n+1
G
n+2
R
2
T
n+2
INV
ICE12 methodology
G
0
G
1
G
n-1
G
n
P
1
P
2
P
n-1
P
n
T
0
T
1
T
n-1
T
n
G
n+1
R
1
T
n+1
G
n+2
R
2
T
n+2
INV
ICE12 methodology
sT
n+1
sG
n+1
Full transcript