Author(s)

J.L Boulanger & M. Gallardo

Abstract

Validation and verification of METEOR safety software J.L. Boulanger & M. Gallardo Abstract The study described in this paper was conducted by the Paris Public Transport Authority (RATP) and aimed to verify the correct application of the concept by the establishment of lists of tests to be played on the final software. In this article, we present the validation process which has been chosen by the RATP team in charge of fixed equipment for the automatic Paris metro system METEOR (Metro Est Quest Rapide - high-speed east-west metro). The idea of properties which the software must respect is one of the characteristics of this validation process. This article gives an idea of industrial practices within a context of installing a safety-critical system implementing formal methods such as ASA+ and the B method. METEORs complexity will be quantified throughout the article, using information such as the number of B components, the number of lines of ADA code produced by the code g

Keywords