Property-Based Modelling and Validation of a CBTC Zone Controller in Event-B

This paper describes a formal analysis method applied at the software design level. The objective is to prove that a software specification and its implementation satisfy the expected system properties. In our case the analysed design is that of the Zone Controller of a CBTC developed using B. The B-Method is used to ensure that the implementation is correct wrt the software specification, but it does not guarantee that the algorithms described in the specification are correct wrt the system level requirements. Our analysis overcomes this shortcoming, providing a stronger assurance that the designed software meets its objectives. In particular, we prove that the implemented algorithms ensure that the track portion actually occupied by a train is covered by a protection envelope on the software side. The analysis is formalised with an Event-B model that is subject to tool-based inspections: animation with ProB and formal proof with Atelier B. In contrast to the existing B-Method model, our Event-B model links environment variables (the real position of the trains) with software variables (protection envelopes) and models the assumptions about the possible evolution of the environment. This analysis was carried out on an industrial scale software, consisting of 12000 lines of executable code, with immediate concrete results. This paper shows that, in addition to demonstrating compliance, this approach is clearly of interest from an industrial point of view.