Skip to content. | Skip to navigation

Emergences

Lettre d'information n° 34

Image emergences pour impression
Personal tools
You are here: Home 2015 Lettre d'information n° 34 Vers la vérification statistique des systèmes de systèmes
Document Actions

Vers la vérification statistique des systèmes de systèmes

Nouvelle équipe dirigée par Axel Legay au centre Inria Rennes - Bretagne Atlantique, Estasys débute une action exploratoire pour étendre la portée des techniques de Model Checking en y injectant de l'analyse statistique. Son objectif : parvenir à vérifier le comportement de systèmes hétérogènes à l'exécution. Dans ses cartons : Plasma Lab, un prototype qui peut aider les bureaux d'études à concevoir facilement leur premier vérifieur statistique.

Nouvelle équipe dirigée par Axel Legay au centre Inria Rennes - Bretagne Atlantique, Estasys débute une action exploratoire pour étendre la portée des techniques de Model Checking en y injectant de l'analyse statistique. Son objectif : parvenir à vérifier le comportement de systèmes hétérogènes à l'exécution. Dans ses cartons : Plasma Lab, un prototype qui peut aider les bureaux d'études à concevoir facilement leur premier vérifieur statistique.  

Prenons le cas d'une nouvelle voiture, propose Axel Legay. Le constructeur veut mettre la batterie la moins chère possible, mais avec l'assurance que le véhicule fonctionne correctement. Cet industriel souhaite donc connaître la capacité minimum de la batterie pour  être sûr par exemple qu'un conducteur puisse à la fois écouter l'auto-radio et bénéficier du système automatique d'aide au freinage.  Et c'est là que les problèmes commencent... “Ce sont des propriétés orthogonales. Or, on ne sait pas vérifier ensemble des propriétés qui portent sur différents domaines : énergie, automobile, aéronautique, sécurité... Il faudrait “des modèles comportementaux pour croiser tout cela.”

La nouvelle équipe Estasys s'intéresse précisément à ces croisements et a fortiori dans le cadre de systèmes qui se reconfigurent.  Exemple : un smartphone. Le nombre d'applications, la mémoire disponible... tout cela change ! Les ingénieurs ne peuvent pas tout connaître par avance. Il faut donc pouvoir prendre ces éléments d'évolution en charge à l'exécution. Comment analyse-t-on les comportements d’un système à l'exécution ? Voilà la nouvelle thématique que nous souhaitons explorer.

Plasma Lab

 Une partie de ces travaux se concrétisent à travers le logiciel Plasma Lab. “À partir d'un nombre fini de simulations, ses algorithmes de statistiques peuvent décider si un système est conforme ou non à une propriété, et jusqu'à quel point. Autrement dit, ce n'est pas seulement ‘oui’ ou ‘non’. C'est aussi quantitatif.  La souplesse d'utilisation de ce prototype de recherche en fait aussi un instrument novateur par rapport aux logiciels de vérification classiques. “Quand les ingénieurs utilisent UPPAAL ou Prism par exemple, ils se voient contraints de transcrire leur problème dans le langage spécifique de ces outils.” Ce qui alourdit les coûts  pour les industriels. “L'avantage de Plasma Lab, c'est que si les langages d'entrée ne vous conviennent pas, vous pouvez en utiliser d'autres par le biais de l'API. De la même façon, si la méthode de simulation ne vous convient pas, vous pouvez changer l'algorithme.

Les chercheurs étudient le déploiement de la vérification statistique dans plusieurs contextes industriels.  Nous collaborons avec Alstom à travers le projet Sys2Soft où nous retrouvons nos collègues de l'équipe Hycomes pour un travail sur la modélisation d'un train. Ils modélisent la physique et les contraintes qui y sont liées. De notre côté, nous modélisons les forces : inertie, vitesse, accélération... Ces simulations s'avèrent très complexes.” À la clé : “l'idée d'un outil embarqué qui puisse anticiper le déraillement et dire quand le coefficient de sécurité est dépassé. En théorie, on sait faire. Mais en pratique, il faut que tout aille très vite pour calculer et arrêter. Cela devient un problème de réactivité.

Déambulateur connecté

 Un autre facteur plaide en faveur des méthodes statistiques : la légèreté. “Les outils classiques de model checking sont très gros. Difficile donc de les déployer sur des smartphones, des GPR-GPU, des BeagleBoards, ou sur la technologie embarquée d'une façon générale. À l'inverse, nos outils de statistiques peuvent être taillés sur mesure pour un besoin donné.” À travers le programme européen Dali, les scientifiques collaborent ainsi avec le groupe allemand Siemens qui s'apprête à commercialiser un déambulateur connecté baptisé c-Walker. “Nous avons un scénario où nous aidons une personne âgée à évoluer dans un centre commercial. Il s'agit de minimiser ses déplacements en modélisant ses desiderata, y compris par exemple l'envie de rencontrer certaines personnes ou pas... Dans cette vie de tous les jours et dans un environnement qui se reconfigure sans cesse, la dynamique équationnelle s'avère très compliquée. Mais les techniques de vérification statistique vont nous aider. En retirant tout ce qui n'est pas nécessaire, nous parvenons à faire fonctionner Plasma Lab sur un simple BeagleBoard.

Co-simulation

Plus loin sur la feuille de route, se profile aussi le concept de co-simulation où différents composants sont simulés en parallèle. “Certains sont réalisés en Modelica. D'autres en Simulink. Naturellement, chaque ingénieur veut garder son langage. D'où l'apparition de nouveaux standards comme FMI (2) qui proposent une sémantique commune à tous ces langages. Nous envisageons d'utiliser FMI en langage d'entrée dans Plasma Lab pour aller vers de la co-simulation. Nous pourrions alors nous diriger vers un outil industriel assez robuste pour avoir un vrai impact dans l'ingénierie.

 

------
Notes :

(1) Diverse est l'équipe de recherche en ingénierie de modèles qui succède à Triskell au centre Inria de Rennes.
(2) FMI : Functional Mock-up Interface.

À découvrir : Plasma sur la plateforme A||GO.