Developing correct-by-construction distributed algorithms
Identifieur interne : 000271 ( Main/Exploration ); précédent : 000270; suivant : 000272Developing correct-by-construction distributed algorithms
Auteurs : Manamiary Bruno Andriamiarina [France]Source :
Descripteurs français
- mix :
English descriptors
- mix :
Abstract
The subject of this thesis is the formal development and verification of distributed algorithms. We are interested in this topic, because proving that a distributed algorithm satisfies given specification and properties is a difficult task. We choose to use the Event B method (refinement, safety properties) and the temporal logic TLA (fairness, liveness properties) for modelling the distributed algorithms. There are several existing approaches for formalising distributed algorithms, and we choose to focus on the "correct-by-construction" paradigm, which is characterised by the use of model refinement, proof of properties (safety, liveness) and reuse of formal models/proofs/properties, developments (~ design patterns) for modelling distributed algorithms. Our works introduce a paradigm which allows us to describe an algorithm with a set of services/functionalities, which are then expressed using liveness properties. These properties guide us in developing the formal Event B models of the studied algorithms. Inference rules from TLA allow to decompose the liveness properties, therefore detailing the services and guiding the refinement process. This paradigm, called "service-as-event" is also characterized by (assertions) diagrams, which allow to graphically represent liveness properties (with respect to fairness hypotheses) and detail the mecanisms and functioning of the studied distributed algorithms. The "service-as-event" paradigm allowed us to develop and verify the following algorithms : routing algorithms, such as Anycast RP (Cisco Systems), XY for Networks-on-Chip (NoC), snapshot and self-* algorithms.
Url:
Affiliations:
Links toward previous steps (curation, corpus...)
- to stream Hal, to step Corpus: 001C30
- to stream Hal, to step Curation: 001C30
- to stream Hal, to step Checkpoint: 000247
- to stream Main, to step Merge: 000271
- to stream Main, to step Curation: 000271
Le document en format XML
<record><TEI><teiHeader><fileDesc><titleStmt><title xml:lang="en">Developing correct-by-construction distributed algorithms</title><title xml:lang="fr">Développement d'algorithmes répartis corrects par construction</title><author><name sortKey="Andriamiarina, Manamiary Bruno" sort="Andriamiarina, Manamiary Bruno" uniqKey="Andriamiarina M" first="Manamiary Bruno" last="Andriamiarina">Manamiary Bruno Andriamiarina</name><affiliation wicri:level="1"><hal:affiliation type="researchteam" xml:id="struct-107895" status="VALID"><idno type="RNSR">201020692C</idno><orgName>Modeling and Verification of Distributed Algorithms and Systems</orgName><orgName type="acronym">VERIDIS</orgName><desc><address><country key="FR"></country></address><ref type="url">http://www.inria.fr/equipes/veridis</ref></desc><listRelation><relation active="#struct-129671" type="direct"></relation><relation active="#struct-300009" type="indirect"></relation><relation active="#struct-423084" type="direct"></relation><relation active="#struct-206040" type="indirect"></relation><relation active="#struct-413289" type="indirect"></relation><relation name="UMR7503" active="#struct-441569" type="indirect"></relation></listRelation><tutelles><tutelle active="#struct-129671" type="direct"><org type="laboratory" xml:id="struct-129671" status="VALID"><idno type="RNSR">198618246Y</idno><orgName>INRIA Nancy - Grand Est</orgName><desc><address><addrLine>615 rue du Jardin Botanique 54600 Villers-lès-Nancy</addrLine><country key="FR"></country></address><ref type="url">http://www.inria.fr/nancy</ref></desc><listRelation><relation active="#struct-300009" type="direct"></relation></listRelation></org></tutelle><tutelle active="#struct-300009" type="indirect"><org type="institution" xml:id="struct-300009" status="VALID"><orgName>Institut National de Recherche en Informatique et en Automatique</orgName><orgName type="acronym">Inria</orgName><desc><address><addrLine>Domaine de VoluceauRocquencourt - BP 10578153 Le Chesnay Cedex</addrLine><country key="FR"></country></address><ref type="url">http://www.inria.fr/en/</ref></desc></org></tutelle><tutelle active="#struct-423084" type="direct"><org type="department" xml:id="struct-423084" status="VALID"><orgName>Department of Formal Methods </orgName><orgName type="acronym">LORIA - FM</orgName><desc><address><country key="FR"></country></address><ref type="url">http://www.loria.fr/la-recherche-en/departements/formal-methods</ref></desc><listRelation><relation active="#struct-206040" type="direct"></relation><relation active="#struct-300009" type="indirect"></relation><relation active="#struct-413289" type="indirect"></relation><relation name="UMR7503" active="#struct-441569" type="indirect"></relation></listRelation></org></tutelle><tutelle active="#struct-206040" type="indirect"><org type="laboratory" xml:id="struct-206040" status="VALID"><idno type="IdRef">067077927</idno><idno type="RNSR">198912571S</idno><idno type="IdUnivLorraine">[UL]RSI--</idno><orgName>Laboratoire Lorrain de Recherche en Informatique et ses Applications</orgName><orgName type="acronym">LORIA</orgName><date type="start">2012-01-01</date><desc><address><addrLine>Campus Scientifique BP 239 54506 Vandoeuvre-lès-Nancy Cedex</addrLine><country key="FR"></country></address><ref type="url">http://www.loria.fr</ref></desc><listRelation><relation active="#struct-300009" type="direct"></relation><relation active="#struct-413289" type="direct"></relation><relation name="UMR7503" active="#struct-441569" type="direct"></relation></listRelation></org></tutelle><tutelle active="#struct-413289" type="indirect"><org type="institution" xml:id="struct-413289" status="VALID"><idno type="IdRef">157040569</idno><idno type="IdUnivLorraine">[UL]100--</idno><orgName>Université de Lorraine</orgName><orgName type="acronym">UL</orgName><date type="start">2012-01-01</date><desc><address><addrLine>34 cours Léopold - CS 25233 - 54052 Nancy cedex</addrLine><country key="FR"></country></address><ref type="url">http://www.univ-lorraine.fr/</ref></desc></org></tutelle><tutelle name="UMR7503" active="#struct-441569" type="indirect"><org type="institution" xml:id="struct-441569" status="VALID"><idno type="ISNI">0000000122597504</idno><idno type="IdRef">02636817X</idno><orgName>Centre National de la Recherche Scientifique</orgName><orgName type="acronym">CNRS</orgName><date type="start">1939-10-19</date><desc><address><country key="FR"></country></address><ref type="url">http://www.cnrs.fr/</ref></desc></org></tutelle></tutelles></hal:affiliation><country>France</country><placeName><settlement type="city">Nancy</settlement><settlement type="city">Metz</settlement><region type="region" nuts="2">Grand Est</region><region type="old region" nuts="2">Lorraine (région)</region></placeName><orgName type="university">Université de Lorraine</orgName></affiliation></author></titleStmt><publicationStmt><idno type="wicri:source">HAL</idno><idno type="RBID">Hal:tel-01258363</idno><idno type="halId">tel-01258363</idno><idno type="halUri">https://hal.inria.fr/tel-01258363</idno><idno type="url">https://hal.inria.fr/tel-01258363</idno><date when="2015-10-20">2015-10-20</date><idno type="wicri:Area/Hal/Corpus">001C30</idno><idno type="wicri:Area/Hal/Curation">001C30</idno><idno type="wicri:Area/Hal/Checkpoint">000247</idno><idno type="wicri:explorRef" wicri:stream="Hal" wicri:step="Checkpoint">000247</idno><idno type="wicri:Area/Main/Merge">000271</idno><idno type="wicri:Area/Main/Curation">000271</idno><idno type="wicri:Area/Main/Exploration">000271</idno></publicationStmt><sourceDesc><biblStruct><analytic><title xml:lang="en">Developing correct-by-construction distributed algorithms</title><title xml:lang="fr">Développement d'algorithmes répartis corrects par construction</title><author><name sortKey="Andriamiarina, Manamiary Bruno" sort="Andriamiarina, Manamiary Bruno" uniqKey="Andriamiarina M" first="Manamiary Bruno" last="Andriamiarina">Manamiary Bruno Andriamiarina</name><affiliation wicri:level="1"><hal:affiliation type="researchteam" xml:id="struct-107895" status="VALID"><idno type="RNSR">201020692C</idno><orgName>Modeling and Verification of Distributed Algorithms and Systems</orgName><orgName type="acronym">VERIDIS</orgName><desc><address><country key="FR"></country></address><ref type="url">http://www.inria.fr/equipes/veridis</ref></desc><listRelation><relation active="#struct-129671" type="direct"></relation><relation active="#struct-300009" type="indirect"></relation><relation active="#struct-423084" type="direct"></relation><relation active="#struct-206040" type="indirect"></relation><relation active="#struct-413289" type="indirect"></relation><relation name="UMR7503" active="#struct-441569" type="indirect"></relation></listRelation><tutelles><tutelle active="#struct-129671" type="direct"><org type="laboratory" xml:id="struct-129671" status="VALID"><idno type="RNSR">198618246Y</idno><orgName>INRIA Nancy - Grand Est</orgName><desc><address><addrLine>615 rue du Jardin Botanique 54600 Villers-lès-Nancy</addrLine><country key="FR"></country></address><ref type="url">http://www.inria.fr/nancy</ref></desc><listRelation><relation active="#struct-300009" type="direct"></relation></listRelation></org></tutelle><tutelle active="#struct-300009" type="indirect"><org type="institution" xml:id="struct-300009" status="VALID"><orgName>Institut National de Recherche en Informatique et en Automatique</orgName><orgName type="acronym">Inria</orgName><desc><address><addrLine>Domaine de VoluceauRocquencourt - BP 10578153 Le Chesnay Cedex</addrLine><country key="FR"></country></address><ref type="url">http://www.inria.fr/en/</ref></desc></org></tutelle><tutelle active="#struct-423084" type="direct"><org type="department" xml:id="struct-423084" status="VALID"><orgName>Department of Formal Methods </orgName><orgName type="acronym">LORIA - FM</orgName><desc><address><country key="FR"></country></address><ref type="url">http://www.loria.fr/la-recherche-en/departements/formal-methods</ref></desc><listRelation><relation active="#struct-206040" type="direct"></relation><relation active="#struct-300009" type="indirect"></relation><relation active="#struct-413289" type="indirect"></relation><relation name="UMR7503" active="#struct-441569" type="indirect"></relation></listRelation></org></tutelle><tutelle active="#struct-206040" type="indirect"><org type="laboratory" xml:id="struct-206040" status="VALID"><idno type="IdRef">067077927</idno><idno type="RNSR">198912571S</idno><idno type="IdUnivLorraine">[UL]RSI--</idno><orgName>Laboratoire Lorrain de Recherche en Informatique et ses Applications</orgName><orgName type="acronym">LORIA</orgName><date type="start">2012-01-01</date><desc><address><addrLine>Campus Scientifique BP 239 54506 Vandoeuvre-lès-Nancy Cedex</addrLine><country key="FR"></country></address><ref type="url">http://www.loria.fr</ref></desc><listRelation><relation active="#struct-300009" type="direct"></relation><relation active="#struct-413289" type="direct"></relation><relation name="UMR7503" active="#struct-441569" type="direct"></relation></listRelation></org></tutelle><tutelle active="#struct-413289" type="indirect"><org type="institution" xml:id="struct-413289" status="VALID"><idno type="IdRef">157040569</idno><idno type="IdUnivLorraine">[UL]100--</idno><orgName>Université de Lorraine</orgName><orgName type="acronym">UL</orgName><date type="start">2012-01-01</date><desc><address><addrLine>34 cours Léopold - CS 25233 - 54052 Nancy cedex</addrLine><country key="FR"></country></address><ref type="url">http://www.univ-lorraine.fr/</ref></desc></org></tutelle><tutelle name="UMR7503" active="#struct-441569" type="indirect"><org type="institution" xml:id="struct-441569" status="VALID"><idno type="ISNI">0000000122597504</idno><idno type="IdRef">02636817X</idno><orgName>Centre National de la Recherche Scientifique</orgName><orgName type="acronym">CNRS</orgName><date type="start">1939-10-19</date><desc><address><country key="FR"></country></address><ref type="url">http://www.cnrs.fr/</ref></desc></org></tutelle></tutelles></hal:affiliation><country>France</country><placeName><settlement type="city">Nancy</settlement><settlement type="city">Metz</settlement><region type="region" nuts="2">Grand Est</region><region type="old region" nuts="2">Lorraine (région)</region></placeName><orgName type="university">Université de Lorraine</orgName></affiliation></author></analytic></biblStruct></sourceDesc></fileDesc><profileDesc><textClass><keywords scheme="mix" xml:lang="en"><term>Algorithms</term><term>Correct-by-construction paradigm</term><term>Distributed</term><term>Mobile</term><term>Modelling</term><term>Refinement</term><term>Systems</term></keywords><keywords scheme="mix" xml:lang="fr"><term>Algorithmes</term><term>Correction-par-construction</term><term>Dynamiques</term><term>Modélisation</term><term>Raffinement</term><term>Répartis</term><term>Systèmes</term></keywords></textClass></profileDesc></teiHeader><front><div type="abstract" xml:lang="en">The subject of this thesis is the formal development and verification of distributed algorithms. We are interested in this topic, because proving that a distributed algorithm satisfies given specification and properties is a difficult task. We choose to use the Event B method (refinement, safety properties) and the temporal logic TLA (fairness, liveness properties) for modelling the distributed algorithms. There are several existing approaches for formalising distributed algorithms, and we choose to focus on the "correct-by-construction" paradigm, which is characterised by the use of model refinement, proof of properties (safety, liveness) and reuse of formal models/proofs/properties, developments (~ design patterns) for modelling distributed algorithms. Our works introduce a paradigm which allows us to describe an algorithm with a set of services/functionalities, which are then expressed using liveness properties. These properties guide us in developing the formal Event B models of the studied algorithms. Inference rules from TLA allow to decompose the liveness properties, therefore detailing the services and guiding the refinement process. This paradigm, called "service-as-event" is also characterized by (assertions) diagrams, which allow to graphically represent liveness properties (with respect to fairness hypotheses) and detail the mecanisms and functioning of the studied distributed algorithms. The "service-as-event" paradigm allowed us to develop and verify the following algorithms : routing algorithms, such as Anycast RP (Cisco Systems), XY for Networks-on-Chip (NoC), snapshot and self-* algorithms.</div></front></TEI><affiliations><list><country><li>France</li></country><region><li>Grand Est</li><li>Lorraine (région)</li></region><settlement><li>Metz</li><li>Nancy</li></settlement><orgName><li>Université de Lorraine</li></orgName></list><tree><country name="France"><region name="Grand Est"><name sortKey="Andriamiarina, Manamiary Bruno" sort="Andriamiarina, Manamiary Bruno" uniqKey="Andriamiarina M" first="Manamiary Bruno" last="Andriamiarina">Manamiary Bruno Andriamiarina</name></region></country></tree></affiliations></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Main/Exploration
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 000271 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Main/Exploration/biblio.hfd -nk 000271 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= Main
|étape= Exploration
|type= RBID
|clé= Hal:tel-01258363
|texte= Developing correct-by-construction distributed algorithms
}}
| This area was generated with Dilib version V0.6.33. |  |