| Line 61: | Line 61: | ||
== Testimonials == | == Testimonials == | ||
*[https://link.springer.com/chapter/10.1007/978-3-031-05814-1_11 The 4SECURail Formal Methods Demonstrator, Franco Mazzanti and Dimitri Belli] | *[https://link.springer.com/chapter/10.1007/978-3-031-05814-1_11 The 4SECURail Formal Methods Demonstrator, Franco Mazzanti and Dimitri Belli] <i>""The second framework that has been chosen to support the formal analysis of the system is ProB [16]. Indeed, according to several surveys (see, e.g., [17,18,19]) B/EventB appears to be one of the most adopted formal methods in railways. Moreover, ProB has a very user-friendly interface requiring a small effort to be learnt and powerful verification methods. Last but not least, it is freely available as an open-source product."</i> | ||
<i>""The second framework that has been chosen to support the formal analysis of the system is ProB [16]. Indeed, according to several surveys (see, e.g., [17,18,19]) B/EventB appears to be one of the most adopted formal methods in railways. Moreover, ProB has a very user-friendly interface requiring a small effort to be learnt and powerful verification methods. Last but not least, it is freely available as an open-source product."</i> | |||
* [http://www.deploy-project.eu/pdf/D41-Siemens-final-full.pdf Data validation at Siemens, Jérôme Falampin]: <i>""The work done with ProB is a great success. Thanks to the automatization and ProB, the wayside data validation is quicker, easier and complete."</i> More details and academic papers can be found on our page [[Siemens Data Validation with ProB]]. | * [http://www.deploy-project.eu/pdf/D41-Siemens-final-full.pdf Data validation at Siemens, Jérôme Falampin]: <i>""The work done with ProB is a great success. Thanks to the automatization and ProB, the wayside data validation is quicker, easier and complete."</i> More details and academic papers can be found on our page [[Siemens Data Validation with ProB]]. | ||
* [http://dl.acm.org/citation.cfm?doid=2406336.2406351 Pacemaker model by Mery and Singh]: <i>"ProB was very useful in the development of the pacemaker specification, and was able to animate all of our models and able to prove the absence of error (no counterexample exist). The ProB model checker also discovered several invariant violations, e.g., related to incorrect responses or unordered pacing and sensing activities. It was also able to discover a deadlock in two of the models, which was due to the fact that “clock counter” were not properly recycled, meaning that after a while no pacing or sensing activities occur into the system. Such kind of errors would have been more difficult to uncover with the prover of RODIN tool."</i> | * [http://dl.acm.org/citation.cfm?doid=2406336.2406351 Pacemaker model by Mery and Singh]: <i>"ProB was very useful in the development of the pacemaker specification, and was able to animate all of our models and able to prove the absence of error (no counterexample exist). The ProB model checker also discovered several invariant violations, e.g., related to incorrect responses or unordered pacing and sensing activities. It was also able to discover a deadlock in two of the models, which was due to the fact that “clock counter” were not properly recycled, meaning that after a while no pacing or sensing activities occur into the system. Such kind of errors would have been more difficult to uncover with the prover of RODIN tool."</i> | ||