Engineering for Critical Systems: The Automatic Train Operation over European Train Control System for Freight Trains Use Case

An ISO standard is the result of a process ensuing from an international industrial consensus. The norm provides a specification, the quality of which is ensured by international experts and may detail the mean to ensure a correct implementation of a given standard. To provide an example in the railway domain, the behavioural specification for the European Vital Computer (EVC) is documented in Subset 26 [1], but the mean for checking this subset fulfilment can be found in Subset 76 [2]. This last subset provides a set of test scenarios that have to be performed successfully, whereas a test bench specification is available in Subset 94 [3]. The European Commission required that corresponding tests have to be executed by independent test laboratories and a way for these independent laboratories to validate their ability is to be evaluated by a national accreditation office in charge of the respect of the ISO/IEC 17025 (https://www.boutique.afnor.org/en-gb/standard/iso-iec-170252017/general-requirements-for-the-competence-oftesting-and-calibration-laborato/xs129227/127779) norm. The global framework for EVC assessment is industrially running for many years. It is also efficient, but expensive because of the use of test benches belonging to external laboratories. Moreover, when the technical system becomes more complex, the quantity of tests exceeds, in the case of Subset 26 conformance, the quantity of 800 tests that must be performed on the real EVC. Considering that there are no laboratories for independent EVC testing in Netherlands, it is obvious that additional constraints introduced in the industrial process are heavy and expensive. In this paper another approach, to assess conformity to norms, is proposed. It transforms a model specifying the required behaviour into a formalism that allows generating byte code or source code in such a way that a continuous certified workflow produces the software, ensuring the required properties.

Section 2 explains step by step the global model engineering methodology while discussing the potential added value of norm modelling, providing examples relative to the railway domain. In Section 3, the methodology is partly illustrated on a case study. This case study is documented using normative or pre-normative documents and the main objects are identified and exploited in order to provide a set of software entities that may be used to build software services. Section 4 provides some conclusions and prospects concerning the remaining unsolved methodological, technical and scientific deadlocks.

The paper proposes an alternative approach to model-based testing. Starting from a SysML model, the main architectural assumptions of the considered system may be formally validated through invariant fulfilment of an Event-B model. Moreover, a refinement link, for a particular implementation of the considered specification and a given model of the norm, contributes to the global conformity. A railway case study is provided in order to illustrate the methodology. It consists of using an automatic operation system over ETCS, while a driver is in charge of safety relevant operations. Analyzing normative documents, assumptions of functioning are explained in a first part of the paper. In a second part, a SysML model of the higher levels of the architecture is described. This SysML model is expressed in a dedicated profile and then transformed into Event-B specifications. This paper presents the main elements of an approach which is correct-by-construction. Applying the systematic multi-layered approach of the study [28] on the AoE case study may provide a more relevant document for software engineering scientist. It may provide an illustration of the methodology on a real size example. Moreover, this application may be used as a benchmark to evaluate concurrent tools and approaches promoted by the scientific community. Following this point of view, it may be useful to present a system analysis built directly on Subset 125 [19]. The case study of the presented paper is an extended version of a railway conference paper [20] presenting AoE as a building brick towards GoA4 autonomous trains. This aspect is not developed any more in the current document, but the underlying vision of this previous paper should be adapted to a wider audience than transport scientists. Starting from this context, the full specification of the methodology application on this case study is published (https://github.com/RacemBougacha/ATO-over-ETCS.git). In order to apply a KAOS methodology [32], it is obvious that further work concerning model engineering are needed. Considering a real size application, a tooled framework assisting the alignment process between high level goals and architecture component would be a precious help. Finally, the added value of the proposed alternative to classical model-based testing still needs to be evaluated from a scientific and technological point of view. Among other points, the reliability of the transformation process, promoted by the current study, is a critical point where formal proofs can contribute efficiently [33].