Informatique et Systèmes d'Information

Les techniques formelles réalisent des modèles de spécifications et/ou de conception servant à l'analyse statique de code, à la démonstration du respect de propriété, à la bonne gestion des calculs sur les flottants, etc.

Dès la première introduction des logiciels au sein d'un équipement, la RATP a mis en oeuvre les techniques formelles afin de démontrer que des impératifs de sécurité sont respectés par le logiciel.

Cet ouvrage présente des exemples concrets de mise en oeuvre des techniques (simulation, model-checking , preuve) et des méthodes formelles (méthode B, SCADE) sur des projets de transport ferroviaire de type métro et grande-ligne (ligne classique, TGV, ERTMS ou fret).