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