Abstract FR:

Nous nous intéressons dans cette thèse à la vérification de propriétés temporelles de systèmes répartis décrits dans le cadre des systèmes de transitions, et plus spécialement dans le formalisme UNITY. Nous avons d'abord choisi un modèle opérationnel : des instructions non-déterministes manipulant des entiers relatifs au sein de l'arithmétique de Presburger, ainsi que des booléens et des tableaux. La vérification par preuve utilisera les triplets de Hoare et le calcul des WPs comme cadre logique. Ces tableaux sont utilisés pour représenter des systèmes paramétrés pour le nombre de sites par exemple. Dans notre contexte opérationnel, les propriétés choisies sont assez expressives, mais suffisamment simples pour être soumises à une automatisation. Nous nous sommes penchés en premier lieu sur les problèmes liés à la modélisation de la répartition. Nous prolongeons les travaux de thèse de M. Charpentier qui a défini et étudié en UNITY l'ajout d'une primitive de communication asynchrone entre deux sites. Nous avons pour but de simplifier les problèmes de vérification des algorithmes distribués utilisant cette primitive pour nous ramener aux problèmes mieux maîtrisés des systèmes de transition classiques. En supposant dorénavant évoluer dans ce cadre familier, nous avons alors défini un calcul généralisé des WPs pour nos programmes, puis conçu une méthode prouvée correcte pour automatiser la preuve des formules logiques issues de ce calcul. L'implantation de cette méthode à travers la réalisation d'un environnement de preuve pour le formalisme UNITY nous a permis de valider expérimentalement nos travaux. De plus, l'outil développé permet à l'utilisateur de contrôler le processus de preuve automatique et de comprendre pourquoi la preuve a réussi (ou échoué).