Skip to Main content Skip to Navigation
Theses

Développement d'algorithmes répartis corrects par construction

Manamiary Bruno Andriamiarina 1, 2
1 VERIDIS - Modeling and Verification of Distributed Algorithms and Systems
LORIA - FM - Department of Formal Methods , Inria Nancy - Grand Est, MPII - Max-Planck-Institut für Informatik
2 MOSEL - Proof-oriented development of computer-based systems
LORIA - FM - Department of Formal Methods
Résumé : 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.
Document type :
Theses
Complete list of metadatas

Cited literature [155 references]  Display  Hide  Download

https://hal.inria.fr/tel-01752149
Contributor : Manamiary Bruno Andriamiarina <>
Submitted on : Monday, January 18, 2016 - 9:39:33 PM
Last modification on : Tuesday, February 19, 2019 - 3:40:03 PM
Document(s) archivé(s) le : Tuesday, April 19, 2016 - 12:40:43 PM

Identifiers

  • HAL Id : tel-01752149, version 2

Citation

Manamiary Bruno Andriamiarina. Développement d'algorithmes répartis corrects par construction. Modélisation et simulation. Université de Lorraine, 2015. Français. ⟨NNT : 2015LORR0181⟩. ⟨tel-01752149v2⟩

Share

Metrics

Record views

523

Files downloads

725