Présentation
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'articleAUTEUR(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
Cet article est réservé aux abonnés. Il vous reste 92 % à découvrir.
Déjà abonné ? Se connecter
MOTS-CLÉS
méthode formelle | vérification | logiciel critique | système embarqué
DOI (DIGITAL OBJECT IDENTIFIER)
Méthodes formelles : application au domaine ferroviaire
Développement du logiciel
Sources bibliographiques
Cet article est réservé aux abonnés. Il vous reste 92 % à découvrir.
Déjà abonné ? Se connecter
Article inclus dans l'offre
"Systèmes ferroviaires"
(
62 articles
)
Actualisée et enrichie d’articles validés par nos comités scientifiques.
Quiz, médias, tableaux, formules, vidéos, etc.
Opérationnels et didactiques, pour garantir l'acquisition des compétences transverses.
Un ensemble de services exclusifs en complément des ressources.
