Designing Old and New Distributed Algorithms by Replaying an Incremental Proof-Based Development
Identifieur interne : 003967 ( Main/Curation ); précédent : 003966; suivant : 003968Designing Old and New Distributed Algorithms by Replaying an Incremental Proof-Based Development
Auteurs : Dominique Cansell [France] ; Dominique Méry [France]Source :
- Lecture Notes in Computer Science [ 0302-9743 ]
Abstract
Abstract: The paper reports on practical experience with the event B method, when developing case studies, especially distributed algorithms, which are very complex to verify in practice. Using the event B method, we develop a famous distributed algorithm, namely the leader election protocol for an acyclic network, generally known as the IEEE 1394. The algorithm exists and the refinement helps us to model it entirely in an elegant way. The final model is very close to the real algorithm. Only the termination proof is missing, since it is a probabilistic algorithm, as well as the contention resolution, which is solved at a global abstract level. Modelling is clearly fundamental and complex; it should be carried out by persons able to use refinement and to manage abstractions or more precisely abstract models and proofs. Advantages of such an incremental development are multiple what we quote here and that will be explained in detail. We replay the development to improve the proof process and we obtain new distributed algorithms solving the leader election protocol problem. Two strategies are used to build the new algorithms; a first strategy is called the contention resolution; a second strategy is called the contention prevention and is based on a priority among possible nodes of the network. The two resulting algorithms are cheaper than the original IEEE 1394 protocol and neither acknowledgement, nor confirmation is required. We show how the techniques of localisation help in deriving the final distributed algorithm. The paper is an extended version of the complete development of the two new algorithms and it aims to emphasize methodological aspects related to the event B development.
Url:
DOI: 10.1007/978-3-642-11447-2_2
Links toward previous steps (curation, corpus...)
- to stream Istex, to step Corpus: Pour aller vers cette notice dans l'étape Curation :003557
- to stream Istex, to step Curation: Pour aller vers cette notice dans l'étape Curation :003515
- to stream Istex, to step Checkpoint: Pour aller vers cette notice dans l'étape Curation :000A74
- to stream Main, to step Merge: Pour aller vers cette notice dans l'étape Curation :003A45
Links to Exploration step
ISTEX:E0B66E9B0748655BE6E95FE66F7254B98BA09F6ACuration
No country items
Dominique Cansell<affiliation><wicri:noCountry code="subField"> </wicri:noCountry>
<country>France</country>
<placeName><settlement type="city">Nancy</settlement>
<region type="region" nuts="2">Grand Est</region>
<region type="region" nuts="2">Lorraine (région)</region>
</placeName>
<orgName type="team" n="7">Mosel (Loria)</orgName>
<orgName type="lab">Laboratoire lorrain de recherche en informatique et ses applications</orgName>
<orgName type="university">Université de Lorraine</orgName>
<orgName type="EPST">Centre national de la recherche scientifique</orgName>
<orgName type="EPST">Institut national de recherche en informatique et en automatique</orgName>
</affiliation>
Le document en format XML
<record><TEI wicri:istexFullTextTei="biblStruct"><teiHeader><fileDesc><titleStmt><title xml:lang="en">Designing Old and New Distributed Algorithms by Replaying an Incremental Proof-Based Development</title>
<author><name sortKey="Cansell, Dominique" sort="Cansell, Dominique" uniqKey="Cansell D" first="Dominique" last="Cansell">Dominique Cansell</name>
<affiliation><country>France</country>
<placeName><settlement type="city">Nancy</settlement>
<region type="region" nuts="2">Grand Est</region>
<region type="region" nuts="2">Lorraine (région)</region>
</placeName>
<orgName type="team" n="7">Mosel (Loria)</orgName>
<orgName type="lab">Laboratoire lorrain de recherche en informatique et ses applications</orgName>
<orgName type="university">Université de Lorraine</orgName>
<orgName type="EPST">Centre national de la recherche scientifique</orgName>
<orgName type="EPST">Institut national de recherche en informatique et en automatique</orgName>
</affiliation>
</author>
<author><name sortKey="Mery, Dominique" sort="Mery, Dominique" uniqKey="Mery D" first="Dominique" last="Méry">Dominique Méry</name>
<affiliation><country>France</country>
<placeName><settlement type="city">Nancy</settlement>
<region type="region" nuts="2">Grand Est</region>
<region type="region" nuts="2">Lorraine (région)</region>
</placeName>
<orgName type="team" n="7">Mosel (Loria)</orgName>
<orgName type="lab">Laboratoire lorrain de recherche en informatique et ses applications</orgName>
<orgName type="university">Université de Lorraine</orgName>
<orgName type="EPST">Centre national de la recherche scientifique</orgName>
<orgName type="EPST">Institut national de recherche en informatique et en automatique</orgName>
</affiliation>
</author>
</titleStmt>
<publicationStmt><idno type="wicri:source">ISTEX</idno>
<idno type="RBID">ISTEX:E0B66E9B0748655BE6E95FE66F7254B98BA09F6A</idno>
<date when="2009" year="2009">2009</date>
<idno type="doi">10.1007/978-3-642-11447-2_2</idno>
<idno type="url">https://api.istex.fr/ark:/67375/HCB-MKT04LDB-Z/fulltext.pdf</idno>
<idno type="wicri:Area/Istex/Corpus">003557</idno>
<idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">003557</idno>
<idno type="wicri:Area/Istex/Curation">003515</idno>
<idno type="wicri:Area/Istex/Checkpoint">000A74</idno>
<idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Checkpoint">000A74</idno>
<idno type="wicri:doubleKey">0302-9743:2009:Cansell D:designing:old:and</idno>
<idno type="wicri:Area/Main/Merge">003A45</idno>
<idno type="wicri:Area/Main/Curation">003967</idno>
</publicationStmt>
<sourceDesc><biblStruct><analytic><title level="a" type="main" xml:lang="en">Designing Old and New Distributed Algorithms by Replaying an Incremental Proof-Based Development</title>
<author><name sortKey="Cansell, Dominique" sort="Cansell, Dominique" uniqKey="Cansell D" first="Dominique" last="Cansell">Dominique Cansell</name>
<affiliation><wicri:noCountry code="subField"> </wicri:noCountry>
<country>France</country>
<placeName><settlement type="city">Nancy</settlement>
<region type="region" nuts="2">Grand Est</region>
<region type="region" nuts="2">Lorraine (région)</region>
</placeName>
<orgName type="team" n="7">Mosel (Loria)</orgName>
<orgName type="lab">Laboratoire lorrain de recherche en informatique et ses applications</orgName>
<orgName type="university">Université de Lorraine</orgName>
<orgName type="EPST">Centre national de la recherche scientifique</orgName>
<orgName type="EPST">Institut national de recherche en informatique et en automatique</orgName>
</affiliation>
</author>
<author><name sortKey="Mery, Dominique" sort="Mery, Dominique" uniqKey="Mery D" first="Dominique" last="Méry">Dominique Méry</name>
<affiliation wicri:level="4"><orgName type="university">Nancy-Université</orgName>
<country>France</country>
<placeName><settlement type="city">Nancy</settlement>
<region type="region" nuts="2">Grand Est</region>
<region type="region" nuts="2">Lorraine (région)</region>
</placeName>
<placeName><settlement type="city">Nancy</settlement>
<region type="region" nuts="2">Grand Est</region>
<region type="region" nuts="2">Lorraine (région)</region>
</placeName>
<orgName type="team" n="7">Mosel (Loria)</orgName>
<orgName type="lab">Laboratoire lorrain de recherche en informatique et ses applications</orgName>
<orgName type="university">Université de Lorraine</orgName>
<orgName type="EPST">Centre national de la recherche scientifique</orgName>
<orgName type="EPST">Institut national de recherche en informatique et en automatique</orgName>
</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: The paper reports on practical experience with the event B method, when developing case studies, especially distributed algorithms, which are very complex to verify in practice. Using the event B method, we develop a famous distributed algorithm, namely the leader election protocol for an acyclic network, generally known as the IEEE 1394. The algorithm exists and the refinement helps us to model it entirely in an elegant way. The final model is very close to the real algorithm. Only the termination proof is missing, since it is a probabilistic algorithm, as well as the contention resolution, which is solved at a global abstract level. Modelling is clearly fundamental and complex; it should be carried out by persons able to use refinement and to manage abstractions or more precisely abstract models and proofs. Advantages of such an incremental development are multiple what we quote here and that will be explained in detail. We replay the development to improve the proof process and we obtain new distributed algorithms solving the leader election protocol problem. Two strategies are used to build the new algorithms; a first strategy is called the contention resolution; a second strategy is called the contention prevention and is based on a priority among possible nodes of the network. The two resulting algorithms are cheaper than the original IEEE 1394 protocol and neither acknowledgement, nor confirmation is required. We show how the techniques of localisation help in deriving the final distributed algorithm. The paper is an extended version of the complete development of the two new algorithms and it aims to emphasize methodological aspects related to the event B development.</div>
</front>
</TEI>
</record>
Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Main/Curation
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 003967 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Main/Curation/biblio.hfd -nk 003967 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien |wiki= Wicri/Lorraine |area= InforLorV4 |flux= Main |étape= Curation |type= RBID |clé= ISTEX:E0B66E9B0748655BE6E95FE66F7254B98BA09F6A |texte= Designing Old and New Distributed Algorithms by Replaying an Incremental Proof-Based Development }}
This area was generated with Dilib version V0.6.33. |