| (7 intermediate revisions by the same user not shown) | |||
| Line 30: | Line 30: | ||
* [https://github.com/Joshua27/BSynthesis BSynthesis] tool for repair and generation of formal models | * [https://github.com/Joshua27/BSynthesis BSynthesis] tool for repair and generation of formal models | ||
* [https://safecap.co.uk SafeCap] | * [https://safecap.co.uk SafeCap] | ||
* [https://pkoerner.github.io/lisb-doc/ LisB], a Clojure/DSL API built-on top of the ProB-JAVA API | |||
* [http://wiki.event-b.org/index.php/IUML-B iUML Statemachines] | * [http://wiki.event-b.org/index.php/IUML-B iUML Statemachines] | ||
* [http://users.ecs.soton.ac.uk/vs2/ac.soton.multisim.updatesite/ MultiSimulation Plug-In for Rodin] | * [http://users.ecs.soton.ac.uk/vs2/ac.soton.multisim.updatesite/ MultiSimulation Plug-In for Rodin] | ||
| Line 66: | Line 67: | ||
== Testimonials == | == Testimonials == | ||
* [https://prologyear.logicprogramming.org/ColmerauerPrize.html Alain Colmerauer Prize, celebrating the 50th anniversary of Prolog]<i> "The winner of the first edition of the Prize was announced at the Prolog Day Symposium, on November 10, 2022: ProB: Harnessing the Power of Prolog to Bring Formal Models and Mathematics to Life. Michael Leuschel and STUPS Group."</i> | |||
* [https://link.springer.com/chapter/10.1007/978-3-031-67114-2_13 Proving B with Atelier B]<i>" In the early 2000’s, formal data validation started to become more wide-spread in the railways [10]. In particular, the ProB model-checker was first demonstrated during the EU project DEPLOY [13]. After some optimisations, ProB was able to fully handle large size metro data and validation rules, resulting in the generation of one B machine per validation rule and instantiated with the data related to this rule. To date, the biggest B machine generated for data validation and analysed by ProB contains 10 Mloc. With Atelier B 4.3, ProB was added as an interactive command [12]. Its behaviour is similar to the predicate prover: it does not modify the goal, only trying to demonstrate it. It comes with a time limit (maximum duration) and the possibility to reduce the number of hypotheses by selecting those having one symbol in common with the goal. PRoB allows better handling of arithmetic goals and case-based proofs on reduced domains."</i> | |||
*[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> | *[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> | ||
*[https://openportal.isti.cnr.it/doc?id=people______::8e1a740ac10b66042af4f30812531d2d The 4SECURail approach to formalizing standard interfaces between signalling systems components, Belli et al.] <i>"ProB has been selected as the second target of the formal encoding because of its recognized role (Ferrari et al. 2020) in the field of formal railway-related modelling. It provides user-friendly interfaces, and allows LTL/CTL model checking, state-space exploration, state-space projections, and trace descriptions in the form of sequence diagrams"</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> | ||