Mémoires de Fin d’Etudes
Etablissement
Université d’Oran1 - Ahmed Ben Bella
Affiliation
Département d’Informatique
Auteur
EL HABIB DAHO, Hocine
Directeur de thèse
BENHAMAMOUCH Djilali (Docteur)
Filière
Informatique
Diplôme
Doctorat
Titre
Vérification formelle des machines à états abstraits par la logique temporelle des actions
Mots clés
La Logique Temporelle des Actions (TLA); Machines à Etats Abstraits(ASMs); Algèbres Dynamiques; Spécifications Temporelles; Comportements (Séquences d’Etats d’Exécution); Propriétés Temporelles(Propriétés d’Invariance ou de Sureté); Vérification Formelle (Preuve de Correction).
Résumé
Le Travail présenté dans cette thèse porte sur la formalisation et la vérification formelle des modèles ASM en utilisant la logique temporelle des actions(TLA). L’approche de formalisation proposée avec la logique TLA, s’appuit sur la définition d’un ensemble de règles de traduction permettant de formaliser les aspects structurels et comportementales d’un modèle (ou une spécification) ASM, en des expressions logiques de leur sémantique dans le langage de spécification formelle TLA+. Ces règles de traduction sont proposées comme des directives permettant de guider l’interprétation formelle des concepts d’un modèle ASM, en termes des concepts logique du langage de spécification TLA+.En ce sens, l’objectif principal de cette approche de formalisation est de pouvoir traduire des spécifications ASM en des spécifications temporelles TLA+ supportant des techniques de preuves axiomatiques associées à la logique TLA, permettant d’établir la preuve de correction qu’une spécification ASM donnée satisfait les propriétés temporelles initialement exigées par le système modélisé en terme du formalisme ASM.
Date de soutenance
2010
Cote
TH3230
Pagination
147F.
Format
30 cm
Notes
BIBLIOG.143-147F.
Statut
Soutenue