Projet ANR-10-BLAN-0317 – ImpRo : Implantabilité et Robustesse des Systèmes Temporisés
Programme : Sciences de l'information, de la matière et de l'ingénierie : Matériels et logiciels pour les systèmes, les calculateurs, les communications (Blanc SIMI 3) 2010
Année de financement : 2010
Coordinateur du projet : Monsieur Didier LIME (ECOLE CENTRALE DE NANTES)
Partenaires : Laboratoire Spécification et Vérification; Institut de Recherche en Communications et Cybernétique de Nantes; Institut de Recherche en Informatique et Systèmes Aléatoires; Laboratoire d'Informatique de Paris 6
Montant : 359999.0 euros
Date de début : 2011
Durée : 36 mois
Résumé : L'objectif de cette proposition 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. Ces
modèles peuvent être construits automatiquement à partir de formalismes de plus
haut niveau tels que UML ou AADL, mais ce processus est délibérément hors du
cadre de notre étude.  Avec ces modèles formels incluant la 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.
Il y a donc un vrai fossé entre les sémantiques usuelles des modèles et celles
des implantations, et une question naturelle est donc de savoir lesquelles,
parmi les propriétés vérifiées formellement sur le modèle, sont toujours
vérifiées dans l'implantation. C'est ce que nous appellerons le problème de la
"robustesse", problème qui sera l'objet de notre étude.
La réponse à cette question dépend bien entendu à la fois de la sémantique du
modèle et de celle de l'implantation : cette dernière varie ainsi grandement
entre, par exemple,  une implantation matérielle sur des circuits
programmables et une implantation logicielle sur un système d'exploitation
temps réel. Ce projet étudie notamment ces deux cas, mais aussi celui
d'implantations réparties.
Pour chacun de ces cas, nous étudierons le problème de la robustesse évoqué
ci-dessus mais également, en lien avec la théorie du contrôle, les moyens de
synthétiser automatiquement des modèles corrects et implantables. Et s'il
n'est pas possible d'obtenir un modèle implantable, nous regarderons comment
la théorie du diagnostic peut être utilisée et étendue pour permettre
l'exécution sûre de l'implantation d'un modèle que l'on sait non robuste, en
lançant des alertes ou en prenant des mesures particulières quand un
comportement non sûr est détecté. En réponse à la demande grandissante de
méthodes de conception basées sur des composants, nous étudierons aussi comment
la robustesse peut être intégrée dans les méthodes de raisonnement
compositionnel classiques, dans le sens où l'on essaiera de relier la
robustesse du système global à celle de ses composants.
Du côté du formalisme de conception, nous étudierons également comment des
sémantiques alternatives à la sémantique classique séquentielle en temps dense
des automates temporisés par exemple, peuvent permettre de concevoir des
modèles plus facilement implémentables. À cet effet, nous considérerons bien
sûr le temps discret qui semble plus proche des sémantiques de nos cibles
d'implantation. Nous regarderons également en détail comment les sémantiques
concurrentes (dépliages) peuvent permettre d'analyser plus efficacement les
problèmes particulier de la robustesse des systèmes  répartis.
Enfin, nous chercherons à valider les approches proposées avec l'exemple
du standard AUTOSAR. En nous appuyant sur les résultats obtenus dans les
premières tâches du projet, nous développerons la génération automatique de code
depuis nos modèles de conception prouvés implantables. Ce travail sera appliqué
au cas restreint d'implantations sur une cible monoprocesseur exécutant un
système d'exploitation temps réel conforme à AUTOSAR OS.