Giuseppe Lipari : une chaire pour la spécification, le développement et l’analyse des systèmes temps réel

Notre quotidien est de plus en plus animé par des objets intelligents : montres connectées, voitures autonomes smartphones ou encore appareils de santé. Derrière chacun de ces objets se cache un système embarqué, une sorte de mini-cerveau à la fois matériel et logiciel qui assure leur bon fonctionnement. En particulier, certains de ces dispositifs doivent réagir rapidement à des événements survenant dans leur environnement. Leur temps de réponse est alors crucial. C’est notamment le cas de l’airbag d'une voiture qui se déclenche grâce à un système embarqué qui réagit en une fraction de seconde et pour lequel un dysfonctionnement peut avoir des conséquences dramatiques. Comment s'assure-t-on alors que ces systèmes embarqués dits temps réel fonctionnent de manière fiable ? 

C’est là qu’interviennent les recherches de Giuseppe Lipari, professeur à l’Université de Lille et directeur de l’équipe-projet commune SyCoMoRES (CNRS/Inria/Université de Lille) au CRIStAL. Il développe et analyse d’un point de vue fondamental ces différents systèmes. « Aujourd’hui l’industrie de l’aviation, de l’automobile et le secteur médicale les valident grâce à des essais incomplets. En effet, pour des systèmes embarqués de grandes tailles, il n’est pas possible de tester toutes les éventualités possibles rencontrées par le système. Les vérifications formelles basées sur la logique mathématique rencontrent la même limite, car le nombre de combinaisons à analyser est énorme, et même les ordinateurs les plus puissants n’arrivent pas à analyser toutes les combinaisons possibles des variables du système », explique Giuseppe Lipari. Autrement dit, nombre de ces systèmes embarqués – bien que critiques et omniprésents autour de nous – nécessitent la mise en place de protocole de vérification consolidés et plus adaptés à leur complexité afin d’être mis en service de manière sure.

Dans le cadre de sa nomination à l’IUF, en tant que membre senior sur une chaire fondamentale, le professeur en informatique va pouvoir développer une méthode alternative pour renforcer la vérification et la sécurité de ces systèmes. L’enjeu : s’assurer qu’ils répondent bien dans les délais imposés. Pour cela, Giuseppe Lipari propose une approche par composant. « L’idée est de découper notre système en différents modules plus ou moins dépendants les uns des autres, puis de les développer de manière indépendante avant de les assembler à nouveau pour vérifier si le système embarqué complet est correct et respecte les temps de réponse exigés », explique-t-il.

Son approche est combinée à une analyse paramétrique. « Par exemple, pour un système de freinage comme l’ABS, je ne connais pas la vitesse maximale du véhicule et la nature des capteurs présents qui dépendent du fabricant. Je vais donc concevoir, développer et tester mon système de manière symbolique sans savoir exactement la valeur de ces paramètres. La sortie de ma méthodologie est l’ensemble de valeurs des paramètres pour lesquels le module fonctionne correctement. Cela facilitera ensuite la phase d’intégration, car les modules seront adaptables à différents systèmes sans besoin de les vérifier à nouveau à chaque fois », décrit Giuseppe Lipari. Au moment d’assembler les modules, la valeur des paramètres est alors connue et permet de garantir que le système fonctionne. 

À terme, les différents modules, pré-vérifiés de manière symbolique, pourront être rassemblés dans des librairies numériques. Les intégrateurs des systèmes pourront alors piocher et assembler les modules d’intérêt pour leurs systèmes.