Bibliographie & annexes
Présentation
En anglais
RÉSUMÉ
Depuis le développement de la première application ferroviaire à base de logiciel, nommée SACEM, les méthodes formelles ont été largement utilisées et mises en œuvre par des industriels à différents niveaux (spécification, conception, code) et pour différents types d’applications (métros automatiques, sous-systèmes de signalisation, applications trains développées avec ControlBuild par exemple). La norme CENELEC 50128 dédiée à la réalisation des applications logicielles pointe l’intérêt de mettre en œuvre des méthodes formelles. Cet article présente le processus de développement des applications logicielles tel que mis en œuvre dans le domaine ferroviaire, et les évolutions induites par la mise en œuvre des méthodes formelles.
Lire cet article issu d'une ressource documentaire complète, actualisée et validée par des comités scientifiques.
Lire l’articleABSTRACT
Since the development of SACEM, the first software application in the railway sector, formal methods have been widely used and implemented by the industry at different levels (specification, design and code analysis) and for different types of applications (automated metro lines, signaling subsystems, railway applications developed with ControlBuild, for example). The CENELEC 50128 standard for implementing advanced software applications highlights the benefits of formal methods. This article presents the process of developing software applications as implemented in the railway sector, and the changes brought about by the implementation of formal methods.
Auteur(s)
-
Jean-Louis BOULANGER : Evaluateur-Certificateur Certifer (Anzin, France)
INTRODUCTION
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).
L'expertise technique et scientifique de référence
KEYWORDS
formal method | verification | critical software | embedded system
DOI (Digital Object Identifier)
Cet article fait partie de l’offre
Systèmes ferroviaires
(56 articles en ce moment)
Cette offre vous donne accès à :
Une base complète d’articles
Actualisée et enrichie d’articles validés par nos comités scientifiques
Des services
Un ensemble d'outils exclusifs en complément des ressources
Un Parcours Pratique
Opérationnel et didactique, pour garantir l'acquisition des compétences transverses
Doc & Quiz
Des articles interactifs avec des quiz, pour une lecture constructive
Présentation
Conclusion
En anglais
7. Qualification
7.1 Besoins
Dans sa version 2001, la norme CENELEC EN 50128 introduisait une demande de qualification des compilateurs, sans vraiment indiquer ce qui était attendu.
La version 2011 de la norme CENELEC EN 50128 introduit formellement le besoin de qualifier les outils (voir § 6.7 de la norme). Comme pour l’IEC 61508 et l’ISO 26262, trois classes d’outils, T1, T2 , T3, ont été introduite :
-
la classe T1 est dédiée aux outils qui n’ont pas d’impact sur la vérification et qui n’ont pas d’impact sur l’exécutable final ;
-
la classe T2 est dédiée aux outils ou un défaut pourrait fausser les résultats de vérification ou de validation. La classe T2 contient les outils de vérification de règles de codage, de mesure des métriques, d’analyse statique de code, de gestion et d’exécution des tests, etc. ;
-
la classe T3 est dédiée aux outils dont une défaillance pourrait avoir un effet sur l’exécutable final. Cette classe concerne les compilateurs, les générateurs de code, etc.
La section 6.7 de la norme CENELEC 50128:2011 définit pour chaque classe un jeu de recommandations qui permet d’identifier le contenu du dossier de qualification.
Dans le cadre de l’article [TRP 3 304], nous avons traité précisément l’analyse de la qualification des outils (processus et document à produire) comme cela est demandé par la norme CENELEC EN 50128.
HAUT DE PAGE7.2 Difficultés
L’un des points délicats concernant la mise en œuvre des différents outils réside dans la démonstration que l’outil est utilisable pour le niveau de sécurité qui est visé.
Comme le montre la figure 46, pour réaliser la qualification d’un outil, il faut mettre en place une activité de qualification qui peut être basé :
-
sur un certificat : il existe des certificats pour certains outils comme les compilateurs et les générateurs de code (par exemple le générateur de code C à partir du modèle SCADE est certifié SSIL3-4 pour la norme ferroviaire CENELEC EN 50128) ;
-
sur...
L'expertise technique et scientifique de référence
Cet article fait partie de l’offre
Systèmes ferroviaires
(56 articles en ce moment)
Cette offre vous donne accès à :
Une base complète d’articles
Actualisée et enrichie d’articles validés par nos comités scientifiques
Des services
Un ensemble d'outils exclusifs en complément des ressources
Un Parcours Pratique
Opérationnel et didactique, pour garantir l'acquisition des compétences transverses
Doc & Quiz
Des articles interactifs avec des quiz, pour une lecture constructive
Qualification
BIBLIOGRAPHIE
-
(1) - ABRIAL Jr., The B Book - Assigning programs to meanings. - Cambridge University Press, Cambridge, août 1996.
-
(2) - BOULANGER (J.-L.), SCHÖN (W.) - Logiciel sûr et fiable : retours d’expérience. - Revue Génie Logiciel, n° 79, p. 37 à 40, déc. 2006.
-
(3) - BOULANGER (J.-L.), SCHÖN (W.) - Assessment of safety railway application. - ESREL (2007).
-
(4) - BOULANGER (J.-L.) - Expression et validation des propriétés de sécurité logique et physique pour les systèmes informatiques critiques. - Thèse, Université de Technologie de Compiègne (2006).
-
(5) - Sous la direction de BOULANGER (J.-L.) - Utilisations industrielles des techniques formelles – Interprétation abstraite. - Collection IC2, Hermès (2011).
-
(6)...
DANS NOS BASES DOCUMENTAIRES
CENELEC http://www.cenelec.eu/Cenelec/Homepage.htm
COFRAC http://www.cofrac.fr
EPSF http://www.securite-ferroviaire.fr/
ERTMS http://www.ertms.com
ISO http://www.iso.org/iso/home.html
MODUrban http://www.modurban.org/
STRMTG http://www.strmtg.equipement.gouv.fr/
UGTMS http://www.ugtms.jrc.cec.eu.int/
CodePeer http://www.adacore.com/codepeer/
Polyspace http://www.mathworks.com/products/polyspace/
Caveat https://ieeexplore.ieee.org/document/1028953
Absint http://www.absint.com/
FRAMAC http://frama-c.com/
ASTREE http://www.astree.ens.fr/
ADA 2012 http://www.ada2012.org/...
L'expertise technique et scientifique de référence
Cet article fait partie de l’offre
Systèmes ferroviaires
(56 articles en ce moment)
Cette offre vous donne accès à :
Une base complète d’articles
Actualisée et enrichie d’articles validés par nos comités scientifiques
Des services
Un ensemble d'outils exclusifs en complément des ressources
Un Parcours Pratique
Opérationnel et didactique, pour garantir l'acquisition des compétences transverses
Doc & Quiz
Des articles interactifs avec des quiz, pour une lecture constructive
