A methodology for automatic generation, formal verification and implementation of safe PLC programs for power supply equipment of the electric lines of railway control systems

Abstract

To improve the design, Verification and Validation phases of Power Supply Equipment of the Electric Lines control systems at French Railway Company (SNCF for Société nationale des chemins de fer français), this paper proposes an integrated methodology, for automatic generation, formal verification and implementation of safe Programmable Logic Control (PLC) programs. The main objective is to save time and to improve the “overloaded” workflow of systems engineers. This methodology is compliant with the traditional engineering workflow. The first phase of the methodology focuses on the automatic generation of PLC programs, wiring diagrams , and test-based recipe books, based on reusing and adapting similar models of existing projects to the new specifications (corresponding to functional and safety requirements). The second phase is related to the application of formal verification and control synthesis techniques to guarantee the safety of the control installation. The first phase of the methodology has been successfully deployed at SNCF. The second phase is currently being evaluated.