Vérification de systèmes distribués paramétrés – PARDI

L'objectif du projet PARDI est la vérification formelle et assistée de systèmes distribués paramétrés. Une spécification de système paramétré est en fait la spécification d'une large classe de systèmes, paramétrés par le nombre d'entités et les propriétés des interactions, comme le modèle de communication (synchrone/asynchrone, ordre de délivrance des messages, ordre applicatif) ou le modèle de défaillances (défaillance d'arrêt, perte de messages). Pour vérifier de tels systèmes sans instancier explicitement tous les paramètres, de nouveaux résultats théoriques et de nouveaux outils sont nécessaires. Compte tenu de l'indécidabilité par essence du problème étudié, les outils automatiques ne sont pas assez puissants pour vérifier des systèmes paramétrés dans toute leur richesse : ils sont limités dans leur expressivité et ne peuvent pas accepter toute la variété des modèles d'interaction. Pour assister et automatiser la vérification sans instanciation des paramètres, deux approches complémentaires sont prises. Tout d'abord un vérificateur de modèles modulo théories est mis en œuvre pour une vérification totalement automatique. Ensuite, pour dépasser les limites intrinsèques des vérificateurs de modèles, le projet défend une approche collaborative entre assistant de preuve et vérification de modèle. Cette collaboration est à double sens : d'une part, le vérificateur de modèle est utilisé en mode exploration pour générer des invariants élémentaires mis à disposition de l'assistant de preuve ; d'autre part, une propriété nécessaire à l'assistant de preuve peut être déchargée au vérificateur de modèles paramétrés.

Cubicle, un vérificateur de modèle pour les systèmes à base de tableaux, et TLAPS, un assistant de preuve adapté à l'étude des algorithmes distribués, forment le socle du projet. En se basant sur des études de cas venant à la fois des systèmes distribués paramétrés et des systèmes de workflow paramétrés, une analyse théorique est nécessaire pour exhiber les paramètres utiles et pour prouver des résultats génériques. Cette analyse est nécessaire pour identifier les structures de données qui étendront l'expressivité du vérificateur de modèle, et pour injecter les résultats génériques dans l'assistant de preuve et le vérificateur.

La première contribution du projet est la vérification de systèmes distribués paramétrés, pour un nombre arbitraire de sites. La deuxième contribution est une bibliothèque de résultats sur les nombreux modèles de communication et de défaillances, et son intégration dans la chaîne d'outils de vérification. La troisième contribution est la conception et la réalisation du chaîne de vérification basée sur l'interaction entre un assistant de preuve et un vérificateur de modèles. Une quatrième contribution est un nouveau langage dédié à la description de systèmes paramétrés basés sur des workflows, et sa traduction dans les langages d'entrée de l'assistant de preuve et du vérificateur de modèles.