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.
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
Cet article est réservé aux abonnés. Il vous reste 92 % à découvrir.
Ingénieurs en bureau d\'études, répondez aux exigences techniques de vos clients grâce aux ressources de Techniques de l\'Ingénieur. Retrouvez dans les articles...
Ce grand événement dédié à la Big Data et à l\'Intelligence Artificielle, aura lieu le 26 et 27 septembre au Palais des Congrès de Paris. Ce sera l’occasion de ...
Découvrez le salon S.O.C (Systèmes et Objets Connectés), où vous pourrez rencontrer les acteurs des systèmes et objets connectés et découvrir les solutions adap...
*Rappel téléphonique réservé aux pays suivants : France métropolitaine, Belgique, Luxembourg, Monaco, Suisse.
Article avec quiz
Cette offre comprend des articles interactifs. Leurs quiz mettent en lumière les informations clés à retenir et valident leur acquisition : de lecteur à joueur, enrichissez vos connaissances.
Vous les repérez facilement grâce à ce pictogramme :