ملخص: 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:
لغة: فرنسية
الوصف المادي: 165 p. ill. ;30 cm
الشهادة: Magister
مؤسسة مناقشة الرسالة: Oran, Université des Sciences et de laTechnologie Mohamed Boudiaf. Faculté des Sciences
تخصص: Informatique
الفهرس العشري 621 .الفيزياء التطبيقية (الهندسة الكهربائية ، الهندسة المدنية ، الهندسة الميكانيكية ، الهندسة التطبيقية ، المبادئ الفيزيائية في الهندسة)
الموضوع الإعلام الآلي

الكلمات الدالة:
Parallélisme (Informatique)
Logique temporelle
Vérification de modèles (informatique)
occam (langage de programmation)

ملاحظة: Bibliogr.pp.159-165