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

Pierre-Emmanuel Hladik, Silvano Dal Zilio, Olivier Pasquier, Sébastien Pillement, Bernard Berthomieu
In AFADL 2016 — 15èmes journées Approches Formelles dans l’Assistance au Développement de Logiciels, jun 2016.

 PDF  HAL-01331726

Abstract

#

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.

Citation

#

@InProceedings{DalzilioS:afadl2016mcse,
   author    = {Hladik, Pierre-Emmanuel and {Dal Zilio}, Silvano and Pasquier, Olivier and Pillement, Sébastien and Berthomieu, Bernard},
   title     = {{Outillage pour la modélisation, la vérification et la génération d'applications temporisées et embarquées}},
   booktitle = {AFADL 2016 -- 15èmes journées Approches Formelles dans l'Assistance au Développement de Logiciels},
   month     = jun, 
   year      = 2016
}