SpaceEx : technologie clé pour l’évaluation de la sûreté des systèmes critiques

La vérification des systèmes hybrides : enjeu essentiel de sûreté

 

Les systèmes hybrides sont un modèle mathématique particulièrement utilisé pour vérifier des phénomènes physiques, technologiques, biologiques ou économiques. Leur utilisation dans les secteurs de l'automobile, de l'aéronautique, de la robotique, des systèmes embarqués, etc. est essentiel pour prévoir le comportement d'un produit industriel, ou de plusieurs de ses éléments, dans des situations critiques en terme de sûreté et de performance – par exemple, le vol d'un hélicoptère dans conditions climatiques exceptionnelles. Les systèmes hybrides permettent d'aider à la conception d'une installation, à l'optimisation de ses performances, à la validation des modèles élaborés, à la formation des opérateurs, etc. En d'autres termes, la prédiction du comportement d'un système permet d'anticiper ses échecs et d’améliorer ses performances avant son implémentation définitive sur le marché.


La vérification de ces systèmes hybrides est donc un enjeu considérable et de nombreuses approches sont actuellement étudiées pour dépasser la complexité et la limitation de ces analyses le plus généralement basées sur la simulation numérique. De plus, et comme l'avait énoncé l'informaticien Edsger Dijkstra, les tests des systèmes existants permettent de montrer la présence de bugs mais jamais de garantir leur absence. Les tests traditionnels et les méthodes de validation actuelles ne sont donc pas assez exhaustifs pour améliorer les garanties de sûreté. C'est pourquoi les travaux de recherche dans la thématique sont essentiels pour développer et évaluer de nouvelles approches.

 

La technologie pionnière de SpaceEx

 

Le projet SpaceEx mené par Goran Frehse, maître de conférence dans l'équipe Systèmes Hybrides d'Oded Maler, directeur de recherche CNRS à Verimag (UJF/CNRS/Grenoble INP), est une des initiatives les plus abouties dans le domaine aujourd'hui. Reconnu dans le monde académique, il a par ailleurs bénéficié du soutien de l'institut Carnot LSI dans le cadre de ses projets de ressourcement scientifique 2013.

 


Vues de la plateforme SpaceEx

 

A l'heure actuelle, les logiciels standards utilisés dans l’industrie, comme MatLab/Simulink, permettent de simuler un système physique et de tester son comportement en exécutant un grand nombre de calculs pour toutes les situations envisagées. Mais ces logiciels présentent des faiblesses car le nombre de manipulations nécessaires tend rapidement vers l’infini, sans pour autant apporter de garantie formelle.

 

A l'opposé de la simulation, la vérification formelle peut garantir la sûreté d'un modèle. Cette sorte de preuve mathématique est équivalente à un nombre infini de tests de simulation. La plateforme SpaceEx est conçue pour faciliter l'implémentation d’algorithmes permettant de vérifier formellement des systèmes à partir de modèles importés dans un format standard d'industrie. Elle se positionne donc comme un enrichissement des logiciels de modélisation système existants et largement utilisés par la communauté scientifique et ingénieur. Un véritable plus aux yeux d'industriels soucieux d'anticiper l'ensemble des comportements de leurs produits pour en identifier les défaillances sans modifier en profondeur l'environnement de travail de leurs opérateurs.

 


SpaceEx peut calculer une enveloppe (zone bleue) englobant l'ensemble des comportements possibles (exemples matérialisés en noir)

 

Un potentiel industriel avéré

 

Ce logiciel de pointe dans la vérification des systèmes hybrides pourrait, à terme, considérablement enrichir la boîte à outils d'ingénieurs et scientifiques dans différents domaines. Les entreprises Bosch et Esterel Technologies l'ont bien compris et se sont associées au projet dans le cadre du programme Horizon 2020. Le volet scientifique du projet SpaceEx bénéficie ainsi d'un financement sur 4 ans au cours duquel la plateforme sera testée sur des études de cas fournies par des industriels des secteurs aéronautique, automobile et robotique. En parallèle, l'équipe de Goran Frehse projette également d'améliorer la gamme des modèles d'entrée de la plateforme, en s'intéressant cette fois-ci aux modèles en langage Modelica, un standard industriel utilisé entre autres par Dassault Systèmes. L'équipe, avec le soutien de YeastLab, la plateforme de maturation technologique de l'iC LSI, devrait également se consacrer à l'aspect IHM du logiciel tant sur l'interface utilisateur que sur l'architecture globale du logiciel.