Bien que les techniques d’analyses formelles de programme (voir les travaux de Hoare et de Dijkstra ) soient assez anciennes, leurs mises en place datent des années 1980. Les méthodes formelles permettent d’analyser le comportement d’une application logicielle décrite dans un langage de programmation. La correction (bon comportement, arrêt du programme, etc.) d’un programme est alors démontrée au travers d’une preuve de programme basée sur le calcul de la plus faible précondition .
Il a fallu attendre la fin des années 1990 pour que les méthodes formelles, Z , VDM et/ou la méthode B , soient utilisées sur des applications industrielles. Les méthodes formelles se basent sur des notations mathématiques pour décrire de façon précise les propriétés qu’un logiciel doit avoir.
L’un des écueils étant l’impossibilité de les mettre en œuvre dans le cadre d’une application industrielle (application de grande taille, contrainte de coût et de délais, etc.), la mise en œuvre – passage à l’échelle – ne peut se faire qu’au travers d’outils « suffisamment » matures et performants.
L’utilisation des méthodes formelles bien qu’en plein essor reste marginale, au vu du nombre de lignes de code. En effet, il y a à l’heure actuelle bien plus de lignes de code Ada (ANSI:1983, ISO 8652:1995, ), C (, ISO 9899:1999) ou C++ qui ont été produites manuellement qu’au travers d’un processus formel.
C’est pourquoi d’autres techniques formelles ont été mises en place afin de vérifier le comportement d’une application logicielle écrite dans un langage de programmation tel que le C ou l’Ada. La principale technique, nommée interprétation abstraite de programme, permet d’évaluer l’ensemble des comportements d’une application logicielle au travers d’une analyse statique. Ce type de techniques a donné naissance, à plusieurs outils tels que Codepeer, POLYSPACE, Caveat, Absint, FRAMAC et/ou ASTREE.
L’efficacité de ces techniques d’interprétation abstraite de programme a fortement progressé avec l’augmentation de la puissance des ordinateurs. Il est à noter que ces techniques nécessitent en général d’intégrer dans le code manuel des informations complémentaires telles que des préconditions, des invariants et/ou des postconditions.
À noter que la version 2012 du langage Ada introduit la possibilité de définir des préconditions, des invariants et des postconditions et qui peuvent être vérifiés durant l’exécution, et que l’environnement SPARK 2014 met à disposition un ensemble d’outils permettant de faire la preuve de ces propriétés.
Le domaine ferroviaire est réglementé et il est nécessaire de respecter les normes CENELEC EN 50126, 50129 et 50128 lors de la réalisation d’un système ferroviaire. Le référentiel CENELEC identifie les méthodes formelles comme moyen à mettre en œuvre.
Cet article fait le point sur l’utilisation des méthodes formelles dans la réalisation des applications ferroviaires de type signalisation, CBTC et contrôle/commande (unité de gestion de la traction, du freinage et/ou application TCMS pour Train Control/Management System).
Nota :
le CBTC, pour Communication Based Train Control, est un système composé d’équipements embarqués à bord des trains et d’équipements fixes communicants entre eux (en général par radio). Le CBTC fait l’objet d’une norme .
