Page 58 - Recherche pour entreprise carnot prepare avenir
P. 58
58
institut carnot lsi
LSI fait sortir la vérification
formelle du laboratoire
Avec le projet SpaceEx, l’institut a mis au point pour l’industrie un
prototype permettant d’effectuer une vérification exhaustive d’un
système cyber physique.
L’utilisation de la simulation numé- processeurs numériques mais n’était jamais
rique est aujourd’hui essentielle sortie des laboratoires en ce qui concerne les
pour prévoir le comportement d’un systèmes cyber-physiques, constitués d’une
produit industriel, ou de plusieurs de composante physique (avion, automobile…) en
ses éléments, dans des situations critiques en interaction avec un logiciel de pilotage. « C’est
termes de sûreté et de performance. L’ensemble une sorte de preuve mathématique qui est équi-
des secteurs, depuis l’automobile et l’aéronau- valente à un nombre infini de tests de simu-
tique en passant par la robotique et les sys- lation » résume Goran Frehse, du laboratoire
tèmes embarqués, est concerné par ces outils Verimag de l’institut grenoblois. Une aubaine
d’aide à la conception et à l’optimisation des pour l’industrie, donc, et c’est bien dans le but
performances. de proposer un tel outil aux industriels que
l’institut s’est lancé dans le projet SpaceEx.
Reste un problème : la vérification du bon fonc- « Le financement par l’abondement Carnot a
tionnement du concept, autrement dit l’absence été le coup de pouce qui nous a permis de fran-
de « bugs ». Il existe actuellement des outils, chir le pas et d’envisager la mise au point d’un
mais ils ont deux défauts majeurs. D’abord, les prototype » raconte Goran Frehse, qui était
tests des systèmes existants sont capables de responsable du projet.
montrer la présence de « bugs » mais jamais
de garantir leur absence. Ensuite, les logiciels Le projet a donné lieu à de nombreuses avan-
utilisés permettent de simuler un système phy- cées sur le plan théorique, à la mise au point
sique et de tester son comportement mais, à d’algorithmes de calculs avancés et, au bout du
chaque fois, pour une configuration bien pré- compte, au prototype envisagé, la plateforme
cise. Autrement dit, pour tester l’intégralité du SpaceEx. Celle-ci est conçue pour faciliter
système, le nombre de manipulations néces- l’implémentation d’algorithmes permettant
saires tend rapidement vers… l’infini, sans pour de vérifier formellement des systèmes, vérifi-
autant apporter de garantie formelle. cation qui s’effectue à partir de modèles impor-
tés dans un format standard de l’industrie. Un
Pour s’affranchir de ces limitations, de nom- partenariat avec Bosch, l’équipementier auto-
breux travaux de recherche académique, dont mobile allemand, a permis d’effectuer des tests
ceux de l’institut Carnot LSI, s’intéressent à sur ses modèles et un objet d’étude, un frein anti
une méthode, la vérification formelle. Elle a bloquant. « Notre outil a déjà été testé par une
le potentiel de garantir la sûreté d’un système, centaine d’organismes de recherche et d’indus-
elle a fait ses preuves dans le domaine des triels » note Goran Frehse.
