Spécification Formelle Des Systèmes Mobiles Temps Réel.

Résumé: Notre sujet d’étude est la programmation de systèmes répartis, temps réel. De tels systèmes comportent de nombreux ordinateurs interconnectés par un réseau. L’étude de ce type de système fait appel a des méthodes formelles permettant de répondre aux exigences au quelles sont soumises ces applications. Dans la littérature, il a été proposé un grand nombre de techniques dotées d’un support mathématique pour raisonner sur la conformité des systèmes informatiques. La notion importante dans ces systèmes, est le temps, c’est à dire des systèmes dotés d’un comportement qui est contraint par le temps. Un système temps-réel doit interagir correctement avec son environnement non seulement au regard des informations échangées, mais également au regard des instants au quels ces interactions se réalisent. Dans ce contexte, les sémantiques de vrai parallélisme, comme la sémantique de maximalité, conviennent à être employées lorsqu’on s’abstrait de l’hypothèse de l’atomicité temporelle et structurelle des actions. Le modèle D-LOTOS1, extension temporelle a l’algèbre de processus LOTOS2, intégrant à la fois contraintes temporelles et durées des actions. L’étude exposée dans ce document s’inscrit dans le cadre de la conception de systèmes temps-réel et mobiles, en s’appuyant sur les modèles mobiles, et les méthodes formelles, temps réel. Le modèle proposé (MD-LOTOS)3, représente un langage de programmation directement utilisable il est implémentable de manière répartie, il s’inspire largement de deux modèles (Join-calcul, D-LOTOS).

Publié dans la revue: