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.

5 Comments

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

    The slides of the presentation are available here: https://github.com/openETCS/model-evaluation/blob/master/Munich_20130415/2013-04-15-GNATprove-ETCS-model.pdf?raw=true

    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

  4. Posted March 1, 2019 at 19:30 | Permalink

    Hello my loved one! I want to say that this post is awesome, nice written and include almost all important information. I would like to peer more posts like this. I’ll right away grab your rss feed as I situs togel terpercaya can’t to find your email subscription hyperlink or e-newsletter service. Do you’ve any? Kindly allow me recognise so that I may subscribe. Thanks.

  5. Posted March 4, 2019 at 07:32 | Permalink

    I would like to peer more posts like this. I’ll right away grab your rss feed as I buku mimpi can’t to find your email subscription hyperlink or e-newsletter service.

Post a Comment

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

*
*
 
  • Categories

  • Open-DO Projects

  • Contact

    info @ open-do.org