Developing correct-by-construction distributed algorithms
Identifieur interne : 001C30 ( Hal/Curation ); précédent : 001C29; suivant : 001C31Developing 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:
Links toward previous steps (curation, corpus...)
- to stream Hal, to step Corpus: Pour aller vers cette notice dans l'étape Curation :001C30
Links to Exploration step
Hal:tel-01258363Le 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></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><hal api="V3"><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 role="aut"><persName><forename type="first">Manamiary Bruno</forename><surname>Andriamiarina</surname></persName><email>Manamiary.Andriamiarina@loria.fr</email><idno type="halauthor">623418</idno><affiliation ref="#struct-107895"></affiliation><affiliation ref="#struct-206041"></affiliation></author><editor role="depositor"><persName><forename>Manamiary Bruno</forename><surname>Andriamiarina</surname></persName><email>Manamiary.Andriamiarina@loria.fr</email></editor></titleStmt><editionStmt><edition n="v1" type="current"><date type="whenSubmitted">2016-01-18 21:39:33</date><date type="whenModified">2016-01-21 01:11:35</date><date type="whenReleased">2016-01-19 12:05:55</date><date type="whenProduced">2015-10-20</date><date type="whenEndEmbargoed">2016-01-18</date><ref type="file" target="https://hal.inria.fr/tel-01258363/document"><date notBefore="2016-01-18"></date></ref><ref type="file" n="1" target="https://hal.inria.fr/tel-01258363/file/these-Andriamiarina-Manamiary-Bruno.pdf"><date notBefore="2016-01-18"></date></ref></edition><respStmt><resp>contributor</resp><name key="163475"><persName><forename>Manamiary Bruno</forename><surname>Andriamiarina</surname></persName><email>Manamiary.Andriamiarina@loria.fr</email></name></respStmt></editionStmt><publicationStmt><distributor>CCSD</distributor><idno type="halId">tel-01258363</idno><idno type="halUri">https://hal.inria.fr/tel-01258363</idno><idno type="halBibtex">andriamiarina:tel-01258363</idno><idno type="halRefHtml">Modélisation et simulation. Université de Lorraine; Loria & Inria Grand Est, 2015. Français</idno><idno type="halRef">Modélisation et simulation. Université de Lorraine; Loria & Inria Grand Est, 2015. Français</idno></publicationStmt><seriesStmt><idno type="stamp" n="CNRS">CNRS - Centre national de la recherche scientifique</idno><idno type="stamp" n="INRIA-LORRAINE">INRIA Nancy - Grand Est</idno><idno type="stamp" n="INRIA-NANCY-GRAND-EST">INRIA Nancy - Grand Est</idno><idno type="stamp" n="LORIA-FM" p="LORIA">Méthodes formelles</idno><idno type="stamp" n="LORIA2">Publications du LORIA</idno><idno type="stamp" n="INRIA">INRIA - Institut National de Recherche en Informatique et en Automatique</idno><idno type="stamp" n="INRIA_TEST">INRIA - Institut National de Recherche en Informatique et en Automatique</idno><idno type="stamp" n="UNIV-LORRAINE">Université de Lorraine</idno><idno type="stamp" n="INRIA2">INRIA 2</idno><idno type="stamp" n="LORIA">LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications</idno></seriesStmt><notesStmt></notesStmt><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 role="aut"><persName><forename type="first">Manamiary Bruno</forename><surname>Andriamiarina</surname></persName><email>Manamiary.Andriamiarina@loria.fr</email><idno type="halAuthorId">623418</idno><affiliation ref="#struct-107895"></affiliation><affiliation ref="#struct-206041"></affiliation></author></analytic><monogr><imprint><date type="dateDefended">2015-10-20</date></imprint><authority type="institution">Université de Lorraine</authority><authority type="institution">Loria & Inria Grand Est</authority><authority type="school">IAEM (Informatique, Automatique, Électronique - Électrotechnique, Mathématiques) Lorraine</authority><authority type="supervisor">Dominique Méry</authority><authority type="jury">Attiogbé Jérémie-Christian</authority><authority type="jury">Quéinnec Philippe</authority><authority type="jury">Chrisment Isabelle</authority><authority type="jury">Méry Dominique</authority><authority type="jury">Merz Stephan</authority><authority type="jury">Mosbah Mohamed</authority><authority type="jury">Poppleton Michael R.</authority></monogr></biblStruct></sourceDesc><profileDesc><langUsage><language ident="fr">French</language></langUsage><textClass><keywords scheme="author"><term xml:lang="en">Modelling</term><term xml:lang="en">Systems</term><term xml:lang="en">Algorithms</term><term xml:lang="en">Distributed</term><term xml:lang="en">Mobile</term><term xml:lang="en">Correct-by-construction paradigm</term><term xml:lang="en">Refinement</term><term xml:lang="fr">Modélisation</term><term xml:lang="fr">Systèmes</term><term xml:lang="fr">Algorithmes</term><term xml:lang="fr">Répartis</term><term xml:lang="fr">Dynamiques</term><term xml:lang="fr">Correction-par-construction</term><term xml:lang="fr">Raffinement</term></keywords><classCode scheme="halDomain" n="info.info-mo">Computer Science [cs]/Modeling and Simulation</classCode><classCode scheme="halTypology" n="THESE">Theses</classCode></textClass><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.</abstract><abstract xml:lang="fr">Nous présentons dans cette thèse intitulée "Développement d'algorithmes répartis corrects par construction" nos travaux sur le développement et la vérification formels d'algorithmes répartis. Nous nous intéressons à ces algorithmes, à cause de la difficulté de leur vérification et validation. Pour analyser ces algorithmes, nous avons choisi d'utiliser Event B pour le raffinement de modèles, la vérification de propriétés de sûreté, et TLA, pour la vérification des propriétés temporelles (vivacité et équité). Nous nous sommes focalisé sur le paradigme de correction-par-construction, basé sur la modélisation par raffinement, la preuve de propriétés, ainsi que la réutilisation de modèles/preuves/propriétés (~ patrons de conception) pour guider le développement formel des algorithmes étudiés. Nous avons mis en place un paradigme de développement lors duquel un algorithme réparti est dans un premier temps caractérisé par les services qu'il fournit, et qui sont ensuite exprimés par des propriétés de vivacité, guidant la construction des modèles Event B de cet algorithme. Les règles d'inférence de TLA nous permettent ensuite de détailler les propriétés de vivacité, et de guider le développement formel par raffinement de l'algorithme. Ce paradigme, appelé "service-as-event", est caractérisé par des diagrammes d'assertions permettant de représenter les propriétés de vivacité (en prenant en compte l'équité) des algorithmes répartis étudiés, de comprendre leurs mécanismes. Ce paradigme nous a permis d'analyser des algorithmes de routage (Anycast RP de Cisco Systems et XY pour les réseaux-sur-puce (NoC)), des algorithmes de snapshot et des algorithmes d'auto-stabilisation.</abstract></profileDesc></hal></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Hal/Curation
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 001C30 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Hal/Curation/biblio.hfd -nk 001C30 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= Hal
|étape= Curation
|type= RBID
|clé= Hal:tel-01258363
|texte= Developing correct-by-construction distributed algorithms
}}
| This area was generated with Dilib version V0.6.33. |  |