icse

50 %
50 %
Information about icse
News-Reports

Published on June 19, 2007

Author: Tarzen

Source: authorstream.com

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

Add a comment

Related presentations

Related pages

ICSE conference s - ICSE Home Page

WELCOME. ICSE, the International Conference on Software Engineering,® is the premier software engineering conference, providing a forum for researchers ...
Read more

CISCE

- Curriculum development and review including preparation of the ICSE, ISC and CVE syllabi. - Design and development of Specimen Question Papers.
Read more

Indian Certificate of Secondary Education - Wikipedia, the ...

The Indian Certificate of Secondary Education (ICSE) is an examination conducted by the Council for the Indian School Certificate Examinations, a private ...
Read more

ICSE | The International Centre for Statistical Education

International Centre for Statistical Education. Welcome to the International Centre for Statistical Education (ICSE), our aim is ‘To promote the ...
Read more

ICSE - Contract Services

Meet Pharma Contract Services Providers. ICSE connects the pharmaceutical community with outsourcing solution providers, including clinical trials ...
Read more

CPhI Worldwide 2015 catalogue - Available for download now

Find products & contact the right suppliers today with CPhI Online. ... Preparing for your visit to one of our CPhI, ICSE, P-MEC or Innopack events?
Read more

37th International Conference on Software Engineering ...

Two decades after ICSE 1994 in Sorrento, we are proud to organize the 37th edition of the premier International Conference on Software Engineering® in the ...
Read more

36th International Conference on Software Engineering ...

About ICSE. ICSE, the International Conference on Software Engineering,® is the premier software engineering conference, providing a forum for researchers ...
Read more

ICSE | Bienvenido

La visión de nuestra entidad consiste en ser un centro de referencia en la formación en Canarias, distinguiéndonos por proporcionar un servicio de ...
Read more

Internet- u. Computerservice Eichhorn ltd ...

Professionelle Erstellung von Internetauftritten inkl. Webdesign, Shopsystemem oder CMS Systeme für Städte, Firmen und Vereine. Computerservice Hardware ...
Read more