ImPro : Implantabilité et Robustesse des Systèmes temporisés

Contact : Beatrice.Berard (at) nulllip6.fr
Du 01/03/2011 au 31/08/2014

L'objectif du projet ImpRo est d'étudier la relation entre les modèles pour la conception de systèmes embarqués et leur implantation en pratique: de tels modèles abstraient en effet de nombreux détails complexes ou restrictions de l'environnement d'exécution. Nous nous concentrons sur des modèles définis mathématiquement et bien connus tels que les automates temporisés ou les réseaux de Petri temporels. Dans ces modèles qui intègrent une notion de temps, la distance entre le modèle et son implantation peut-être particulièrement importante: en effet, ces formalismes permettent la modélisation de comportements non implantables tels que des tests d'horloge ponctuels, des horloges parfaites, des comportements zénons, etc. Compte tenu de ce fossé entre les sémantiques usuelles des modèles et celles des implantations, une question naturelle est de savoir lesquelles, parmi les propriétés vérifiées formellement sur le modèle, sont toujours garanties dans l'implantation. Ce problème de "robustesse" est au centre du projet ImpRo. Outre une tâche dévolue à une définition unifiée du problème, l'étude porte sur plusieurs axes : quantification de la robustesse dans un contexte temporisé et/ou probabiliste, caractérisation dans le cadre d'applications réparties, liens avec les activités de monitoring et de diagnostic.

Ecole Centrale de Nantes, Ecole Normale Supérieure de Cachan, CNRS
Agence Nationale pour la Recherche

Beatrice BERARD