Mémoires de Fin d’Etudes
Etablissement
Université d’Oran1 - Ahmed Ben Bella
Affiliation
Département d’Informatique
Auteur
ELHABIB DAHO, Hocin
Directeur de thèse
SLIMANI Yahia (Professeur)
Filière
Informatique
Diplôme
Magister
Titre
Spécification et vérification des systèmes concunents en utilisent la logique temporelle des actions.
Mots clés
Parallélisme - logique temporelle module - abstrait - propriéte de
Résumé
La logique temporelle des actions (TLA) s’est avérée un cadre formelle particuliérement approprie pour la specification et la vérification des systèmes concurents. C’est dans ce contexte, que nous mémes une étude d’une méthode d’analyse basée sur la TLA, pour valider des programmes utilisants des mécanismes de communication. Les propriétes temporelles à vérifier vis à vis ces systèmes sont de deux types : propriéte de surté à savoir l’interblocage et la propriete de vivacité à s’avoir l’assence de formel.
Statut
Validé