Industrial application of event-B to a wayside train monitoring system: Formal conceptual data analysis

Abstract

The experience gained in the application of Event-B to a subsystem of a wayside train monitoring system (WTMS) will be presented in this paper. The WTMS configuration management system (CMS) supports the creation and management of configuration data for the WTMS. Consistency of system data is one of the most important quality properties of a CMS since inconsistency may lead to critical malfunctioning. Therefore, the development of the data handling part of a CMS requires the use of high integrity methods in order to ensure the highest quality. Event-B, with its set-theoretic basis for modelling, its approach of refinement and the use of formal proof to ensure consistency of refinement steps, is used in this study for the conceptual modelling of system data and system operations. Due to the Agile-structured development process, the conceptual model has been created in several iterations by a changing team of developers. The challenge was to guarantee completeness and consistency of this model and to keep it aligned with the goals of all relevant stakeholders. This has been achieved by producing an incremental, refinement-based creation of a formal conceptual model together with an appropriate formalization of the conceptual data constraints. The relationship between the conceptual model and the formal conceptual model has been realized by using an appropriate traceability model. This paper describes how the application of Event-B can successfully address these challenges.