AFSEC

Approches Formelles des Systèmes Embarqués Communicants

Archive pour March, 2014

Programme du workshop AFSEC lors des journées GPL

Saturday 8 March 2014

Le Workshop AFSEC se tiendra le vendredi 13 juin (session 11h-12h30) lors des journées nationales du GDR GPL qui se dérouleront du 11 au 13 juin 2014 au Cnam à Paris
Elles seront co-localisées avec CAL, CIEL et AFADL : http://cedric.cnam.fr/cpr/gdr-gpl2014/ .

Programme du Workshop AFSEC :

  • Marc Pouzet (Ecole Normale Supérieure, Paris.)
    Une analyse des boucles de causalite dans les modeleurs de systemes hybrides.
  • Resume: Les modeleurs de systemes hybrides tels que Simulink/Stateflow permettent de decrire des systemes a temps discret et continu. Un des points delicats de leur compilation est le traitement des boucles de causalite. Dans cet expose, nous presenterons une analyse de ces boucles pour un langage combinant des constructions d’un langage synchrone — equations de suites, automates hiérarchiques et composition parallele synchrone — et des equations differentielles ordinaires (ODEs). Nous illustrerons cette analyse a l’aide d’exemples écrits en Zélus (zelus.di.ens.fr). Il s’agit d’un travail en commun avec Albert Benveniste, Timothy Bourke, Benoit Caillaud et Bruno Pagano.

  • Étienne André (LIPN, Paris 13)
    Analyse de robustesse précise pour réseaux de Petri temporels
  • Résumé: Quantifier la robustesse des systèmes temporisés consiste à mesurer l’extension maximale des constantes temporelles du système tel que celui-ci satisfasse toujours sa spécification. Ici, nous introduisons une notion de robustesse précise, considérant une mesure locale de la variabilité de toutes les constantes temporelles. Nous considérons cette étude dans le formalisme des réseaux de Petri temporels à arcs inhibiteurs. Nous utilisons la méthode inverse, définie à l’origine pour les automates temporisés, ce qui nous permet d’exprimer cette mesure de robustesse sous la forme d’une contrainte portant sur les différentes constantes du système. Nous proposons aussi une technique afin de rendre robuste un système qui ne l’était pas. Il s’agit d’un travail en commun avec Giuseppe Pellegrino, Laure Petrucci

  • Julien Tanguy (SeeForSys, IRCCyN)
    Synthèse de pilotes de périphériques pour systèmes temps-réel embarqués
  • Résumé: Le développement logiciel de systèmes embarqués critiques (avec des contraintes de temps-réel, de sûreté) est une tâche complexe et difficile.
    A la base de tous les systèmes embarqués, les pilotes doivent prendre en compte un très grand nombre de cas d’utilisations grâce à une généricité et une configurabilité toujours plus grande.
    Des erreurs de configuration peuvent entrainer des bugs graves, cependant l’analyse de toutes les configurations possibles est une tâche difficile.
    Nous proposons une méthode alternative qui est de synthétiser entièrement les pilotes de périphérique grâce aux méthodes formelles.
    A partir de la modélisation du périphérique et de son environnement d’exécution (application, OS, etc.), il est possible de synthétiser un modèle du pilote répondant par construction à des propriétés temporelles, fonctionnelles et de sécurité.
    Ce modèle du pilote est ensuite transformé en code afin d’être embarqué pour une application donnée.
    En déplaçant la configuration au niveau modèle, on simplifie la vérification du code embarqué, et on bénéficie d’outils puissants de model-checking afin de vérifier les contraintes fonctionnelles et de sûreté de fonctionnement.

Publié dans Actions Afsec, Journées | Pas de commentaire »