icse

Information about icse

Published on June 19, 2007

Author: Tarzen

Source: authorstream.com

Content

Efficient Decentralized Monitoring of Safety in Distributed Systems :  Efficient Decentralized Monitoring of Safety in Distributed Systems Koushik Sen Abhay Vardhan Gul Agha Grigore Rosu University of Illinois at Urbana-Champaign, USA Software Reliability:  Software Reliability Software Validation Rigorous and Complete Methods Model Checking Theorem Proving Infeasible for large-scale open distributed systems Non-determinism and Asynchrony Testing Widely used Ad-Hoc Good Test Coverage Required Runtime Monitoring Adds rigor to Testing Centralized Monitoring Approach:  Centralized Monitoring Approach Monitoring – Use Formal Methods in Testing Synthesize light-weight Monitors from Specification Automata, Rewriting-based Monitors, State machines Instrument code to insert monitors Execute instrumented code Distributed System Monitoring Global state is distributed For every state update send state to a central monitor Central monitor assembles them to form consistent execution traces (Vector Clocks) Sequence of global states Monitor execution traces An Example:  An Example Mobile node a requests certain value from node b b computes the value and sends it to a Property: no node receives a value from another node to which it had not sent a request Centralized Monitoring Example:  valRcv → (valComputed  valReq) Centralized Monitoring Example valRcv → (valComputed  valReq) 'If a receives a value from b then b calculated the value after receiving request from a' valReq valComputed valRcv a b valReq valReq valComputed  valReq (valComputed  valReq) Monitor Decentralized Monitoring Approach:  Decentralized Monitoring Approach 'If a receives a value from b then b calculated the value after receiving request from a' valRcv → @b((valComputed  @a(valReq))) valReq valComputed valRcv a b valReq valRcv → @b((valComputed  @a(valReq))) (valComputed  @a(valReq)) @a(valReq) valComputed  @a(valReq) Past time Distributed Temporal Logic (pt-DTL):  Past time Distributed Temporal Logic (pt-DTL) Past Time Linear Temporal Logic [Pnueli] Extended with a Operator from epistemic logic (@) [Aumann76][Meenakshi et al. 00] Properties with respect to a process, say p Interpreted over sequence of knowledge that p has about global state Remote Formulas in pt-DTL:  Remote Formulas in pt-DTL @a F at process b @ makes remote formula F at process a local to process b 'Alarm at process b implies that there was a fire at a' alarm → @afire a formula with respect to process b Remote Expressions in pt-DTL:  Remote Expressions in pt-DTL Remote expressions – arbitrary expressions related to the state of a remote process Propositions constructed from remote and local expressions 'If my alarm is set then eventually in past difference between my temperature and temperature at process b exceeded the allowed value' alarm → ((myTemp - @btemp) andgt; allowed) Safety in Airplane Landing:  Safety in Airplane Landing ' If my airplane is landing then the runway that the airport has allocated matches the one that I am planning to use' landing → (runway = @airportallocRunway) Leader Election Example:  Leader Election Example 'If a leader is elected then if the current process is a leader then, at its knowledge, none of the other processes is a leader' elected → (state=leader → /\i≠j(@j(state ≠ leader))) pt-DTL syntax:  pt-DTL syntax Fi ::= true | false | P(Ei) | : Fi | Fi Æ Fi propositional | ¯ Fi | ¡ Fi | Fi | Fi S Fi temporal | @jFj epistemic Ei ::= c | vi 2 Vi | f(Ei) functional | @jEj epistemic Interpretation of @jEj at process i:  Interpretation of @jEj at process i p3 p1 p2 m4 m3 m2 m1 x=7 x=9 @ 1(x=9) Monitoring Algorithm:  Monitoring Algorithm Requirements Should be fast so that online monitoring is possible Little memory overhead Additional messages sent should be minimal; ideally zero KnowledgeVector:  KnowledgeVector Let KV be a vector one entry for each process appearing in formula KV[j] denotes entry for process j KV[j].seq is the sequence number of last event seen at process j KV[j].values stores values of j-expressions and j-formulae Monitoring using KnowledgeVector:  Monitoring using KnowledgeVector Maintain KnowledgeVector about global state at each process Attach KnowledgeVector with outgoing messages Update KnowledgeVector with incoming messages At each process monitor local KnowledgeVector KnowledgeVector Algorithm:  KnowledgeVector Algorithm [internal event]: (at process i) store eval(Ei,si) and eval(Fi,si) for each @iEi and @iFi in KVi[i].values [send m]: KVi[i].seq à KVi[i].seq + 1. Send KVi with m as KVm [receive m]: for all j, if KVm[j].seq andgt; KVi[j].seq then KVi[j].seq à KVm[j].seq KVi[j].values à KVm[j].value store eval(Ei,si) and eval(Fi,si) for each @iEi and @iFi in KVi[i].values Example:  Example p3 p2 p1 X=5 X=9 X=6 Y=7 Y=3 violation ¡(Y ¸ @1X) at p2 KV[1].seq KV[1].values DIANA Architecture:  DIANA Architecture pt-DTL Monitor Conclusion:  Conclusion pt-DTL can express interesting and useful safety properties of distributed systems Decentralized Technique to effectively verify Distributed Systems at runtime No extra message over-head for monitoring KnowledgeVector as monitors

