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

Oran:
Langue: Français
Collation: 165 p. ill. ;30 cm
Diplôme: Magister
Etablissement de soutenance: Oran, Université des Sciences et de laTechnologie Mohamed Boudiaf. Faculté des Sciences
Spécialité: Informatique
Index décimal 621 .Physique appliquée (électrotechnique, génie civil, génie mécanique, ingénierie appliquée, principes physiques en ingénierie)
Thème Informatique

Mots clés:
Parallélisme (Informatique)
Logique temporelle
Vérification de modèles (informatique)
occam (langage de programmation)

Note: Bibliogr.pp.159-165