This article describes techniques for applying formal mathematical methods to the specification and design of railway signalling and interlocking equipment which is implemented using microprocessors and real-time software. Our results have been obtained by combining the specification language higher-order logic (HOL) with the disciplined use of annotated subsets of the computer programming languages such as Ada. A global framework has been developed both for computer-aided design (CAD) tools for railway interlocking and for the future development of the operational software for practical signalling systems.