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!
5 Comments
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).
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?
I like to read your article because it really helps me. Thank you for sharing this post with us. by : Angka Jitu Singapore
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.
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.