A Formal Specification for a Real-Time Train Controller

We give a formal specification for a real-time controller for trains that operate on the Italian railway network. The controller will control train movements and is part of a larger system destined to guarantee safety with respect to dangers originating from train traffic in the railway network. Based on an informal specification document from the Italian railway company, we construct a simple state-based model and formalise it in terms of the property-based specification language TRIO. The obtained specification being formal, we are able to perform certain verifications on it, such as checking its satisfiability and verifying correctness of refinement steps.