“La preuve est plus puissante que le test “, argue Thierry Servat, directeur général de Clearsy. Cette filiale des sociétés de services Steria et Teamlog, spécialisée dans la production de logiciels prouvés et dans l’expertise de systèmes, a fait de la méthode formelle B son cheval de bataille. Et son discours rallie à sa cause un nombre croissant d’entreprises utilisatrices. Gemplus, la RATP, la SNCF, Peugeot, le CEA (Commissariat à l’énergie atomique)… sont autant de références dont se targue la SSII. Les méthodes formelles seraient-elles en train de gagner leurs lettres de noblesse ? Elles ont, en tout cas, d’ores et déjà prouvé leur efficacité lorsqu’il s’agit de fiabiliser des logiciels embarqués. Elles sont en mesure de garantir la cohérence des spécifications d’un système et la conformité du code produit par rapport à celles-ci. A tel point que Thierry Servat n’hésite pas à affirmer : “La méthode formelle B permet de supprimer les tests unitaires.”
Mariage de la modélisation et de la preuve
Appliquer une méthode formelle revient d’abord à construire un modèle mathématique correspondant aux spécifications informelles d’un système. Pour cela, on utilise un formalisme mathématique de haut niveau. Celui-ci est composé, entre autres, d’ensembles, de propriétés et d’opérateurs. La seule lecture du modèle obtenu permet de retrouver les spécifications. Il est ensuite transformé afin de prendre de plus en plus en compte les contraintes de codage. C’est-à-dire des caractéristiques propres à la réalisation d’un logiciel. Il s’agit du “raffinement “. Le modèle est décomposé en modules successifs, toujours plus précis. A chaque étape de cette décomposition, il est “prouvé” que tout nouveau module n’introduit pas d’incohérence avec le niveau supérieur. Ce processus, mené à son terme, aboutit à la production d’un pseudo-code de programmation, qu’il suffit alors de traduire dans le langage de développement choisi pour le logiciel. Les “preuves” émises lors des phases de spécification, de conception et de codage permettent de se dispenser de procéder aux tests unitaires et de validation. C’est une remise en cause des cycles de développement traditionnels, et notamment du cycle en V. Les méthodes formelles suscitent depuis peu un engouement croissant chez les industriels. Pourtant, elles ne sont pas nouvelles. Issues du milieu universitaire, elles ont plus de vingt ans. Mais il a tout de même fallu attendre la fin des années quatre-vingt pour que certains d’entre eux commencent à s’y intéresser. Alstom, spécialiste des infrastructures pour l’énergie et le transport, fut l’un des premiers, à l’occasion du développement du Sacem (système d’aide à la conduite, l’exploitation et la maintenance) pour la ligne A du RER (réseau express régional) parisien. Ce système permet au conducteur de se passer de la signalisation latérale ?” ramenée en cabine ?” et assure un contrôle continu de la vitesse des trains. S’en remettre à des automatismes lorsqu’il s’agit de transporter des milliers de voyageurs quotidiennement peut susciter de légitimes appréhensions. “La RATP trouvait que les méthodes de sécurité traditionnelles étaient insuffisantes “, confie Luis-Fernando Meija, responsable des méthodes formelles chez Alstom. Le choix s’est porté sur la méthode B pour garantir au transporteur la fiabilité des logiciels “sécuritaires” (liés à la sécurité des passagers) du Sacem. “Il a été motivé par les difficultés inhérentes à la validation du Sacem “, confirme Pierre Desforges, responsable de l’équipe sûreté de fonctionnement de l’unité ingénierie du transport ferroviaire du département des équipements et systèmes du transport de la RATP.
Le recours aux outils est un passage obligé
“Les applications embarquées sont un défi en matière de sécurité, témoigne, pour sa part, Daniel Le Métayer, directeur technique de Trusted Logic, une société spécialisée dans le logiciel sur cartes à puce. Nous utilisons la méthode formelle Coq pour vérifier le code chargé sur les puces.” A mesure que les exigences des utilisateurs vis-à-vis des logiciels croissent, les méthodes formelles deviennent donc peu à peu incontournables.Leur emploi n’est cependant pas simple. “Il n’est pas possible d’utiliser B sans outils “, explique Luis-Fernando Meija. Et, au début des années quatre-vingt-dix, il n’en existait aucun. Candidat à la réalisation du projet Météor (quatorzième ligne du métro parisien, entièrement automatisée), Alstom a constitué une équipe pour l’industrialiser. Mais c’est Matra Transport International (MTI) qui a finalement remporté l’appel d’offres. Néanmoins, durant deux années, un ensemble d’outils a tout de même vu le jour, constituant peu à peu l’Atelier B, aujourd’hui maintenu et commercialisé par Clearsy. Cet atelier de modélisation et de preuve permet d’automatiser certaines tâches durant le cycle de développement. Il assure, entre autres, la vérification syntaxique des modèles, la génération automatique de théorèmes, la preuve de ceux-ci, ou encore la traduction automatique des modèles B en langages C ou Ada. La démarche a été comparable chez Trusted Logic : “Coq est un composant qui complète le cadre offert par notre outil TL-FIT “, explique Daniel Le Métayer. Ce produit intègre, lui aussi, les différents niveaux de raffinement et les vérifications de cohérence exigées par les “critères communs de sécurité”, norme internationale utilisée pour la certification des logiciels (voir, à ce sujet, notre enquête parue dans le numéro 1657 du 30 novembre 2001, page 30).
Un surcoût compensé par une utilisation élargie
Mais, pour attirer de nouveaux adeptes, les seuls arguments techniques ne suffisent pas. Comme partout, au final, c’est le facteur économique qui prime. “Les méthodes formelles entraînent un surcoût en phase de développement, atténué par les gains réalisés en phase de validation. Et ce pour des niveaux de qualité et de sécurité estimés bien meilleurs “, argumente Pierre Desforges. Et pour Jean-Marc Meynadier, responsable du service équipement pilote automatique chez MTI, “la réutilisation permet d’en réduire fortement les coûts “. Ces arguments pourraient bientôt faire sortir les méthodes formelles du seul domaine des logiciels sécuritaires embarqués. “Nous évaluons actuellement la possibilité d’utiliser B pour le développement des logiciels non sécuritaires “, confirme Jean-Marc Meynadier. De son côté, Thierry Servat plaide pour l’extension de son champ d’application aux systèmes dans leur globalité. “L’intérêt, c’est de monter le plus haut possible dans la spécification, affirme-il. Il faut considérer le système comme un tout, et ne pas essayer de séparer le logiciel du matériel. C’est de cette manière que nous pouvons diminuer substantiellement les coûts.” Une démarche qui, si elle devait être mise en ?”uvre, permettrait, de plus, de limiter les tests d’intégration tout en garantissant une plus grande maintenabilité des systèmes. Car les méthodes formelles permettent naturellement d’améliorer la traçabilité des développements. La RATP envisage d’ailleurs d’assurer désormais elle-même la maintenance de ses logiciels. “On maîtrise mieux limpact des modifications apportées aux spécifications “, assure Pierre Desforges.
🔴 Pour ne manquer aucune actualité de 01net, suivez-nous sur Google Actualités et WhatsApp.
