| 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 |