Building a metro in a week: formal methods in action at CentraleSupélec

CentraleSupélec students bring the Metropolis metro to life

For the fifth year in a row, Prover joined CentraleSupélec in Paris to supervise the “Signaling Design Automation” integration project. For one week, 33 engineering students took on the role of a signaling supplier, using Prover iLock and Prover Studio to develop the software of a complete metro network.

A city, a network, a backlog

The project starts with a letter from the fictional city of Metropolis: its metro network needs new interlockings. The network has 8 lines, 29 stations and 11 interchanges. Many of its stations are named after pioneers of formal methods and computer science: Turing, Ada Lovelace, Dijkstra, Margaret Hamilton, Kripke, Clarke, Emerson, Sifakis, McMillan and Stålmarck.

Each of the eight student teams was responsible for one line, with one interlocking per station: 41 interlockings in total. As in a real project, the work was described in a backlog of tickets, not a list of exercises. The teams had to plan their week, split the work, ask the client the right questions and deliver.

From station layouts to a running line

Ticket after ticket, the teams went through the full Signaling Design Automation workflow:

• Layout. They drew the track layout of each station on their line and configured the interlockings from a generic application written in PiSPEC.
• Proof. They used formal verification to find and fix errors in the generic application, then formalized new safety requirements and proved them with automatic model checking.
• Testing. They wrote test cases and ran them in simulation.
• New functions. They designed and verified new interlocking functions such as manual route release, together with their safety properties and tests.
• Integration. They connected the interlockings of their line and simulated the whole line end to end, with the interlockings exchanging data in real time.

Opening day for Metropolis metro

By the end of the week, the Metropolis metro was ready to open. There were a few last-minute issues at two or three stations, which is not unusual for a commissioning. In one week, the students went through the same cycle our customers follow for their signaling projects: specify, design, prove, test and generate.

Thank you

We warmly thank the students for their energy and commitment. They impressed us with how quickly they mastered our tools, the PiSPEC language and the railway domain. Special thanks go to Idir Ait Sadoune and the CentraleSupélec teaching team for renewing their trust in us.

At Prover, we believe that introducing the next generation of engineers to formal methods and signaling is essential for safer and more reliable railways. If you are interested in an internship in formal methods or railway signaling, we have offices in Toulouse and Stockholm in several fields. Please have a look at our career site.