Blanc SIMI 3 - 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

Implantabilité et Robustesse des Systèmes Temporisés – ImpRo

ImpRo

Implémentabilité et robustesse des systèmes temporisés

Vers des modèles plus proches de la leur implémentation

Le projet ImpRo, «Implantabilité et Robustesse des Systèmes Temporisés«, <br />s'intéresse à la relation entre les modèles formels pour la conception de <br />systèmes embarqués communicants et leur implantation en pratique : de tels <br />modèles abstraient en effet de nombreux détails complexes ou restrictions de <br />l'environnement d'exécution. En particulier, la prise en compte du temps se <br />fait habituellement de façon idéale, par des horloges infiniment précises, des <br />tests ou des commutations de modes instantanés, etc. <br /> <br />Notre objectif est ainsi d'étudier dans quelle mesure l'implantation en <br />pratique de ces modèles préserve leurs bonnes propriétés.

Dans un premier
temps, nous définirons un cadre mathématique général pour l'expression et la
mesure des propriétés de robustesse d'implantation, puis nous étudierons la
possibilité d'intégrer dans les modèles les contraintes de l'implantation. Nous
nous concentrerons, en particulier, sur la combinaison de plusieurs sources de
perturbation telles que l'allocation de ressources, le caractère distribué des
applications, etc. Nous étudierons aussi les problèmes d'implantabilité au
travers des techniques de contrôle et de diagnostique. Enfin nous appliquerons
les méthodes développées à un cas d'étude basé sur l'architecture AUTOSAR, un
standard de l'industrie automobile.

Le projet n'est pas fini

Le projet n'est pas fini

Au 1/07/2012, une dizaine de publications scientifiques dans des revues et conférences internationales reconnues.

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.

Coordinateur du projet

Monsieur Didier Lime (ECOLE CENTRALE DE NANTES) – Didier.Lime@ec-nantes.fr

L'auteur de ce résumé est le coordinateur du projet, qui est responsable du contenu de ce résumé. L'ANR décline par conséquent toute responsabilité quant à son contenu.

Partenaire

IRCCyN ECOLE CENTRALE DE NANTES
ENS Cachan / IRISA ECOLE NORMALE SUPERIEURE DE CACHAN
UPMC/LIP6 UNIVERSITE PARIS VI [PIERRE ET MARIE CURIE]
LSV CNRS - DELEGATION REGIONALE ILE-DE-FRANCE SECTEUR EST

Aide de l'ANR 359 999 euros
Début et durée du projet scientifique : - 36 Mois

Liens utiles

Explorez notre base de projets financés

 

 

L’ANR met à disposition ses jeux de données sur les projets, cliquez ici pour en savoir plus.

Inscrivez-vous à notre newsletter
pour recevoir nos actualités
S'inscrire à notre newsletter