Validation of railway data. In CBTC systems, the track is divided into several sub-sections, each of which is controlled by safety critical software. In order to avoid multiple developments, each software is made from a generic B-model and parameters that are specific to a sub-section. The proof of the generic B-model relies on assumptions that formally describe the topology properties of the track. We therefore have to make sure that the parameters used fulfil the formal assumptions. For example, in case of the San Xxxx development, about 300 assumptions were made. It is vital that these assumptions are checked when the system is put in place, as well as whenever the rail network topology changes (e.g., due to line extension or addition or removal of certain track sections). For this, STS has developed the following approach: • The topology is extracted from the ADA program and encoded in B syntax, written into AtelierB definition files. • The relevant part of the B model is extracted and conjoined with the definition files containing the topology. • The properties and assertions are proven with Atelier B, using custom proof rules and tactics. There are two problems with this approach. • If the proof of a property fails, the feedback of the prover is not very useful in locating the problem (and it may be unclear whether there actually is a problem with the topology or "simply" with the power of the prover). • The constants are very large (relations with thousands of tuples) and the properties so complex (see Figure 2) that Atelier B quite often runs out of memory. For example, for the San Xxxx development, 80 properties (out of the 300) could not be checked by Atelier B (because of memory overflow). The second point means that these properties have to be checked by hand (e.g., by creating huge spreadsheets on paper for the compatibility constraints of all possible itineraries). For the San Xxxx development, this meant about one man month of effort, which is likely to grow much further for larger developments. The starting point of this experiment was to try to automate this task, by using an alternate technology. Indeed, the proB plugin has capabilities to deal with B properties in order to animate and model check B models. The big question was, whether the technology would scale to deal with the industrial models and the large constants in this case study. To handle the large model provided by STS, proB was improved, in particular the Parser and the Type Inference. In order to eval...
