Abstractions de modèles en automates temporisés pour la validation temporelle d'architectures embarquées

Karen Godary-Dejean (1) , Isabelle Augé-Blum (2)

1 EXPLORE - Robotique mobile pour l'exploration de l'environnement
2 ARES - Architectures of networks of services

The reliability of critical real time distributed applications must be guaranty by formal techniques of validation, as the model-checking. However these techniques often lead to combinatory explosion problems. This paper proposes efficient abstractions of the timed automata model of TTA (Time-Triggered Architecture) in a temporal validation context.

La fiabilité des applications distribuées temps réel critiques doit être garantie par des techniques formelles de validation, comme le model-checking. Cependant, ces méthodes ont souvent des problèmes d’explosion combinatoire. Cet article propose des abstractions efficaces pour la modélisation et la validation temporelle de l’'architecture TTA (Time-Triggered Architecture) avec des automates temporisés (UPPAAL).

Mots clés: validation temporelle; architecture embarquée; automates temporisés; abstraction de modèle

Domaines: Modélisation et simulation; Théorie et langage formel [cs.FL]; Réseaux et télécommunications [cs.NI]

Karen Godary-Dejean, Isabelle Augé-Blum. Abstractions de modèles en automates temporisés pour la validation temporelle d'architectures embarquées. Journal Européen des Systèmes Automatisés (JESA), 2005, 39 (1/3), pp.63-78. ⟨10.3166/jesa.39.63-78⟩. ⟨lirmm-00812571⟩