Specifications for safety-critical railway signalling systems have traditionally been expressed in natural language. Due to a lack of traceability features, these requirements are difficult to reason about and thus very resistant to change. Validation and verification processes of cyber-physical components based on such specifications require extensive manual review and are prone to inefficiencies. This paper describes our work towards a comprehensive methodology for deriving formal specifications for railway signalling and generating verified software for it. Our method focuses on accessibility for domain experts and industrial applicability. To this effect, we integrate established techniques into a unified tool chain comprising (1) fault tree analysis, (2) the goal-oriented requirements engineering method KAOS, and (3) formal modeling with AdaCore SPARK. We aim to facilitate end-to-end traceability of requirements through all artifacts. Currently, we are applying our methodology to a case study that involves the specification of a new ETCS-based moving block signalling system.