Formal Specification and Development of a Safety-Critical Train Management System

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 provide several novel services at different levels of functionality, 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 cont...