Présentation

Article

1 - DÉVELOPPEMENT DU LOGICIEL

2 - NORMES FERROVIAIRES

3 - MÉTHODES FORMELLES, SEMI-FORMELLES, STRUCTURÉES ET TECHNIQUES FORMELLES

4 - MISE EN ŒUVRE DES MÉTHODES FORMELLES LORS DE LA RÉALISATION D’UNE APPLICATION LOGICIELLE

5 - RÉALISATION METTANT EN ŒUVRE LES APPROCHES FORMELLES

6 - LOGICIEL PARAMÉTRABLE

7 - QUALIFICATION

8 - CONCLUSION

9 - GLOSSAIRE

Article de référence | Réf : TRP3309 v1

Méthodes formelles, semi-formelles, structurées et techniques formelles
Méthodes formelles : application au domaine ferroviaire

Auteur(s) : Jean-Louis BOULANGER

Date de publication : 10 févr. 2016

Pour explorer cet article
Télécharger l'extrait gratuit

Vous êtes déjà abonné ?Connectez-vous !

Sommaire

Présentation

Version en anglais 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’article

ABSTRACT

Formal Methods : Application to the Railway Domain

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)

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).

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 .

Cet article est réservé aux abonnés.
Il vous reste 93% à découvrir.

Pour explorer cet article
Téléchargez l'extrait gratuit

Vous êtes déjà abonné ?Connectez-vous !


L'expertise technique et scientifique de référence

La plus importante ressource documentaire technique et scientifique en langue française, avec + de 1 200 auteurs et 100 conseillers scientifiques.
+ de 10 000 articles et 1 000 fiches pratiques opérationnelles, + de 800 articles nouveaux ou mis à jours chaque année.
De la conception au prototypage, jusqu'à l'industrialisation, la référence pour sécuriser le développement de vos projets industriels.

KEYWORDS

formal method   |   verification   |   critical software   |   embedded system

DOI (Digital Object Identifier)

https://doi.org/10.51257/a-v1-trp3309


Cet article fait partie de l’offre

Systèmes ferroviaires

(55 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

ABONNEZ-VOUS

Version en anglais En anglais

3. Méthodes formelles, semi-formelles, structurées et techniques formelles

3.1 Définitions

HAUT DE PAGE

3.1.1 Modèle

La définition d’un modèle M est un moyen pour comprendre et/ou appréhender un problème/une situation. En général, la phase de spécification qui permet de s’approprier le cahier des charges passe par la création d’un modèle M.

Un modèle peut être plus ou moins proche du système étudié, on parle alors d’abstraction. Plus la modélisation est proche, plus les résultats obtenus seront proches de ceux qui seront observés sur le système final.

Si le modèle est utilisé pour l’élicitation des exigences, il sera plutôt un prototype du système à réaliser. S’il est utilisé pour la vérification des exigences (cohérence, complétude, etc.) il aura la forme d’une collection de modèle, chaque modèle permettant de modéliser une ou plusieurs exigences.

Une autre caractéristique des modèles provient du fait que le langage support dispose ou non d’une sémantique. En l’absence de sémantique, il s’agit de modèle pour conceptualiser et raisonner sur le besoin. En présence de sémantique, il sera possible de vérifier des propriétés, voir de générer tout ou partie du code finale.

La présence d’une sémantique permet de mettre en œuvre des techniques de raisonnement qui garantissent la correction (au sens vérification) des résultats obtenus. La sémantique permet effectivement de vérifier que le logiciel respecte des propriétés (d’ou le retrait de certaine phase de tests comme les TU et les TI L/L) mais il reste nécessaire d’exécuter le logiciel sur la machine cible afin de vérifier que l’ensemble (logiciel + matériel support) est conforme aux exigences. La machine cible pouvant compromettre l’exécution du logiciel.

Dès le niveau SSIL 1, la nouvelle version de la norme CENELEC EN 50128:2011 – table A.3 recommande que l’architecture de l’application logicielle se base sur une méthode structurée (SADT, OMT, etc.). Mais il est possible de mettre en place une modélisation qui se base sur les techniques de la table A.17 (tableau 2).

Il ressort des différents projets (réalisé...

Cet article est réservé aux abonnés.
Il vous reste 92% à découvrir.

Pour explorer cet article
Téléchargez l'extrait gratuit

Vous êtes déjà abonné ?Connectez-vous !


L'expertise technique et scientifique de référence

La plus importante ressource documentaire technique et scientifique en langue française, avec + de 1 200 auteurs et 100 conseillers scientifiques.
+ de 10 000 articles et 1 000 fiches pratiques opérationnelles, + de 800 articles nouveaux ou mis à jours chaque année.
De la conception au prototypage, jusqu'à l'industrialisation, la référence pour sécuriser le développement de vos projets industriels.

Cet article fait partie de l’offre

Systèmes ferroviaires

(55 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

ABONNEZ-VOUS

Lecture en cours
Méthodes formelles, semi-formelles, structurées et techniques formelles
Sommaire
Sommaire

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)...

Cet article est réservé aux abonnés.
Il vous reste 94% à découvrir.

Pour explorer cet article
Téléchargez l'extrait gratuit

Vous êtes déjà abonné ?Connectez-vous !


L'expertise technique et scientifique de référence

La plus importante ressource documentaire technique et scientifique en langue française, avec + de 1 200 auteurs et 100 conseillers scientifiques.
+ de 10 000 articles et 1 000 fiches pratiques opérationnelles, + de 800 articles nouveaux ou mis à jours chaque année.
De la conception au prototypage, jusqu'à l'industrialisation, la référence pour sécuriser le développement de vos projets industriels.

Cet article fait partie de l’offre

Systèmes ferroviaires

(55 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

ABONNEZ-VOUS