GNATprove Takes the Train

David Mentré from Mitsubishi Electric R&D Centre Europe has produced a very interesting report on his use of GNATprove (the formal verification tool we develop for the next version of SPARK) on a case-study from the Open-ETCS European project, to develop the tools for the future European Train Control Systems.

Although David asked me to mention this is highly experimental (neither fully proved nor fully tested), I think it shows quite well what one can do with formal verification. The report contains inlined code showing how some units were specified using preconditions/postconditions and annotated with assertions for proofs. You can also download the code from github, or browse it online.

David will present this model at an internal Open-ETCS meeting next Monday, I’ll ask him to post the conclusion of his presentation!

This entry was posted in Open-DO News and tagged , , . Bookmark the permalink. Post a comment or leave a trackback: Trackback URL.


  1. David Mentré
    Posted April 17, 2013 at 16:39 | Permalink

    The slides of the presentation are available here:

    On openETCS benchmark, I was able to do most of activities, even if not all of this small model made has been fully proven.

    From our point of view, GNATprove is a very interesting technology. They are currently rough edges but it seems promising for safety critical embedded systems. The ability to mix tests and proofs is very interesting and useful in practice (e.g. help debug formal assertions).

  2. Yannick Moy
    Posted April 22, 2013 at 23:01 | Permalink

    Thanks David for the slides and nice comment. I see that you mention the “safety principles” that are missing, like in your report. Can you explain what are those? Can they be formalized?

  3. Posted November 13, 2018 at 08:02 | Permalink

    I like to read your article because it really helps me. Thank you for sharing this post with us. by : Angka Jitu Singapore

Post a Comment

Your email is never published nor shared. Required fields are marked *

  • Categories

  • Open-DO Projects

  • Want to get involved?

  • Contact

    info @