Modélisation, vérification et test de systèmes informatisés

1 Thème scientifique

De plus en plus de systèmes produits par l’industrie contiennent des dispositifs logiciels complexes assurant des fonctions de contrôle-commande ou de communication dans des environnements plus ou moins prévisibles. Le bon fonctionnement de ces logiciels souvent critiques doit être absolument garanti :

• par des spécifications formelles précises et validées

• par des conceptions architecturales vérifiées

• par un développement méthodique et contrôlé

• par des tests aussi exhaustifs que possible

1.1 Les enjeux

Longtemps confinées au monde académique, les recherches dans ce domaine ont fait preuve de leur pertinence dans le monde industriel. Elles sont sur le point d’être utilisées massivement dans plusieurs domaines industriels (transports terrestres, aéronautique, énergie). Les chercheurs doivent donc être en mesure, dans un délai très court, de proposer aux industriels des techniques et des méthodes adaptées à leurs besoins.

1.2 Les verrous

Pour pouvoir répondre de façon satisfaisante à cette demande naissante, les efforts doivent porter sur trois points essentiels :

• l’intégration des diverses approches

Les chercheurs ont proposé et étudié plusieurs modèles de systèmes et plusieurs techniques de vérification. Aucun ne peut à lui seul prétendre couvrir tous les aspects d’une application réelle.

L’intégration de ces modèles et de ces techniques, qui est beaucoup plus que leur juxtaposition, demande encore beaucoup de recherches.

• la réflexion méthodologique

Pour être utile, l’offre de techniques issues de la recherche doit être accompagnée de leur ”mode d’emploi”. Cette réflexion méthodologique s’appuie sur des expériences nombreuses conduites en collaboration avec des partenaires industriels.

• le développement d’outils

Il est clair que ces techniques sont inséparables des outils qui les implémentent. Si dans une première phase les outils peuvent se présenter à l’état de maquette pour valider des algorithmes ou des structures de données spécifiques, il est indispensable qu’ils puissent être portés au moins à l’état de prototypes. Ceci dépasse bien entendu le domaine de la recherche pure et rentre en partie dans le cadre du transfert de technologie qu’il faut absolument et rapidement développer dans ce domaine.

2 La position du LaBRI

Pendant longtemps, le LaBRI a été l’un des rares laboratoires dans le monde qui s’est intéressé à ces problèmes (MEC a été l’un des trois premiers ”modelcheckers” jamais écrits). C’est aussi un des rares laboratoires oùla sûreté de fonctionnement fait l’objet d’études approfondies du point de vue informatique.

L’enrichissement de la problématique initiale (les produits synchronisés de systèmes de transitions) par celles de la sûreté de fonctionnement, de la génération de tests, des réseaux de Petri, fait que le LaBRI tient encore une position de tout premier plan. Il faut cependant noter, que compte-tenu de l’importance scientifique et technologique de ce domaine, et plus généralement de celui des techniques formelles pour le développement du logiciel, de très nombreux laboratoires s’y sont investis massivement, avec parfois des moyens considérables.

3 Prospective

Les activités du LaBRI dans le domaine de l’ingénierie des systèmes critiques doivent encore être considérablement développées pour faire face à l’importance majeune que ce domaine est en train de prendre. Les points sur lesquels il doit se donner des compétences nouvelles sont :

• méthodes de spécifications formelles, (en particulier la méthode B)

• vérification des systèmes à nombre infini d’états

• systèmes temporisés ; systèmes stochastiques

• contrôle de qualité logicielle

• théorie du contrôle des systèmes à évènements discrets.