Lamiae
Sommaire: Spécification formelle des systèmes mobiles temps réel
Notations générales
Remerciements
Résumé
1 Introduction
1.1 Context
1.2 Contributions
1.3 Plandudocument
2 Modèles algébriques de spécification des applications mobiles
2.1 Introductionauxalgèbresdeprocessus
2.1.1 CCS:CalculusofCommunicatingSystems
2.1.2 Algèbre de processus à synchronisation multiple : LOTOS
2.2 π-calcul
2.2.1 π-calculmonadique
2.2.2 π-calculpolyadique
2.2.3 Sémantique opérationnelle du π-calcul
2.2.4 Equivalences
2.2.5 Applications
2.3 Join-Calcul
2.3.1 Machinechimiqueabstraite
2.3.2 La machine chimique réflexive(RCHAM)
2.3.3 Equivalences
2.3.4 Lecalculouvert
2.3.5 Localité,migrationetpannes
2.4 CalculdesAmbients
2.4.1 Présentation
2.4.2 Mobilité
2.4.3 Sémantiqueopérationnelle
2.4.4 Exemples
2.4.5 Communication
2.5 Logique de réécriture
2.5.1 Définitionsdebase
2.5.2 Structuresémantiquepourmodèlesdeconcurrence
2.5.3 MAUDE
2.5.4 Systèmetemps-réel
2.5.5 Modèles de temps et théorie de réecriture temps réel
2.5.6 Théorie temps réel intériorisée dans la logique de réecriture
2.6 Conclusionetdiscussion
2.6.1 π-calculetjoin-calcul
2.6.2 Lesambientsetlejoin-calcul
3 Modèles algébriques de spécification des applications temps réel
3.1 ExtensiontemporelledeLOTOS
3.2 Le langage D-LOTOS
3.2.1 Sémantiquedemaximalité
3.2.2 Introduction des durées et des contraintes temporelles
3.2.3 SémantiqueopérationnellestructuréedeD-LOTOS
3.2.4 Relationsdebissimulation
3.3 Limites du langage D-LOTOS
3.4 Conclusion
4 MD-LOTOS (mobil D-LOTOS) : Un modèle de spécification des applications temps réel et mobiles
4.1 PrésentationdeMD-LOTOS
4.1.1 Traitementlocaletglobal
4.1.2 Syntaxe et sémantique opérationnelle de maximalité
4.2 Etudedecas(Gigued’information)
4.3 Outildecompilation
4.3.1 L’outilOcamllex
4.3.2 L’outilOcamlyacc
4.3.3 OutildecompilationpourMD-LOTOS
4.3.4 Etaped’analyse
4.4 Conclusion
5 Conclusion et perspectives
Extrait du mémoire spécification formelle des systèmes mobiles temps réel
Chapitre 1: Introduction
1.1 Context
L’informatique répartie a connue, depuis les dix dernières années, une véritable révolution, avec la génération des réseaux locaux et globaux. Pourtant la programmation distribuée semble n’avoir pas bénéficié de cette révolution, tant le nombre de programmes répartis est encore limité.
Des efforts ont été entrepris, à la fois pour offrir à la programmation répartie des modèles formels, et pour fournir des infrastructures simples d’utilisation. Ainsi les algèbres de processus – on retrouve parmi lesquelles CCS1 [30] et le π-calcul[31] [35]- représentent un cadre naturel pour décrire et analyser les systèmes répartis. Elles fournissent plusieurs descriptions d’un même système à des niveaux d’abstraction différents, et des techniques permettant de montrer leur équivalence. Le π-calcul est une extension de CCS, dans la mesure où les processus peuvent échanger des noms de canaux. Cette possibilité augmente le pouvoir expressif de ce langage, et permet de décrire les systèmes dont la topologie du réseau de communications change dynamiquement. Le prix à payer pour ce gain d’expressivité est la complexité de la vérification et d’analyse de ces systèmes.
De l’autre coté une implémentation distribuée de CCS ou de π-calcul et loin d’être évidente, les deux modèles utilisent la communication par rendez-vous, ce qui donne une synchronisation distribuée, qui n’est pas adéquate à la programmation répartie.
Join-calcul représente un modèle élémentaire de programmation répartie, il hérite la plupart des propriétés formelles de π-calcul. Il utilise la communication asynchrone, ce qui le rend implantable directement. Il offre aussi des primitives pour la migration et les pannes.
Les caractéristiques principales de ces systèmes répartis :
· Mobilité : c’est une notion de base dans un système distribué. Dans le cas de π−calcul cette notion se traduit par l’existence de noms, qui est inséparable du processus de communication fondamentale dans tout système concurrent. L’existence de noms suggère de plus un espace abstrait de processus connectés, dans lequel les noms représentent les connexions, seuls les processus qui partagent des noms sont alors en mesure d’interagir. La structure d’un système change donc d’une manière dynamique, car les liens entre processus sont sans cesse crées et détruits.
…….
Si le lien ne fonctionne pas correctement, veuillez nous contacter (mentionner le lien dans votre message)Mémoire Online: Spécification formelle des systèmes mobiles temps réel (853 KO) (Cours PDF)
