Date : 2001
Type : Livre / Book
Type : Thèse / ThesisLangue / Language : anglais / English
Résumé / Abstract : La modélisation des systèmes temps-réel est nécessaire pour l'analyse de leur temporisation. Le modèle doit être une représentation fidèle du comportement dynamique et permettre un raisonnement compositionnel pour le traitement de systèmes complexes. Nous présentons une méthodologie de modélisation basée sur une décomposition en couches du système temps-réel en un ensemble de processus - modélisés sous forme de systèmes temporisés -, une couche de synchronisation qui assure des propriétés fonctionnelles et un ordonnanceur spécifiant des politiques d'ordonnancement telles que RMS, EDF ou le préoràty ceiling protocol. Pour la synchronisation, comme pour l'ordonnanceur, la notion de priorités joue un rôle primordial pour permettre leur composabilité. La méthodologie utilise une opération de composition parallèle "souple" conçue pour préserver des propriétés de progression. Nous définissons la propriété de vivacité structurelle, qui est facile à vérifier et préservée par la composition parallèle et les priorités. Ceci permet un raisonnement compositionnel sur la vivacité et la construction de systèmes temporisés vivants. L'outil de modélisation compositionnelle PROMETHEUS implante ces résultats et supporte la méthodologie proposée. Les processus temps-réel, leur synchronisation et leur ordonnanceur sont spécifiés dans un langage de haut niveau. PROMETHEUS analyse la sûreté, les propriétés temporelles et la cohérence de la spécification. Des traitements complémentaires peuvent être effectués grâce à la connexion de PROMETHEUS à la plate-forme de validation IF. Notre méthodologie est illustrée par des applications réelles faisant intervenir une synchronisation et un ordonnanceur non triviaux