[TRIBUNE de Anthony Aiello et Yannick Moy, ADACORE] Longtemps considérées comme peu pratiques ou trop chères, les méthodes formelles ont atteint aujourd’hui un degré de maturité élevé qui leur permet de répondre aux normes de fiabilité les plus élevées pour le développement de logiciels critiques. Comme le détaillent ici Anthony Aiello et Yannick Moy, experts sur l'utilisation des méthodes formelles chez AdaCore, avec un white paper complet sur ce sujet à télécharger....

La taille et la complexité des logiciels dans les systèmes critiques augmentent à un rythme étonnant. Avions, automobiles, appareils médicaux, applications d'infrastructure… Des systèmes qui étaient autrefois uniquement matériels dépendent aujourd'hui de logiciels pour une grande partie de leurs fonctionnalités. Dans ces cas de figure, la vérification du bon fonctionnement des logiciels est un enjeu majeur.

Or, les défauts non découverts dans les logiciels de systèmes critiques peuvent entraîner une défaillance catastrophique, des pertes de vies humaines, de graves dommages liés à une vulnérabilité au hacking. Le niveau d'exigence est très élevé : la probabilité maximale requise de défaillance des éléments les plus critiques de ces systèmes peut être de l'ordre de 10^-7 à moins de 10^-9 défaillances par heure.

Dans ce cadre, les méthodes de test traditionnelles permettent de trouver des bogues... mais ne peuvent prouver qu'il n'y en a plus. Ces approches sont désormais insuffisantes car elles ne peuvent établir que la présence de défauts, et non leur absence. Pour démontrer une probabilité d'erreur inférieure à 10^-9, les essais requis devraient durer des centaines d'années voire des centaines de milliers ou des millions d'années selon les hypothèses. Les tests traditionnels ne peuvent donc pas garantir le niveau de fiabilité requis par les systèmes critiques car il y a tout simplement trop de combinaisons à couvrir.

Les méthodes formelles : une nécessité pour vérifier les logiciels critiques

Aujourd'hui, de grandes organisations remédient à cet écueil en utilisant les méthodes formelles. Longtemps considérées comme peu pratiques ou trop chères pour les logiciels commerciaux, les méthodes formelles ont atteint aujourd’hui leur maturité grâce aux progrès de la puissance de calcul et de nouveaux outils qui automatisent et simplifient leur application.

Contrairement aux tests qui échantillonnent le comportement des logiciels afin de révéler les défauts, les méthodes formelles analysent le comportement du logiciel et établissent la présence ou l'absence de défauts. Les développeurs peuvent ainsi identifier des conditions spécifiques qui doivent ou ne doivent pas se produire et utiliser des méthodes formelles pour prouver que ces conditions se produisent toujours ou jamais.

Toute organisation qui développe des logiciels critiques pour répondre aux normes de fiabilité les plus élevées – c'est-à-dire des logiciels dont la défaillance est inacceptable – tirera ainsi profit de l'utilisation de méthodes formelles de vérification. De nombreuses applications sont concernées, parmi lesquelles les modules critiques pour la sécurité dans les domaines de l'avionique ou des dispositifs médicaux, le contrôle des véhicules automobiles, le contrôle et la surveillance de centrales d'énergie nucléaire, les applications d'infrastructures critiques comme la distribution d'énergie et la commutation des télécommunications, les applications de données sécurisées ainsi que les composants informatiques critiques comme les noyaux de systèmes d'exploitation.

Choisir sa solution de méthodes formelles

Différentes solutions de méthodes formelles existent. Pour faire son choix, AdaCore recommande de prendre en compte plusieurs éléments.

D’abord, il faut trouver le bon équilibre entre l'expressivité et l'automatisation. L'expressivité fait référence à la facilité avec laquelle les développeurs peuvent décrire la fonctionnalité souhaitée dans un langage formel donné. L'automatisation fait référence à la facilité avec laquelle les outils de méthodes formelles peuvent effectuer une analyse sans l'aide d'un humain. En général, une plus grande expressivité se traduit par une automatisation moindre.

Au-delà, il faut réfléchir à la notion de “solidité”, c'est-à-dire la précision et la fiabilité des résultats d'analyse. Si une méthodologie ou un outil prétend vérifier une propriété donnée d'un programme (par exemple qu'un index dans un tableau se trouve dans les limites du tableau), il doit alors détecter toute violation de cette propriété. C'est une caractéristique essentielle des méthodes formelles.

Ensuite, les possibilités d'intégration sont à regarder avec attention. Les méthodes formelles offrent généralement des bibliothèques de tâches de programmation courantes beaucoup plus petites que celles des langages de programmation traditionnels. Les développeurs devront donc être capables d'intégrer la partie du logiciel écrite dans le langage formel avec la partie du logiciel qui dépend des bibliothèques existantes.

L'adoption d'une procédure incrémentale est un autre élément important à prendre en compte. Les méthodes formelles peuvent être déployées progressivement dans le cadre d'efforts de développement de logiciels existants.

La qualité de l'outillage (les environnements et outils logiciels qui permettent de manipuler les méthodes formelles) et le support aux développeurs sont aussi des sujets à examiner de près. Car de nombreuses méthodes formelles ne sont pas développées ou supportées de manière professionnelle, ce qui peut remettre en question leur adoption pour le développement de logiciels industriels.

Enfin, la qualité de la communauté d'utilisateurs actifs est un point important pour les méthodes formelles, autant qu'il peut l'être pour les langages de programmation classiques.

Sur ce sujet AdaCore, éditeur de solutions de développement pour les langages Ada et Spark, et spécialiste des systèmes critiques, propose un livre blanc réalisé par ses experts sur l'utilisation des méthodes formelles pour les systèmes critiques. Le document est téléchargeable gratuitement ici.