Formal Specification and Development of a Safety-Critical Train Management

In this paper we describe the on-going specification and development of Ansaldo’s Radio Block Center (RBC), a component of the next-generation European Rail Traffic Management System (ERTMS). The RBC will be responsible of managing the movement of trains equipped with radio communication. Its development process is critical: the RBC is a large-scale and complex system, it must guarantee interoperability according to European standards, and, last but not least, a high level of safety. We have addressed these issues by devising a development based on formal specifications. ERTMS scenarios have been formalized in order to provide a better understanding of the interoperability requirements. The architecture of the RBC has been formally specified such that the system can be incrementally built as an overlay system (compatible with the existing train detection and interlocking systems) and modularly expanded to control different kinds of trains. The formal specifications of the behaviour of each RBC module have been structured hierarchically: they provide an easy-to-understand documentation for customers and developers; moreover, they can be simulated and validated automatically at the early stage of the development process, thus providing a high level of confidence in their safety in a cost-effective way