Mémoires de Fin d’Etudes
Etablissement
Université Mohamed Boudiaf des Sciences et de la Technologie - Mohamed Boudiaf d’Oran
Affiliation
Département d’Informatique
Auteur
El Habib Daho, Hocine
Directeur de thèse
Slimani, Yahya (Docteur)
Filière
Informatique
Diplôme
Magister
Titre
Spécification et validation de programmes concurrents en utilisant la logique temporelle des actions-TLA
Mots clés
Parallélisme; Spécifications; Occam (langage de programmation); Temps (logique)
Résumé
L’emploi de spécifications formelles, notamment pour des systèmes complexes, est aujourd’hui une nécéssité vitale. L’usage de telles spécifications est dans beaucoup de cas, une exigence d’un cahier de charges. Une déscription rigoureuse d’un système, à l’aide d’un modèle formel, facilite en effet le raisonnement du concepteur, permet d’effectuer des vérifications et des validations, avant sa mise en exploitation ainsi que sa maintenance. C’est dans ce contexte formel, que nous avons mené une étude concernant la spécification de système parallèles, à l’aide d’une logique. temporelle des actions (TLA). Cette logique s’avère être un cadre formel, particulièrement approprié, pour la spécification et la vérification de systèmes parallèles. Ainsi, dans une première étape, nous nous sommes concentrés sur la définition d’une méthode d’analyse, basée sur des concepts de la TLA, permettant de caractériser le comportment temporel d’un système de processus communicants par échange de message. Comme modèle de programmation concurente, nous avons choisi le langage Occam, qui utilise un style de communication basé sur le concept de rendez-vous proposé une formalisation (sous forme d’axiomes) des processus primitifs de communication, à savoir les primitives d’émission et de réception de message. Puis, nous avons défini un axione de communication synchrone, qui modélise le comportement de deux opération complémentaires (Emission, Réception), sur un même canal de communication sur la base de cette définition axiomatique, nous avons proposé une méthode d’analyse, permettant de prédire, des situations indésirables telles que l’interblocage (deadlok) ou l’attente infinie. Dans une deuxième étape, nous nous sommes intéréssés à la combinaison de la TLA avec le formalisme des types Abstraits Algébriques (ADT). L’intégration de ces deux formalismes de spécification, a permis de définir un modèle structuré de spécification à deux niveaux. Ainsi, nous avons proposé une technique de structuration hiéarchique....
Date de soutenance
2000
Cote
TH1.4250
Pagination
165 p.
Format
30 cm.
Statut
Traitée