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

Manamiary Bruno Andriamiarina 1, 2
1 VERIDIS - Modeling and Verification of Distributed Algorithms and Systems
Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
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.
Type de document :
Thèse
Modélisation et simulation. Université de Lorraine; Loria & Inria Grand Est, 2015. Français
Liste complète des métadonnées

Littérature citée [155 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/tel-01258363
Contributeur : Manamiary Bruno Andriamiarina <>
Soumis le : lundi 18 janvier 2016 - 21:39:33
Dernière modification le : mercredi 4 octobre 2017 - 14:12:24
Document(s) archivé(s) le : mardi 19 avril 2016 - 12:40:43

Identifiants

  • HAL Id : tel-01258363, version 1

Citation

Manamiary Bruno Andriamiarina. Développement d'algorithmes répartis corrects par construction. Modélisation et simulation. Université de Lorraine; Loria & Inria Grand Est, 2015. Français. 〈tel-01258363〉

Partager

Métriques

Consultations de la notice

284

Téléchargements de fichiers

335