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

Pierre-Emmanuel Hladik (1) , Silvano Dal Zilio (1) , Olivier Pasquier (2) , Sébastien Pillement (2) , Bernard Berthomieu (1)

1 LAAS-VERTICS - Équipe Verification de Systèmes Temporisés Critiques
2 IETR - Institut d'Électronique et des Technologies du numéRique

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.

Domaines: Systèmes embarqués

Pierre-Emmanuel Hladik, Silvano Dal Zilio, Olivier Pasquier, Sébastien Pillement, Bernard Berthomieu. Outillage pour la modélisation, la vérification et la génération d'applications temporisées et embarquées. 15èmes journées Approches Formelles dans l'Assistance au Développement de Logiciels (AFADL), Jun 2016, Besançon, France. ⟨hal-01331726⟩