This year, we once again had the pleasure of introducing Signaling Design Automation to the students of CentraleSupélec in Paris. Our goal was to engage them in the real-world challenges of working on a railway project using formal methods and the generic application/specific applications approach. Thirty-eight students, in eight groups, worked simultaneously to develop eight small lines, with three interlockings each, using Prover iLock and Prover Studio.

We started with a brief introduction to railway fundamentals, after which students dived into practical examples. They started by setting up a new interlocking track layout, then proceeded to debug the generic application we provided, verifying the validity of safety requirements and functional tests. After this initial stage, students then created their own safety requirements and test cases. In the final stage, they added a manual release feature to their interlocking system, covering key elements like design, safety requirements, and testing.

We extend our sincere appreciation to the dedicated students of CentraleSupélec for their commitment and enthusiasm throughout the week. They impressed us with how quickly they got the hang of our tools, languages, and the railway field. Special thanks also to their teachers, in particular Idir Ait Sadoune, for trusting us again this year.

We hope to have the opportunity to see these talented students again in the railway industry or in the field of formal methods. We believe that opportunities to introduce these two fields to new students are essential. We are convinced that this new generation of talents can contribute to the development of these two exciting fields for engineering a safer world.

Share this article

Learn to build a solid safety case for rail control systems using formal verification

Fill out your information here.

Do you want news and upcoming events from Prover?

Fill out your information here.

More News & Articles

  • When replacing relay interlockings, most conversations start with technology. The better starting point is governance: how do you make sure you can still change parts of the system 20 years from now? We look at what Open Signaling means in practice, and how our Stockholm Metro pilot was designed for replaceability from day one.

  • Prover, RATP and Systerel publish the unified HLL 4.0 specification, keeping the rail industry's formal verification language open and free of dialects.

  • Generative AI has entered railway software engineering ahead of the standards governing it. A new CENELEC draft amendment to EN 50716 doesn't add requirements. It clarifies which existing rules apply when AI drafts specs, writes code, or generates test cases, and why those rules are harder to satisfy with generative models than teams might assume.