Related presentations


Other presentations created by Tarzen

FastFood
24. 02. 2008
0 views

FastFood

Money Banking
14. 04. 2008
0 views

Money Banking

Nature nurture
04. 09. 2007
0 views

Nature nurture

tolkein presentation
04. 09. 2007
0 views

tolkein presentation

chapter08
16. 06. 2007
0 views

chapter08

Data Storage 1
16. 06. 2007
0 views

Data Storage 1

Best Practices
17. 04. 2008
0 views

Best Practices

Community Workshop Seminar
17. 04. 2008
0 views

Community Workshop Seminar

mohamed ariff and greg lopez
13. 04. 2008
0 views

mohamed ariff and greg lopez

20011105e1
10. 04. 2008
0 views

20011105e1

s2 dewulf
09. 04. 2008
0 views

s2 dewulf

AAAS
07. 04. 2008
0 views

AAAS

D200510 06 GermanETRforJapan
30. 03. 2008
0 views

D200510 06 GermanETRforJapan

sez10
28. 03. 2008
0 views

sez10

SouthAfrica
21. 09. 2007
0 views

SouthAfrica

Scanning Tunneling Microscope
21. 09. 2007
0 views

Scanning Tunneling Microscope

chem lab bonding 05
12. 10. 2007
0 views

chem lab bonding 05

ClassifyAnimals
12. 10. 2007
0 views

ClassifyAnimals

desc fashion en
18. 10. 2007
0 views

desc fashion en

36 Isaiah and the Mountains
04. 09. 2007
0 views

36 Isaiah and the Mountains

Lecture 6
05. 10. 2007
0 views

Lecture 6

Berlin Conference
26. 10. 2007
0 views

Berlin Conference

Vietnam
07. 12. 2007
0 views

Vietnam

mobisys tutorial hardware
29. 10. 2007
0 views

mobisys tutorial hardware

ne tutorial
01. 11. 2007
0 views

ne tutorial

Koranteng MFRD
04. 09. 2007
0 views

Koranteng MFRD

korea
07. 11. 2007
0 views

korea

Salma Hayek
12. 11. 2007
0 views

Salma Hayek

global stanton
22. 10. 2007
0 views

global stanton

Success risk factor
16. 11. 2007
0 views

Success risk factor

0738001
19. 11. 2007
0 views

0738001

Funny Not So
18. 08. 2007
0 views

Funny Not So

earthhistory
03. 10. 2007
0 views

earthhistory

Justice and Equality
14. 12. 2007
0 views

Justice and Equality

peda2
22. 10. 2007
0 views

peda2

Gavin cholera risk prediction
04. 09. 2007
0 views

Gavin cholera risk prediction

2006 09 13DeepakAgarwal
23. 10. 2007
0 views

2006 09 13DeepakAgarwal

Oak Hill2
04. 01. 2008
0 views

Oak Hill2

informedegestion2005
22. 10. 2007
0 views

informedegestion2005

ClosingSession2005
07. 01. 2008
0 views

ClosingSession2005

vogel games
07. 11. 2007
0 views

vogel games

Obesity and Risk Factor
07. 08. 2007
0 views

Obesity and Risk Factor

Linda Simoni Wastila
07. 08. 2007
0 views

Linda Simoni Wastila

mbti students intro only team
07. 08. 2007
0 views

mbti students intro only team

Module14
07. 08. 2007
0 views

Module14

mmo 42
07. 08. 2007
0 views

mmo 42

Localization Week 2
27. 11. 2007
0 views

Localization Week 2

Clinica
28. 12. 2007
0 views

Clinica

GMV DP Wizard
21. 09. 2007
0 views

GMV DP Wizard

Milner China IndiaGEP
16. 10. 2007
0 views

Milner China IndiaGEP

Lecture 31 Power Point
28. 12. 2007
0 views

Lecture 31 Power Point

sessionr 9 12 13 1107
24. 02. 2008
0 views

sessionr 9 12 13 1107

