Analysis of DSR Protocol in Event-B
Identifieur interne : 002391 ( Istex/Corpus ); précédent : 002390; suivant : 002392Analysis of DSR Protocol in Event-B
Auteurs : Dominique Méry ; Neeraj Kumar SinghSource :
- Lecture Notes in Computer Science [ 0302-9743 ]
Abstract
Abstract: This paper presents an incremental formal development of the Dynamic Source Routing (DSR) protocol in Event-B. DSR is a reactive routing protocol, which finds a route for a destination on demand, whenever communication is needed. Route discovery is an important task of any routing algorithm and formal specification of it, itself is a challenging problem. The specification is performed in a stepwise manner composing more advanced routing components between the abstract specification and topology. It is verified through a series of refinements. The specification includes safety properties as set of invariants, and liveness properties that characterize when the system reaches stable states. We establish these properties by proof of invariants, event refinement and deadlock freedom. The consequence of this incremental approach helps to achieve a high degree of automatic proof. Our approach can be useful for formalizing and developing other kinds of reactive routing protocols (i.e. AODV etc.).
Url:
DOI: 10.1007/978-3-642-24550-3_30
Links to Exploration step
ISTEX:99F497AB2E858B39775632C7B44DBA83DA5E9FE3Le document en format XML
<record><TEI wicri:istexFullTextTei="biblStruct"><teiHeader><fileDesc><titleStmt><title xml:lang="en">Analysis of DSR Protocol in Event-B</title><author><name sortKey="Mery, Dominique" sort="Mery, Dominique" uniqKey="Mery D" first="Dominique" last="Méry">Dominique Méry</name><affiliation><mods:affiliation>LORIA, Université Henri Poincaré Nancy 1, BP 239, 54506, Vandoeuvre lès Nancy, France</mods:affiliation></affiliation><affiliation><mods:affiliation>E-mail: mery@loria.fr</mods:affiliation></affiliation></author><author><name sortKey="Singh, Neeraj Kumar" sort="Singh, Neeraj Kumar" uniqKey="Singh N" first="Neeraj Kumar" last="Singh">Neeraj Kumar Singh</name><affiliation><mods:affiliation>LORIA, Université Henri Poincaré Nancy 1, BP 239, 54506, Vandoeuvre lès Nancy, France</mods:affiliation></affiliation><affiliation><mods:affiliation>E-mail: singhnne@loria.fr</mods:affiliation></affiliation></author></titleStmt><publicationStmt><idno type="wicri:source">ISTEX</idno><idno type="RBID">ISTEX:99F497AB2E858B39775632C7B44DBA83DA5E9FE3</idno><date when="2011" year="2011">2011</date><idno type="doi">10.1007/978-3-642-24550-3_30</idno><idno type="url">https://api.istex.fr/ark:/67375/HCB-35RQZ2RP-Z/fulltext.pdf</idno><idno type="wicri:Area/Istex/Corpus">002391</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">002391</idno></publicationStmt><sourceDesc><biblStruct><analytic><title level="a" type="main" xml:lang="en">Analysis of DSR Protocol in Event-B</title><author><name sortKey="Mery, Dominique" sort="Mery, Dominique" uniqKey="Mery D" first="Dominique" last="Méry">Dominique Méry</name><affiliation><mods:affiliation>LORIA, Université Henri Poincaré Nancy 1, BP 239, 54506, Vandoeuvre lès Nancy, France</mods:affiliation></affiliation><affiliation><mods:affiliation>E-mail: mery@loria.fr</mods:affiliation></affiliation></author><author><name sortKey="Singh, Neeraj Kumar" sort="Singh, Neeraj Kumar" uniqKey="Singh N" first="Neeraj Kumar" last="Singh">Neeraj Kumar Singh</name><affiliation><mods:affiliation>LORIA, Université Henri Poincaré Nancy 1, BP 239, 54506, Vandoeuvre lès Nancy, France</mods:affiliation></affiliation><affiliation><mods:affiliation>E-mail: singhnne@loria.fr</mods:affiliation></affiliation></author></analytic><monogr></monogr><series><title level="s" type="main" xml:lang="en">Lecture Notes in Computer Science</title><idno type="ISSN">0302-9743</idno><idno type="eISSN">1611-3349</idno><idno type="ISSN">0302-9743</idno></series></biblStruct></sourceDesc><seriesStmt><idno type="ISSN">0302-9743</idno></seriesStmt></fileDesc><profileDesc><textClass></textClass></profileDesc></teiHeader><front><div type="abstract" xml:lang="en">Abstract: This paper presents an incremental formal development of the Dynamic Source Routing (DSR) protocol in Event-B. DSR is a reactive routing protocol, which finds a route for a destination on demand, whenever communication is needed. Route discovery is an important task of any routing algorithm and formal specification of it, itself is a challenging problem. The specification is performed in a stepwise manner composing more advanced routing components between the abstract specification and topology. It is verified through a series of refinements. The specification includes safety properties as set of invariants, and liveness properties that characterize when the system reaches stable states. We establish these properties by proof of invariants, event refinement and deadlock freedom. The consequence of this incremental approach helps to achieve a high degree of automatic proof. Our approach can be useful for formalizing and developing other kinds of reactive routing protocols (i.e. AODV etc.).</div></front></TEI><istex><corpusName>springer-ebooks</corpusName><author><json:item><name>Dominique Méry</name><affiliations><json:string>LORIA, Université Henri Poincaré Nancy 1, BP 239, 54506, Vandoeuvre lès Nancy, France</json:string><json:string>E-mail: mery@loria.fr</json:string></affiliations></json:item><json:item><name>Neeraj Kumar Singh</name><affiliations><json:string>LORIA, Université Henri Poincaré Nancy 1, BP 239, 54506, Vandoeuvre lès Nancy, France</json:string><json:string>E-mail: singhnne@loria.fr</json:string></affiliations></json:item></author><subject><json:item><lang><json:string>eng</json:string></lang><value>Abstract model</value></json:item><json:item><lang><json:string>eng</json:string></lang><value>Event-B</value></json:item><json:item><lang><json:string>eng</json:string></lang><value>Event-driven approach</value></json:item><json:item><lang><json:string>eng</json:string></lang><value>Proof-based development</value></json:item><json:item><lang><json:string>eng</json:string></lang><value>Refinement</value></json:item><json:item><lang><json:string>eng</json:string></lang><value>Ad hoc Network</value></json:item></subject><arkIstex>ark:/67375/HCB-35RQZ2RP-Z</arkIstex><language><json:string>eng</json:string></language><originalGenre><json:string>OriginalPaper</json:string></originalGenre><abstract>Abstract: This paper presents an incremental formal development of the Dynamic Source Routing (DSR) protocol in Event-B. DSR is a reactive routing protocol, which finds a route for a destination on demand, whenever communication is needed. Route discovery is an important task of any routing algorithm and formal specification of it, itself is a challenging problem. The specification is performed in a stepwise manner composing more advanced routing components between the abstract specification and topology. It is verified through a series of refinements. The specification includes safety properties as set of invariants, and liveness properties that characterize when the system reaches stable states. We establish these properties by proof of invariants, event refinement and deadlock freedom. The consequence of this incremental approach helps to achieve a high degree of automatic proof. Our approach can be useful for formalizing and developing other kinds of reactive routing protocols (i.e. AODV etc.).</abstract><qualityIndicators><score>8.788</score><pdfWordCount>7471</pdfWordCount><pdfCharCount>39317</pdfCharCount><pdfVersion>1.6</pdfVersion><pdfPageCount>15</pdfPageCount><pdfPageSize>429.725 x 659.895 pts</pdfPageSize><refBibsNative>false</refBibsNative><abstractWordCount>149</abstractWordCount><abstractCharCount>1013</abstractCharCount><keywordCount>6</keywordCount></qualityIndicators><title>Analysis of DSR Protocol in Event-B</title><chapterId><json:string>30</json:string><json:string>Chap30</json:string></chapterId><genre><json:string>conference</json:string></genre><serie><title>Lecture Notes in Computer Science</title><language><json:string>unknown</json:string></language><copyrightDate>2011</copyrightDate><issn><json:string>0302-9743</json:string></issn><eissn><json:string>1611-3349</json:string></eissn><editor><json:item><name>David Hutchison</name><affiliations><json:string>Lancaster University, Lancaster, UK</json:string></affiliations></json:item><json:item><name>Takeo Kanade</name><affiliations><json:string>Carnegie Mellon University, Pittsburgh, PA, USA</json:string></affiliations></json:item><json:item><name>Josef Kittler</name><affiliations><json:string>University of Surrey, Guildford, UK</json:string></affiliations></json:item><json:item><name>Jon M. Kleinberg</name><affiliations><json:string>Cornell University, Ithaca, NY, USA</json:string></affiliations></json:item><json:item><name>Friedemann Mattern</name><affiliations><json:string>ETH Zurich, Zurich, Switzerland</json:string></affiliations></json:item><json:item><name>John C. Mitchell</name><affiliations><json:string>Stanford University, Stanford, CA, USA</json:string></affiliations></json:item><json:item><name>Moni Naor</name><affiliations><json:string>Weizmann Institute of Science, Rehovot, Israel</json:string></affiliations></json:item><json:item><name>Oscar Nierstrasz</name><affiliations><json:string>University of Bern, Bern, Switzerland</json:string></affiliations></json:item><json:item><name>C. Pandu Rangan</name><affiliations><json:string>Indian Institute of Technology, Madras, India</json:string></affiliations></json:item><json:item><name>Bernhard Steffen</name><affiliations><json:string>University of Dortmund, Dortmund, Germany</json:string></affiliations></json:item><json:item><name>Madhu Sudan</name><affiliations><json:string>Massachusetts Institute of Technology, MA, USA</json:string></affiliations></json:item><json:item><name>Demetri Terzopoulos</name><affiliations><json:string>University of California, Los Angeles, CA, USA</json:string></affiliations></json:item><json:item><name>Doug Tygar</name><affiliations><json:string>University of California, Berkeley, CA, USA</json:string></affiliations></json:item><json:item><name>Moshe Y. Vardi</name><affiliations><json:string>Rice University, Houston, TX, USA</json:string></affiliations></json:item><json:item><name>Gerhard Weikum</name><affiliations><json:string>Max-Planck Institute of Computer Science, Saarbrücken, Germany</json:string></affiliations></json:item></editor></serie><host><title>Stabilization, Safety, and Security of Distributed Systems</title><language><json:string>unknown</json:string></language><copyrightDate>2011</copyrightDate><doi><json:string>10.1007/978-3-642-24550-3</json:string></doi><issn><json:string>0302-9743</json:string></issn><eissn><json:string>1611-3349</json:string></eissn><eisbn><json:string>978-3-642-24550-3</json:string></eisbn><bookId><json:string>978-3-642-24550-3</json:string></bookId><isbn><json:string>978-3-642-24549-7</json:string></isbn><volume>6976</volume><pages><first>401</first><last>415</last></pages><genre><json:string>book-series</json:string></genre><editor><json:item><name>Xavier Défago</name><affiliations><json:string>School of Information Science, Japan Advanced Institute of Science and Technology (JAIST), Ishikawa, Japan</json:string><json:string>E-mail: defago@jaist.ac.jp</json:string></affiliations></json:item><json:item><name>Franck Petit</name><affiliations><json:string>LIP6/INRIA/UPMC Sorbonne Universities, Paris, France</json:string><json:string>E-mail: franck.petit@lip6.fr</json:string></affiliations></json:item><json:item><name>Vincent Villain</name><affiliations><json:string>University of Picardie Jules Verne, Picardie, France</json:string><json:string>E-mail: vincent.villain@u-picardie.fr</json:string></affiliations></json:item></editor><subject><json:item><value>Computer Science</value></json:item><json:item><value>Computer Science</value></json:item><json:item><value>Computer Communication Networks</value></json:item><json:item><value>Special Purpose and Application-Based Systems</value></json:item><json:item><value>Computation by Abstract Devices</value></json:item><json:item><value>Algorithm Analysis and Problem Complexity</value></json:item><json:item><value>Systems and Data Security</value></json:item><json:item><value>Management of Computing and Information Systems</value></json:item></subject></host><ark><json:string>ark:/67375/HCB-35RQZ2RP-Z</json:string></ark><publicationDate>2011</publicationDate><copyrightDate>2011</copyrightDate><doi><json:string>10.1007/978-3-642-24550-3_30</json:string></doi><id>99F497AB2E858B39775632C7B44DBA83DA5E9FE3</id><score>1</score><fulltext><json:item><extension>pdf</extension><original>true</original><mimetype>application/pdf</mimetype><uri>https://api.istex.fr/ark:/67375/HCB-35RQZ2RP-Z/fulltext.pdf</uri></json:item><json:item><extension>zip</extension><original>false</original><mimetype>application/zip</mimetype><uri>https://api.istex.fr/ark:/67375/HCB-35RQZ2RP-Z/bundle.zip</uri></json:item><istex:fulltextTEI uri="https://api.istex.fr/ark:/67375/HCB-35RQZ2RP-Z/fulltext.tei"><teiHeader><fileDesc><titleStmt><title level="a" type="main" xml:lang="en">Analysis of DSR Protocol in Event-B</title></titleStmt><publicationStmt><authority>ISTEX</authority><availability><licence>Springer-Verlag Berlin Heidelberg</licence></availability><date when="2011">2011</date></publicationStmt><notesStmt><note type="conference" source="proceedings" scheme="https://content-type.data.istex.fr/ark:/67375/XTP-BFHXPBJJ-3">conference</note><note type="publication-type" subtype="book-series" scheme="https://publication-type.data.istex.fr/ark:/67375/JMC-0G6R5W5T-Z">book-series</note></notesStmt><sourceDesc><biblStruct><analytic><title level="a" type="main" xml:lang="en">Analysis of DSR Protocol in Event-B</title><author><persName><forename type="first">Dominique</forename><surname>Méry</surname></persName><email>mery@loria.fr</email><affiliation><orgName type="department">LORIA</orgName><orgName type="institution">Université Henri Poincaré Nancy 1</orgName><address><postBox>BP 239</postBox><postCode>54506</postCode><settlement>Vandoeuvre lès Nancy</settlement><country key="FR">FRANCE</country></address></affiliation></author><author><persName><forename type="first">Neeraj</forename><forename type="first">Kumar</forename><surname>Singh</surname></persName><email>singhnne@loria.fr</email><affiliation><orgName type="department">LORIA</orgName><orgName type="institution">Université Henri Poincaré Nancy 1</orgName><address><postBox>BP 239</postBox><postCode>54506</postCode><settlement>Vandoeuvre lès Nancy</settlement><country key="FR">FRANCE</country></address></affiliation></author><idno type="istex">99F497AB2E858B39775632C7B44DBA83DA5E9FE3</idno><idno type="ark">ark:/67375/HCB-35RQZ2RP-Z</idno><idno type="DOI">10.1007/978-3-642-24550-3_30</idno></analytic><monogr><title level="m" type="main">Stabilization, Safety, and Security of Distributed Systems</title><title level="m" type="sub">13th International Symposium, SSS 2011, Grenoble, France, October 10-12, 2011. Proceedings</title><idno type="DOI">10.1007/978-3-642-24550-3</idno><idno type="book-id">978-3-642-24550-3</idno><idno type="ISBN">978-3-642-24549-7</idno><idno type="eISBN">978-3-642-24550-3</idno><idno type="chapter-id">Chap30</idno><editor><persName><forename type="first">Xavier</forename><surname>Défago</surname></persName><email>defago@jaist.ac.jp</email><affiliation><orgName type="department">School of Information Science</orgName><orgName type="institution">Japan Advanced Institute of Science and Technology (JAIST)</orgName><address><settlement>Ishikawa</settlement><country key="JP">JAPAN</country></address></affiliation></editor><editor><persName><forename type="first">Franck</forename><surname>Petit</surname></persName><email>franck.petit@lip6.fr</email><affiliation><orgName type="institution">LIP6/INRIA/UPMC Sorbonne Universities</orgName><address><settlement>Paris</settlement><country key="FR">FRANCE</country></address></affiliation></editor><editor><persName><forename type="first">Vincent</forename><surname>Villain</surname></persName><email>vincent.villain@u-picardie.fr</email><affiliation><orgName type="institution">University of Picardie Jules Verne</orgName><address><settlement>Picardie</settlement><country key="FR">FRANCE</country></address></affiliation></editor><imprint><biblScope unit="vol">6976</biblScope><biblScope unit="page" from="401">401</biblScope><biblScope unit="page" to="415">415</biblScope><biblScope unit="chapter-count">41</biblScope></imprint></monogr><series><title level="s" type="main" xml:lang="en">Lecture Notes in Computer Science</title><editor><persName><forename type="first">David</forename><surname>Hutchison</surname></persName><affiliation><orgName type="institution">Lancaster University</orgName><address><settlement>Lancaster</settlement><country key="GB">UNITED KINGDOM</country></address></affiliation></editor><editor><persName><forename type="first">Takeo</forename><surname>Kanade</surname></persName><affiliation><orgName type="institution">Carnegie Mellon University</orgName><address><settlement>Pittsburgh</settlement><region>PA</region><country key="US">UNITED STATES</country></address></affiliation></editor><editor><persName><forename type="first">Josef</forename><surname>Kittler</surname></persName><affiliation><orgName type="institution">University of Surrey</orgName><address><settlement>Guildford</settlement><country key="GB">UNITED KINGDOM</country></address></affiliation></editor><editor><persName><forename type="first">Jon</forename><forename type="first">M.</forename><surname>Kleinberg</surname></persName><affiliation><orgName type="institution">Cornell University</orgName><address><settlement>Ithaca</settlement><region>NY</region><country key="US">UNITED STATES</country></address></affiliation></editor><editor><persName><forename type="first">Friedemann</forename><surname>Mattern</surname></persName><affiliation><orgName type="institution">ETH Zurich</orgName><address><settlement>Zurich</settlement><country key="CH">SWITZERLAND</country></address></affiliation></editor><editor><persName><forename type="first">John</forename><forename type="first">C.</forename><surname>Mitchell</surname></persName><affiliation><orgName type="institution">Stanford University</orgName><address><settlement>Stanford</settlement><region>CA</region><country key="US">UNITED STATES</country></address></affiliation></editor><editor><persName><forename type="first">Moni</forename><surname>Naor</surname></persName><affiliation><orgName type="institution">Weizmann Institute of Science</orgName><address><settlement>Rehovot</settlement><country key="IL">ISRAEL</country></address></affiliation></editor><editor><persName><forename type="first">Oscar</forename><surname>Nierstrasz</surname></persName><affiliation><orgName type="institution">University of Bern</orgName><address><settlement>Bern</settlement><country key="CH">SWITZERLAND</country></address></affiliation></editor><editor><persName><forename type="first">C.</forename><surname>Pandu Rangan</surname></persName><affiliation><orgName type="institution">Indian Institute of Technology</orgName><address><settlement>Madras</settlement><country key="IN">INDIA</country></address></affiliation></editor><editor><persName><forename type="first">Bernhard</forename><surname>Steffen</surname></persName><affiliation><orgName type="institution">University of Dortmund</orgName><address><settlement>Dortmund</settlement><country key="DE">GERMANY</country></address></affiliation></editor><editor><persName><forename type="first">Madhu</forename><surname>Sudan</surname></persName><affiliation><orgName type="institution">Massachusetts Institute of Technology</orgName><address><region>MA</region><country key="US">UNITED STATES</country></address></affiliation></editor><editor><persName><forename type="first">Demetri</forename><surname>Terzopoulos</surname></persName><affiliation><orgName type="institution">University of California</orgName><address><settlement>Los Angeles</settlement><region>CA</region><country key="US">UNITED STATES</country></address></affiliation></editor><editor><persName><forename type="first">Doug</forename><surname>Tygar</surname></persName><affiliation><orgName type="institution">University of California</orgName><address><settlement>Berkeley</settlement><region>CA</region><country key="US">UNITED STATES</country></address></affiliation></editor><editor><persName><forename type="first">Moshe</forename><forename type="first">Y.</forename><surname>Vardi</surname></persName><affiliation><orgName type="institution">Rice University</orgName><address><settlement>Houston</settlement><region>TX</region><country key="US">UNITED STATES</country></address></affiliation></editor><editor><persName><forename type="first">Gerhard</forename><surname>Weikum</surname></persName><affiliation><orgName type="institution">Max-Planck Institute of Computer Science</orgName><address><settlement>Saarbrücken</settlement><country key="DE">GERMANY</country></address></affiliation></editor><idno type="pISSN">0302-9743</idno><idno type="eISSN">1611-3349</idno><idno type="seriesID">558</idno></series></biblStruct></sourceDesc></fileDesc><profileDesc><abstract xml:lang="en"><head>Abstract</head><p>This paper presents an incremental formal development of the Dynamic Source Routing (DSR) protocol in Event-B. DSR is a reactive routing protocol, which finds a route for a destination on demand, whenever communication is needed. Route discovery is an important task of any routing algorithm and formal specification of it, itself is a challenging problem. The specification is performed in a stepwise manner composing more advanced routing components between the abstract specification and topology. It is verified through a series of refinements. The specification includes safety properties as set of invariants, and liveness properties that characterize when the system reaches stable states. We establish these properties by proof of invariants, event refinement and deadlock freedom. The consequence of this incremental approach helps to achieve a high degree of automatic proof. Our approach can be useful for formalizing and developing other kinds of reactive routing protocols (i.e. AODV etc.).</p></abstract><textClass ana="keyword"><keywords xml:lang="en"><term>Abstract model</term><term>Event-B</term><term>Event-driven approach</term><term>Proof-based development</term><term>Refinement</term><term>Ad hoc Network</term></keywords></textClass><textClass ana="subject"><keywords scheme="book-subject-collection"><list><label>SUCO11645</label><item><term>Computer Science</term></item></list></keywords></textClass><textClass ana="subject"><keywords scheme="book-subject"><list><label>I</label><item><term type="Primary">Computer Science</term></item><label>I13022</label><item><term type="Secondary" subtype="priority-1">Computer Communication Networks</term></item><label>I13030</label><item><term type="Secondary" subtype="priority-2">Special Purpose and Application-Based Systems</term></item><label>I16013</label><item><term type="Secondary" subtype="priority-3">Computation by Abstract Devices</term></item><label>I16021</label><item><term type="Secondary" subtype="priority-4">Algorithm Analysis and Problem Complexity</term></item><label>I14050</label><item><term type="Secondary" subtype="priority-5">Systems and Data Security</term></item><label>I24067</label><item><term type="Secondary" subtype="priority-6">Management of Computing and Information Systems</term></item></list></keywords></textClass><langUsage><language ident="EN"></language></langUsage></profileDesc></teiHeader></istex:fulltextTEI><json:item><extension>txt</extension><original>false</original><mimetype>text/plain</mimetype><uri>https://api.istex.fr/ark:/67375/HCB-35RQZ2RP-Z/fulltext.txt</uri></json:item></fulltext><metadata><istex:metadataXml wicri:clean="corpus springer-ebooks not found" wicri:toSee="no header"><istex:xmlDeclaration>version="1.0" encoding="UTF-8"</istex:xmlDeclaration><istex:docType PUBLIC="-//Springer-Verlag//DTD A++ V2.4//EN" URI="http://devel.springer.de/A++/V2.4/DTD/A++V2.4.dtd" name="istex:docType"></istex:docType><istex:document><Publisher><PublisherInfo><PublisherName>Springer Berlin Heidelberg</PublisherName><PublisherLocation>Berlin, Heidelberg</PublisherLocation></PublisherInfo><Series><SeriesInfo SeriesType="Series" TocLevels="0"><SeriesID>558</SeriesID><SeriesPrintISSN>0302-9743</SeriesPrintISSN><SeriesElectronicISSN>1611-3349</SeriesElectronicISSN><SeriesTitle Language="En">Lecture Notes in Computer Science</SeriesTitle></SeriesInfo><SeriesHeader><EditorGroup><Editor AffiliationIDS="Aff1"><EditorName DisplayOrder="Western"><GivenName>David</GivenName><FamilyName>Hutchison</FamilyName></EditorName></Editor><Editor AffiliationIDS="Aff2"><EditorName DisplayOrder="Western"><GivenName>Takeo</GivenName><FamilyName>Kanade</FamilyName></EditorName></Editor><Editor AffiliationIDS="Aff3"><EditorName DisplayOrder="Western"><GivenName>Josef</GivenName><FamilyName>Kittler</FamilyName></EditorName></Editor><Editor AffiliationIDS="Aff4"><EditorName DisplayOrder="Western"><GivenName>Jon</GivenName><GivenName>M.</GivenName><FamilyName>Kleinberg</FamilyName></EditorName></Editor><Editor AffiliationIDS="Aff5"><EditorName DisplayOrder="Western"><GivenName>Friedemann</GivenName><FamilyName>Mattern</FamilyName></EditorName></Editor><Editor AffiliationIDS="Aff6"><EditorName DisplayOrder="Western"><GivenName>John</GivenName><GivenName>C.</GivenName><FamilyName>Mitchell</FamilyName></EditorName></Editor><Editor AffiliationIDS="Aff7"><EditorName DisplayOrder="Western"><GivenName>Moni</GivenName><FamilyName>Naor</FamilyName></EditorName></Editor><Editor AffiliationIDS="Aff8"><EditorName DisplayOrder="Western"><GivenName>Oscar</GivenName><FamilyName>Nierstrasz</FamilyName></EditorName></Editor><Editor AffiliationIDS="Aff9"><EditorName DisplayOrder="Western"><GivenName>C.</GivenName><FamilyName>Pandu Rangan</FamilyName></EditorName></Editor><Editor AffiliationIDS="Aff10"><EditorName DisplayOrder="Western"><GivenName>Bernhard</GivenName><FamilyName>Steffen</FamilyName></EditorName></Editor><Editor AffiliationIDS="Aff11"><EditorName DisplayOrder="Western"><GivenName>Madhu</GivenName><FamilyName>Sudan</FamilyName></EditorName></Editor><Editor AffiliationIDS="Aff12"><EditorName DisplayOrder="Western"><GivenName>Demetri</GivenName><FamilyName>Terzopoulos</FamilyName></EditorName></Editor><Editor AffiliationIDS="Aff13"><EditorName DisplayOrder="Western"><GivenName>Doug</GivenName><FamilyName>Tygar</FamilyName></EditorName></Editor><Editor AffiliationIDS="Aff14"><EditorName DisplayOrder="Western"><GivenName>Moshe</GivenName><GivenName>Y.</GivenName><FamilyName>Vardi</FamilyName></EditorName></Editor><Editor AffiliationIDS="Aff15"><EditorName DisplayOrder="Western"><GivenName>Gerhard</GivenName><FamilyName>Weikum</FamilyName></EditorName></Editor><Affiliation ID="Aff1"><OrgName>Lancaster University</OrgName><OrgAddress><City>Lancaster</City><Country>UK</Country></OrgAddress></Affiliation><Affiliation ID="Aff2"><OrgName>Carnegie Mellon University</OrgName><OrgAddress><City>Pittsburgh</City><State>PA</State><Country>USA</Country></OrgAddress></Affiliation><Affiliation ID="Aff3"><OrgName>University of Surrey</OrgName><OrgAddress><City>Guildford</City><Country>UK</Country></OrgAddress></Affiliation><Affiliation ID="Aff4"><OrgName>Cornell University</OrgName><OrgAddress><City>Ithaca</City><State>NY</State><Country>USA</Country></OrgAddress></Affiliation><Affiliation ID="Aff5"><OrgName>ETH Zurich</OrgName><OrgAddress><City>Zurich</City><Country>Switzerland</Country></OrgAddress></Affiliation><Affiliation ID="Aff6"><OrgName>Stanford University</OrgName><OrgAddress><City>Stanford</City><State>CA</State><Country>USA</Country></OrgAddress></Affiliation><Affiliation ID="Aff7"><OrgName>Weizmann Institute of Science</OrgName><OrgAddress><City>Rehovot</City><Country>Israel</Country></OrgAddress></Affiliation><Affiliation ID="Aff8"><OrgName>University of Bern</OrgName><OrgAddress><City>Bern</City><Country>Switzerland</Country></OrgAddress></Affiliation><Affiliation ID="Aff9"><OrgName>Indian Institute of Technology</OrgName><OrgAddress><City>Madras</City><Country>India</Country></OrgAddress></Affiliation><Affiliation ID="Aff10"><OrgName>University of Dortmund</OrgName><OrgAddress><City>Dortmund</City><Country>Germany</Country></OrgAddress></Affiliation><Affiliation ID="Aff11"><OrgName>Massachusetts Institute of Technology</OrgName><OrgAddress><State>MA</State><Country>USA</Country></OrgAddress></Affiliation><Affiliation ID="Aff12"><OrgName>University of California</OrgName><OrgAddress><City>Los Angeles</City><State>CA</State><Country>USA</Country></OrgAddress></Affiliation><Affiliation ID="Aff13"><OrgName>University of California</OrgName><OrgAddress><City>Berkeley</City><State>CA</State><Country>USA</Country></OrgAddress></Affiliation><Affiliation ID="Aff14"><OrgName>Rice University</OrgName><OrgAddress><City>Houston</City><State>TX</State><Country>USA</Country></OrgAddress></Affiliation><Affiliation ID="Aff15"><OrgName>Max-Planck Institute of Computer Science</OrgName><OrgAddress><City>Saarbrücken</City><Country>Germany</Country></OrgAddress></Affiliation></EditorGroup></SeriesHeader><Book Language="En"><BookInfo BookProductType="Proceedings" ContainsESM="No" Language="En" MediaType="eBook" NumberingDepth="2" NumberingStyle="ContentOnly" OutputMedium="All" TocLevels="0"><BookID>978-3-642-24550-3</BookID><BookTitle>Stabilization, Safety, and Security of Distributed Systems</BookTitle><BookSubTitle>13th International Symposium, SSS 2011, Grenoble, France, October 10-12, 2011. Proceedings</BookSubTitle><BookVolumeNumber>6976</BookVolumeNumber><BookSequenceNumber>6976</BookSequenceNumber><BookDOI>10.1007/978-3-642-24550-3</BookDOI><BookTitleID>273633</BookTitleID><BookPrintISBN>978-3-642-24549-7</BookPrintISBN><BookElectronicISBN>978-3-642-24550-3</BookElectronicISBN><BookChapterCount>41</BookChapterCount><BookCopyright><CopyrightHolderName>Springer-Verlag GmbH Berlin Heidelberg</CopyrightHolderName><CopyrightYear>2011</CopyrightYear></BookCopyright><BookSubjectGroup><BookSubject Code="I" Type="Primary">Computer Science</BookSubject><BookSubject Code="I13022" Priority="1" Type="Secondary">Computer Communication Networks</BookSubject><BookSubject Code="I13030" Priority="2" Type="Secondary">Special Purpose and Application-Based Systems</BookSubject><BookSubject Code="I16013" Priority="3" Type="Secondary">Computation by Abstract Devices</BookSubject><BookSubject Code="I16021" Priority="4" Type="Secondary">Algorithm Analysis and Problem Complexity</BookSubject><BookSubject Code="I14050" Priority="5" Type="Secondary">Systems and Data Security</BookSubject><BookSubject Code="I24067" Priority="6" Type="Secondary">Management of Computing and Information Systems</BookSubject><SubjectCollection Code="SUCO11645">Computer Science</SubjectCollection></BookSubjectGroup><BookContext><SeriesID>558</SeriesID></BookContext></BookInfo><BookHeader><EditorGroup><Editor AffiliationIDS="Aff16"><EditorName DisplayOrder="Western"><GivenName>Xavier</GivenName><FamilyName>Défago</FamilyName></EditorName><Contact><Email>defago@jaist.ac.jp</Email></Contact></Editor><Editor AffiliationIDS="Aff17"><EditorName DisplayOrder="Western"><GivenName>Franck</GivenName><FamilyName>Petit</FamilyName></EditorName><Contact><Email>franck.petit@lip6.fr</Email></Contact></Editor><Editor AffiliationIDS="Aff18"><EditorName DisplayOrder="Western"><GivenName>Vincent</GivenName><FamilyName>Villain</FamilyName></EditorName><Contact><Email>vincent.villain@u-picardie.fr</Email></Contact></Editor><Affiliation ID="Aff16"><OrgDivision>School of Information Science</OrgDivision><OrgName>Japan Advanced Institute of Science and Technology (JAIST)</OrgName><OrgAddress><City>Ishikawa</City><Country>Japan</Country></OrgAddress></Affiliation><Affiliation ID="Aff17"><OrgName>LIP6/INRIA/UPMC Sorbonne Universities</OrgName><OrgAddress><City>Paris</City><Country>France</Country></OrgAddress></Affiliation><Affiliation ID="Aff18"><OrgName>University of Picardie Jules Verne</OrgName><OrgAddress><City>Picardie</City><Country>France</Country></OrgAddress></Affiliation></EditorGroup></BookHeader><Chapter ID="Chap30" Language="En"><ChapterInfo ChapterType="OriginalPaper" ContainsESM="No" NumberingDepth="2" NumberingStyle="ContentOnly" TocLevels="0"><ChapterID>30</ChapterID><ChapterDOI>10.1007/978-3-642-24550-3_30</ChapterDOI><ChapterSequenceNumber>30</ChapterSequenceNumber><ChapterTitle Language="En">Analysis of DSR Protocol in Event-B</ChapterTitle><ChapterFirstPage>401</ChapterFirstPage><ChapterLastPage>415</ChapterLastPage><ChapterCopyright><CopyrightHolderName>Springer-Verlag Berlin Heidelberg</CopyrightHolderName><CopyrightYear>2011</CopyrightYear></ChapterCopyright><ChapterGrants Type="Regular"><MetadataGrant Grant="OpenAccess"></MetadataGrant><AbstractGrant Grant="OpenAccess"></AbstractGrant><BodyPDFGrant Grant="Restricted"></BodyPDFGrant><BodyHTMLGrant Grant="Restricted"></BodyHTMLGrant><BibliographyGrant Grant="Restricted"></BibliographyGrant><ESMGrant Grant="Restricted"></ESMGrant></ChapterGrants><ChapterContext><SeriesID>558</SeriesID><BookID>978-3-642-24550-3</BookID><BookTitle>Stabilization, Safety, and Security of Distributed Systems</BookTitle></ChapterContext></ChapterInfo><ChapterHeader><AuthorGroup><Author AffiliationIDS="Aff19"><AuthorName DisplayOrder="Western"><GivenName>Dominique</GivenName><FamilyName>Méry</FamilyName></AuthorName><Contact><Email>mery@loria.fr</Email></Contact></Author><Author AffiliationIDS="Aff19"><AuthorName DisplayOrder="Western"><GivenName>Neeraj</GivenName><GivenName>Kumar</GivenName><FamilyName>Singh</FamilyName></AuthorName><Contact><Email>singhnne@loria.fr</Email></Contact></Author><Affiliation ID="Aff19"><OrgDivision>LORIA</OrgDivision><OrgName>Université Henri Poincaré Nancy 1</OrgName><OrgAddress><Postbox>BP 239</Postbox><Postcode>54506</Postcode><City>Vandoeuvre lès Nancy</City><Country>France</Country></OrgAddress></Affiliation></AuthorGroup><Abstract ID="Abs1" Language="En"><Heading>Abstract</Heading><Para>This paper presents an incremental formal development of the Dynamic Source Routing (DSR) protocol in Event-B. DSR is a reactive routing protocol, which finds a route for a destination on demand, whenever communication is needed. Route discovery is an important task of any routing algorithm and formal specification of it, itself is a challenging problem. The specification is performed in a stepwise manner composing more advanced routing components between the abstract specification and topology. It is verified through a series of refinements. The specification includes safety properties as set of invariants, and liveness properties that characterize when the system reaches stable states. We establish these properties by proof of invariants, event refinement and deadlock freedom. The consequence of this incremental approach helps to achieve a high degree of automatic proof. Our approach can be useful for formalizing and developing other kinds of reactive routing protocols (i.e. AODV etc.).</Para></Abstract><KeywordGroup Language="En"><Heading>Keywords</Heading><Keyword>Abstract model</Keyword><Keyword>Event-B</Keyword><Keyword>Event-driven approach</Keyword><Keyword>Proof-based development</Keyword><Keyword>Refinement</Keyword><Keyword>Ad hoc Network</Keyword></KeywordGroup></ChapterHeader><NoBody></NoBody></Chapter></Book></Series></Publisher></istex:document></istex:metadataXml><mods version="3.6"><titleInfo lang="en"><title>Analysis of DSR Protocol in Event-B</title></titleInfo><titleInfo type="alternative" contentType="CDATA"><title>Analysis of DSR Protocol in Event-B</title></titleInfo><name type="personal"><namePart type="given">Dominique</namePart><namePart type="family">Méry</namePart><affiliation>LORIA, Université Henri Poincaré Nancy 1, BP 239, 54506, Vandoeuvre lès Nancy, France</affiliation><affiliation>E-mail: mery@loria.fr</affiliation><role><roleTerm type="text">author</roleTerm></role></name><name type="personal"><namePart type="given">Neeraj</namePart><namePart type="given">Kumar</namePart><namePart type="family">Singh</namePart><affiliation>LORIA, Université Henri Poincaré Nancy 1, BP 239, 54506, Vandoeuvre lès Nancy, France</affiliation><affiliation>E-mail: singhnne@loria.fr</affiliation><role><roleTerm type="text">author</roleTerm></role></name><typeOfResource>text</typeOfResource><genre displayLabel="OriginalPaper" authority="ISTEX" authorityURI="https://content-type.data.istex.fr" type="conference" valueURI="https://content-type.data.istex.fr/ark:/67375/XTP-BFHXPBJJ-3">conference</genre><originInfo><publisher>Springer Berlin Heidelberg</publisher><place><placeTerm type="text">Berlin, Heidelberg</placeTerm></place><dateIssued encoding="w3cdtf">2011</dateIssued><copyrightDate encoding="w3cdtf">2011</copyrightDate></originInfo><language><languageTerm type="code" authority="rfc3066">en</languageTerm><languageTerm type="code" authority="iso639-2b">eng</languageTerm></language><abstract lang="en">Abstract: This paper presents an incremental formal development of the Dynamic Source Routing (DSR) protocol in Event-B. DSR is a reactive routing protocol, which finds a route for a destination on demand, whenever communication is needed. Route discovery is an important task of any routing algorithm and formal specification of it, itself is a challenging problem. The specification is performed in a stepwise manner composing more advanced routing components between the abstract specification and topology. It is verified through a series of refinements. The specification includes safety properties as set of invariants, and liveness properties that characterize when the system reaches stable states. We establish these properties by proof of invariants, event refinement and deadlock freedom. The consequence of this incremental approach helps to achieve a high degree of automatic proof. Our approach can be useful for formalizing and developing other kinds of reactive routing protocols (i.e. AODV etc.).</abstract><subject lang="en"><genre>Keywords</genre><topic>Abstract model</topic><topic>Event-B</topic><topic>Event-driven approach</topic><topic>Proof-based development</topic><topic>Refinement</topic><topic>Ad hoc Network</topic></subject><relatedItem type="host"><titleInfo><title>Stabilization, Safety, and Security of Distributed Systems</title><subTitle>13th International Symposium, SSS 2011, Grenoble, France, October 10-12, 2011. Proceedings</subTitle></titleInfo><name type="personal"><namePart type="given">Xavier</namePart><namePart type="family">Défago</namePart><affiliation>School of Information Science, Japan Advanced Institute of Science and Technology (JAIST), Ishikawa, Japan</affiliation><affiliation>E-mail: defago@jaist.ac.jp</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Franck</namePart><namePart type="family">Petit</namePart><affiliation>LIP6/INRIA/UPMC Sorbonne Universities, Paris, France</affiliation><affiliation>E-mail: franck.petit@lip6.fr</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Vincent</namePart><namePart type="family">Villain</namePart><affiliation>University of Picardie Jules Verne, Picardie, France</affiliation><affiliation>E-mail: vincent.villain@u-picardie.fr</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><genre type="book-series" authority="ISTEX" authorityURI="https://publication-type.data.istex.fr" valueURI="https://publication-type.data.istex.fr/ark:/67375/JMC-0G6R5W5T-Z">book-series</genre><originInfo><publisher>Springer</publisher><copyrightDate encoding="w3cdtf">2011</copyrightDate><issuance>monographic</issuance></originInfo><subject><genre>Book-Subject-Collection</genre><topic authority="SpringerSubjectCodes" authorityURI="SUCO11645">Computer Science</topic></subject><subject><genre>Book-Subject-Group</genre><topic authority="SpringerSubjectCodes" authorityURI="I">Computer Science</topic><topic authority="SpringerSubjectCodes" authorityURI="I13022">Computer Communication Networks</topic><topic authority="SpringerSubjectCodes" authorityURI="I13030">Special Purpose and Application-Based Systems</topic><topic authority="SpringerSubjectCodes" authorityURI="I16013">Computation by Abstract Devices</topic><topic authority="SpringerSubjectCodes" authorityURI="I16021">Algorithm Analysis and Problem Complexity</topic><topic authority="SpringerSubjectCodes" authorityURI="I14050">Systems and Data Security</topic><topic authority="SpringerSubjectCodes" authorityURI="I24067">Management of Computing and Information Systems</topic></subject><identifier type="DOI">10.1007/978-3-642-24550-3</identifier><identifier type="ISBN">978-3-642-24549-7</identifier><identifier type="eISBN">978-3-642-24550-3</identifier><identifier type="ISSN">0302-9743</identifier><identifier type="eISSN">1611-3349</identifier><identifier type="BookTitleID">273633</identifier><identifier type="BookID">978-3-642-24550-3</identifier><identifier type="BookChapterCount">41</identifier><identifier type="BookVolumeNumber">6976</identifier><identifier type="BookSequenceNumber">6976</identifier><part><date>2011</date><detail type="volume"><number>6976</number><caption>vol.</caption></detail><extent unit="pages"><start>401</start><end>415</end></extent></part><recordInfo><recordOrigin>Springer-Verlag GmbH Berlin Heidelberg, 2011</recordOrigin></recordInfo></relatedItem><relatedItem type="series"><titleInfo><title>Lecture Notes in Computer Science</title></titleInfo><name type="personal"><namePart type="given">David</namePart><namePart type="family">Hutchison</namePart><affiliation>Lancaster University, Lancaster, UK</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Takeo</namePart><namePart type="family">Kanade</namePart><affiliation>Carnegie Mellon University, Pittsburgh, PA, USA</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Josef</namePart><namePart type="family">Kittler</namePart><affiliation>University of Surrey, Guildford, UK</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Jon</namePart><namePart type="given">M.</namePart><namePart type="family">Kleinberg</namePart><affiliation>Cornell University, Ithaca, NY, USA</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Friedemann</namePart><namePart type="family">Mattern</namePart><affiliation>ETH Zurich, Zurich, Switzerland</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">John</namePart><namePart type="given">C.</namePart><namePart type="family">Mitchell</namePart><affiliation>Stanford University, Stanford, CA, USA</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Moni</namePart><namePart type="family">Naor</namePart><affiliation>Weizmann Institute of Science, Rehovot, Israel</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Oscar</namePart><namePart type="family">Nierstrasz</namePart><affiliation>University of Bern, Bern, Switzerland</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">C.</namePart><namePart type="family">Pandu Rangan</namePart><affiliation>Indian Institute of Technology, Madras, India</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Bernhard</namePart><namePart type="family">Steffen</namePart><affiliation>University of Dortmund, Dortmund, Germany</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Madhu</namePart><namePart type="family">Sudan</namePart><affiliation>Massachusetts Institute of Technology, MA, USA</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Demetri</namePart><namePart type="family">Terzopoulos</namePart><affiliation>University of California, Los Angeles, CA, USA</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Doug</namePart><namePart type="family">Tygar</namePart><affiliation>University of California, Berkeley, CA, USA</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Moshe</namePart><namePart type="given">Y.</namePart><namePart type="family">Vardi</namePart><affiliation>Rice University, Houston, TX, USA</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Gerhard</namePart><namePart type="family">Weikum</namePart><affiliation>Max-Planck Institute of Computer Science, Saarbrücken, Germany</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><originInfo><publisher>Springer</publisher><copyrightDate encoding="w3cdtf">2011</copyrightDate><issuance>serial</issuance></originInfo><identifier type="ISSN">0302-9743</identifier><identifier type="eISSN">1611-3349</identifier><identifier type="SeriesID">558</identifier><recordInfo><recordOrigin>Springer-Verlag GmbH Berlin Heidelberg, 2011</recordOrigin></recordInfo></relatedItem><identifier type="istex">99F497AB2E858B39775632C7B44DBA83DA5E9FE3</identifier><identifier type="ark">ark:/67375/HCB-35RQZ2RP-Z</identifier><identifier type="DOI">10.1007/978-3-642-24550-3_30</identifier><identifier type="ChapterID">30</identifier><identifier type="ChapterID">Chap30</identifier><accessCondition type="use and reproduction" contentType="copyright">Springer-Verlag GmbH Berlin Heidelberg, 2011</accessCondition><recordInfo><recordContentSource authority="ISTEX" authorityURI="https://loaded-corpus.data.istex.fr" valueURI="https://loaded-corpus.data.istex.fr/ark:/67375/XBH-RLRX46XW-4">springer</recordContentSource><recordOrigin>Springer-Verlag Berlin Heidelberg, 2011</recordOrigin></recordInfo></mods><json:item><extension>json</extension><original>false</original><mimetype>application/json</mimetype><uri>https://api.istex.fr/ark:/67375/HCB-35RQZ2RP-Z/record.json</uri></json:item></metadata></istex></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Istex/Corpus
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 002391 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Istex/Corpus/biblio.hfd -nk 002391 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= Istex
|étape= Corpus
|type= RBID
|clé= ISTEX:99F497AB2E858B39775632C7B44DBA83DA5E9FE3
|texte= Analysis of DSR Protocol in Event-B
}}
| This area was generated with Dilib version V0.6.33. |  |