
Beginning May 18th, I led a four-day online crash course on HLL for a dozen safety engineers. Due to the French COVID-19 lockdown, the course was conducted via Microsoft Teams, alternating lectures and exercises. An online course is a very special experience: you can get very close to a student’s activities when sharing terminals and files. At the same time, when someone doesn’t speak or write anything, you can’t even know where they are! I felt that we are not an online course company as is, and this kind of course could be improved by some extra communication tools and personalization. My lectures were live, while recorded ones would allow trainees to set their own pace. I also think that I would make sure the trainees have access to a shared chat, even in a face to face course. This allows rich interactions and stores questions and answers one could revisit anytime.
This course provided a practical introduction to formal verification activities that are encountered in real-world projects. We talked about formalizing requirements, environment modeling through constraints, choosing an appropriate proof strategy and, of course, some debugging. This may sound like it would require a strong background in software engineering to be at ease with the software tools. However, the attendees revealed unexpected skills when digging into PSL – our proof engine – and its associated tools.
As per usual in formal verification, a large amount of time was spent on the corner cases of requirement specification. Indeed, even though safety engineers are used to providing such requirements, they were sometimes surprised when formalization exposed some missing behaviors or lack of precision. Manipulating HLL formulas, especially when quantification enters, is a powerful way to reveal corner cases of even the most simple designs.
Prover would like to congratulate all of the attendees for their patience and enthusiasm during this course, helping to share lessons learned with others. We are happy that more people are now Prover Certified formal verification engineers.
Share this article

Learn to build a solid safety case for rail control systems using formal verification
Fill out your information here.
More News & Articles
Prover is partnering with Eiffage Énergie Systèmes on the Villeneuve Demain project, delivering railway signaling software for the PAVS system at SIL4 safety level.
Using Prover’s automation tools, the solution ensures EN 50716 compliance, facilitates future maintenance, and enables reuse across similar systems.
Prover will be at Train & Rail, meet us in our booth located at A06:31.
Learn how Prover’s Relay Signaling Migration enables safe, efficient modernization of legacy railway systems with formal verification and digital twin technology.