Making Your Home Safer
26. 02. 2008
0 views

Making Your Home Safer

contextualized learning
28. 02. 2008
0 views

contextualized learning

disarmament
04. 03. 2008
0 views

disarmament

ogot
07. 08. 2007
0 views

ogot

installing globus
19. 06. 2007
0 views

installing globus

JPW Talk AHM2005 MAIN
19. 06. 2007
0 views

JPW Talk AHM2005 MAIN

jensen rockwell seesymp02
19. 06. 2007
0 views

jensen rockwell seesymp02

ipv6 workshop plzak 28oct02
19. 06. 2007
0 views

ipv6 workshop plzak 28oct02

ipfrr kvalbein
19. 06. 2007
0 views

ipfrr kvalbein

Clast Mind L M 2210
19. 06. 2007
0 views

Clast Mind L M 2210

brochure 2
19. 06. 2007
0 views

brochure 2

Brandmeldeanlage
19. 06. 2007
0 views

Brandmeldeanlage

birnecker cms
19. 06. 2007
0 views

birnecker cms

belleville ppthistory
19. 06. 2007
0 views

belleville ppthistory

belleville ppt2K
19. 06. 2007
0 views

belleville ppt2K

launchevent final fnr
15. 11. 2007
0 views

launchevent final fnr

IETF 68 P2PSIP Agenda
19. 06. 2007
0 views

IETF 68 P2PSIP Agenda

MSM Slides2005
07. 08. 2007
0 views

MSM Slides2005

lacnic V APNIC Report
19. 06. 2007
0 views

lacnic V APNIC Report

learning style roles 2007 05 15
07. 08. 2007
0 views

learning style roles 2007 05 15

Global Johnny Appleseed Project
02. 11. 2007
0 views

Global Johnny Appleseed Project

belleville flash
19. 06. 2007
0 views

belleville flash

NaTang Inverse
07. 08. 2007
0 views

NaTang Inverse

Ramos Lab Tour
04. 10. 2007
0 views

Ramos Lab Tour

interims 2003b
19. 06. 2007
0 views

interims 2003b

kao tai BASS 2004
07. 08. 2007
0 views

kao tai BASS 2004

Rhew02
03. 01. 2008
0 views

Rhew02

Dale Tongue
16. 06. 2007
0 views

Dale Tongue

CS598STK Terra
16. 06. 2007
0 views

CS598STK Terra

Computer Essentials
16. 06. 2007
0 views

Computer Essentials

Coming SL 7 Overview
16. 06. 2007
0 views

Coming SL 7 Overview

CLI220 Mark Minasi
16. 06. 2007
0 views

CLI220 Mark Minasi

bpm keynote
16. 06. 2007
0 views

bpm keynote

beyond soa
16. 06. 2007
0 views

beyond soa

Intro OO Neuf
19. 06. 2007
0 views

Intro OO Neuf

PBOCFrance051219alsd1
23. 11. 2007
0 views

PBOCFrance051219alsd1

MOS384 Sel 07 test
07. 08. 2007
0 views

MOS384 Sel 07 test

NT 512B 2
07. 08. 2007
0 views

NT 512B 2

CP1 Commo
16. 06. 2007
0 views

CP1 Commo

Mark Carpenter
07. 08. 2007
0 views

Mark Carpenter

ma chap8
07. 08. 2007
0 views

ma chap8

Basic2
03. 10. 2007
0 views

Basic2

IPAM concluding workshop
19. 06. 2007
0 views

IPAM concluding workshop

michael cantor
07. 08. 2007
0 views

michael cantor

ietf 63 enum validation v01
19. 06. 2007
0 views

ietf 63 enum validation v01

KSU Speech1
07. 08. 2007
0 views

KSU Speech1

Mumulus Presentation
07. 08. 2007
0 views

Mumulus Presentation

bethel
19. 06. 2007
0 views

bethel

Mgt 201 Personality Differences
07. 08. 2007
0 views

Mgt 201 Personality Differences

ISSUES presentation
19. 06. 2007
0 views

ISSUES presentation

internet sec
19. 06. 2007
0 views

internet sec

Sathaye
24. 11. 2007
0 views

Sathaye

kline
07. 08. 2007
0 views

kline

wg2 t6
23. 10. 2007
0 views

wg2 t6

KNIT
20. 11. 2007
0 views

KNIT

Multicam2
07. 01. 2008
0 views

Multicam2

bilingual poll march2004
19. 06. 2007
0 views

bilingual poll march2004

NASC1 Lucken
07. 08. 2007
0 views

NASC1 Lucken

Corel Corporation
16. 06. 2007
0 views

Corel Corporation