Sites Inria

Méthodes formelles

Françoise Breton - 20/06/2013

Fiabilité des logiciels, pas uniquement pour les avions !

Cockpit Airbus A350 © Airbus

Tous les avions actuellement admirés au salon du Bourget sont équipés de systèmes embarqués critiques dont la qualité, la fiabilité et la sureté reposent sur l’utilisation des méthodes formelles. Longtemps confinées à ce domaine et quelques autres comme le spatial, les circuits électroniques ou le nucléaire, les méthodes formelles intéressent un nombre croissant d’entreprises, notamment automobiles et médicales.

Entretien avec Agusti Canals, directeur adjoint Communications & Systems (membre des pôles Aerospace Valley à Toulouse et Minalogic à Grenoble).

Comment les méthodes formelles peuvent-elles intéresser d’autres secteurs d’activité ?

Agusti Canals Agusti Canals, animateur du domaine "Systèmes embarqués, électroniques et logiciels" d'Aerospace Valley

Ces méthodes sont intéressantes en premier lieu pour les applications critiques comme en aéronautique où elles sont aujourd’hui utilisées de manière industrielle. Mais elles le sont aussi, plus largement, pour augmenter la qualité et la fiabilité des applications tout en gagnant un temps précieux dans leur conception et leur développement. De nombreux secteurs d’activité bénéficieraient de ces techniques, comme les automobiles ou les équipements médicaux. Par exemple, lorsque l’on développe aujourd’hui une application pour piloter un pace-maker ou un appareil de radiothérapie, la phase de tests est très longue et coûteuse. Les méthodes formelles qui recouvrent un grand nombre de techniques permettent de vérifier les applications à toutes les étapes de leur développement, de la modélisation à la vérification du code. La phase de test est ainsi très réduite et les codes produits sont de meilleure qualité et plus fiables.

Un forum pour profiter des retours d'expériences industrielles

Le Forum Méthodes Formelles (FMF) est un cycle de conférences qui se déroule au rythme de deux par an environ. Il est organisé par Aerospace Valley en lien avec le pôle Minalogic de Grenoble et le STAE, un réseau de laboratoires de la région toulousaine s’intéressant aux logiciels critiques. Son objectif est de démystifier les méthodes formelles qui sont habituellement considérées comme très compliquées à employer et nécessitant une expertise importante. Nous voulons montrer aux entreprises, grands groupes, mais aussi PME qui ne les utilisent pas encore, qu’il n’est pas si difficile de les mettre en œuvre et que leur adoption est très profitable en terme de productivité et de qualité des logiciels. Le forum présente ainsi les outils disponibles et fait une large place aux retours d’expériences des industriels. La prochaine édition du Forum Méthodes Formelles se déroulera le 28 juin à Toulouse et sera retransmise en direct à Inria Grenoble Rhône-Alpes.

Quel est le thème du forum du 28 juin?

Il s’agit de la seconde édition du forum. La première édition, qui s’est déroulée en novembre 2012, portait sur l’utilisation des méthodes formelles dans les systèmes critiques. Elle a rencontré un succès certain avec 85 participants dont les représentants de 23 grands groupes et de 10 PME. Le 28 juin nous traiterons de l’analyse statique des codes qui consiste à analyser le code produit par le développeur et à vérifier, grâce à un certain nombre de techniques, qu’il est correct. La conférence se déroule en français, même si nous avons l’honneur d’accueillir des orateurs qui viennent des Etats-Unis et d’Allemagne. La transmission simultanée à Grenoble permettra aux adhérents du pôle Minalogic, qui compte des industriels de l’électronique, de l’énergie et du médical directement concernés, de pouvoir participer à l’événement.

Les méthodes formelles amenées à prendre de plus en plus d’importance

Hubert Garavel, chercheur de l’équipe Convecs (Inria), membre du comité de pilotage de FMF .

Hubert Garavel © Inria / Photo A.Eidelman

« Bien que les méthodes formelles soient développées partout dans le monde, la science française est à l’origine de contributions remarquables, en particulier dans la preuve de théorèmes, l’analyse statique, la vérification automatisée (model checking ), le test formel, l’ingénierie des protocoles, la sémantique des langages, les langages synchrones et asynchrones, la compilation certifiée correcte, etc. Les méthodes formelles ont d’abord été adoptées dans des secteurs critiques très réglementés comme l’avionique civile, soumise à des normes de qualité et des autorités de certification indépendantes, et des secteurs non réglementés mais pour lesquels une erreur peut causer des pertes financières colossales, comme dans l’industrie des processeurs et circuits électroniques.

Les industriels de ces secteurs utilisent aujourd’hui les méthodes formelles avec des résultats très satisfaisants. Ils sont donc motivés pour diffuser ces méthodes, en premier lieu vers leurs sous-traitants, mais aussi vers d’autres secteurs susceptibles d’en bénéficier, afin de développer un large écosystème profitable à tous. En parallèle, on voit bien que la sûreté et la sécurité des logiciels font l’objet d’une attention croissante, par exemple avec l’essor des méthodes formelles dans les équipements médicaux aux Etats-Unis. Le forum répond à un besoin émergent des entreprises de Minalogic, en particulier dans les secteurs de l’énergie, des circuits et du matériel médical. Il devient indispensable pour les entreprises française de se former à ces techniques qui, non seulement procurent un gain en temps et en qualité, mais risquent de devenir indispensables pour obtenir des autorisations de mise sur le marché. L’introduction de ces technologies a naturellement un coût, comme toute démarche de qualité, mais le Forum Méthodes Formelles souhaite montrer que les résultats valent l’effort.»

Mots-clés : Analyse statique Aerospace valley Systèmes critiques embarqués Méthodes formelles Minalogic

Haut de page

Suivez Inria tout au long de son 50e anniversaire et au-delà !