Abstrakt
The Hybrid ERTMS/ETCS Level 3 is a standard for the management and interoperation of signalling for railways by the European Union. Its aim was to increase the throughput of railway tracks, by integrating the physical information coming from the trackside detection system with information transmitted by the train itself regarding its position and integrity.
In this paper, we propose a formal model of the Hybrid ERTMS/ETCS Level 3 (ver. 1A) in Promela and its validation using Spin. We describe how we derived the model from the informal requirements and the abstractions we applied during this process; moreover, we explain how we validated and verified the model, and the ambiguities we detected in the requirements document.
Although Spin provides very good verification facilities, it lacks a proper support for performing user-driven validation by simulation and scenario specification; therefore, we propose two facilities built upon the Promela language (having different expressive power) that allow for easy specification of scenario execution.