Vérification formelle des systèmes parallèles décrits en UNITY à l'aide d'un outil de démonstration automatique - Université de Lorraine Accéder directement au contenu
Thèse Année : 1996

Vérification formelle des systèmes parallèles décrits en UNITY à l'aide d'un outil de démonstration automatique

Résumé

Non disponible / Not available
Cette thèse est consacrée à l'utilisation des méthodes formelles de spécification et de vérification dans le cadre des techniques déductives basées sur la preuve de théorèmes. En particulier, nous nous intéressons à la spécification et à la vérification mécanique de programmes parallèles décrits en UNITY à l'aide du démonstrateur du LARCH, LP. Nous décrivons la formalisation et la mécanisation de la logique et de la méthodologie d'UNITY à l'aide d'un outil de démonstration automatique du premier ordre et à large spectre tel que LP et à leur mise en oeuvre dans des exemples utiles et conséquents. Nous formalisons dans un premier temps la syntaxe et la sémantique d'UNITY dans l'environnement de LP en choisissant comme outil formel la plus faible pré-condition introduite par Dijkstra. Cette modélisation comprend la représentation syntaxique concrète des objets prédicats, de la notation de programmation et des prédicats temporels de UNITY dans une logique du premier ordre. Nous décrivons la construction et la validation d'une base de faits basée sur l'approche des spécifications LSL. Nous proposons une méthodologie de preuve incrémentale basée sur l'utilisation d'un démonstrateur pour la vérification mécanisée dans le but à la fois d'aider à la mise au point des preuves et à la réutilisation des preuves. Nous illustrons l'approche proposée à l'aide de trois études de cas. La vérification formelle mécanique d'un protocole de communication à travers des canaux défectueux met en évidence la méthodologie utilisée pour montrer des propriétés de sûreté et de vivacité et comment un démonstrateur peut être effectivement utilisé pour détecter des failles dans la spécification. La vérification du problème des lecteurs rédacteurs illustre un aspect important dans l'utilisation des démonstrateurs, à savoir la réutilisation et la mécanisation des preuves. Enfin, la vérification d'un protocole de contrôle d'un ascenseur permet de comparer notre approche à celle utilisée avec le démonstrateur d'ordre supérieur HOL
Fichier principal
Vignette du fichier
SCD_T_1996_0037_CHETALI.pdf (10.35 Mo) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)

Dates et versions

tel-01753552 , version 1 (29-03-2018)

Identifiants

  • HAL Id : tel-01753552 , version 1

Citer

Boutheïna Chetali. Vérification formelle des systèmes parallèles décrits en UNITY à l'aide d'un outil de démonstration automatique. Informatique [cs]. Université Henri Poincaré - Nancy 1, 1996. Français. ⟨NNT : 1996NAN10037⟩. ⟨tel-01753552⟩
41 Consultations
162 Téléchargements

Partager

Gmail Facebook X LinkedIn More