Les méthodes formelles permettent d’être plus rigoureux dans le développement des logiciels et d’éliminer les erreurs de spécification, de conception et de codage“, explique Luis-Fernando Meija, responsable méthodes formelles chez Alstom. Car, lorsqu’il s’agit de concevoir le pilote automatique d’un train ou le programme d’une puce de carte bancaire, les exigences de sécurité sont extrêmes. Ces programmes ne supportent aucune défaillance. Le principe des méthodes formelles consiste à traduire les spécifications du système dans un langage mathématique ?” ensembles, propriétés, etc. Les techniques de transformation et de vérification du modèle obtenu reposent sur la preuve mathématique. Elles prouvent que le système est complet vis-à-vis de ses exigences. La preuve garantit l’élimination des erreurs. La méthode formelle aboutit à la production d’un pseudo-code de programmation, qu’il suffit de traduire dans le langage de développement.
La méthode B appliquée au monde ferroviaire
Alstom est à la genèse de l’industrialisation de la méthode B, à l’occasion du développement du Sacem (Système d’aide à la conduite, l’exploitation et la maintenance) pour la ligne A du RER parisien. “La RATP estimait les méthodes de sécurité traditionnelles insuffisantes”, développe Luis-Fernando Meija. Le constructeur s’est donc appuyé sur les travaux de Jean-Raymond Abrial, professeur au Cnam (Conservatoire national des arts et métiers), pour appliquer la méthode B au monde ferroviaire. “Au début des années quatre-vingt-dix, nous avons développé des outils pour industrialiser B. Sans eux, c’était impossible”, précise Luis-Fernando Meija. Face aux quatre-vingt-six mille lignes de code Ada des logiciels “sécuritaires” (liés à la sécurité du voyageur) de Météor (quatorzième ligne du métro parisien, entièrement automatisée), Matra Transport International (MTI) a choisi la même méthode. “Pour un logiciel sécuritaire, le développement n’est pas plus coûteux, car il supprime les tests unitaires”, justifie Jean-Marc Meynadier, responsable du service équipement pilote automatique chez MTI. Chez Trusted Logic, spécialiste du logiciel Java embarqué sur cartes à puce, Coq a été choisi. “L’intérêt est de modéliser la partie complexe du logiciel et de démontrer qu’il résiste à des attaques”, explique Daniel Le Métayer, directeur technique de Trusted Logic. “C’est surtout un élément complémentaire par rapport au cycle de développement classique”, ajoute Claire Loiseaux, responsable évaluations sécuritaires et méthodes formelles de la société.
🔴 Pour ne manquer aucune actualité de 01net, suivez-nous sur Google Actualités et WhatsApp.
