Interlocking systems carry out the critical function of routing of trains throughout a station. In this paper, we discuss the research underlying the program to migrate the Italian Railway Network from legacy relay-based to software-based interlocking. The long-term program tackles many challenges: dealing with legacy, relay-based intelockings; providing a solution amenable for domain experts; developing a unique, highly configurable framework for large-scale deployment. The overarching ecosystem, called OPERA, relies on the adoption of controlled natural languages, model-based technologies, and formal verification. OPERA integrates five tools: AIDA, for interlocking procedures specification and code generation; TOSCA, for test case specification and generation; CARMEN, for formal verification; LUCIA, for the formalization of guideline documents; NORMA, for the specification and verification of relay-based interlocking.