Outillage pour la modélisation, la vérification et la génération d'applications temporisées et embarquées

Overview & Synopsis

Cet article présente un travail en cours pour mettre en place une chaîne d'outils dédiée à la conception, la vérification et l'exécution de systèmes embarqués temps réel. Ce travail se base sur la méthode MCSE et les modèles qu'elle préconise pour la description d'applications. Une traduction du modèle dans le langage formel Fiacre est appliquée pour ensuite vérifier le système à l'aide du model-checker Tina. Afin de faciliter cette analyse et la génération d'un exécutif, la notion de Logical Execution Time est utilisée pour décrire le comportement tem-porel. Nous présentons ces différentes méthodes et outils avant d'exposer l'état d'avancement des différents composants de la chaîne.