Modèles algébriques de spécification des applications mobiles

♣ Contenu du memoire

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