(27 intermediate revisions by the same user not shown) | |||
Line 1: | Line 1: | ||
== Books == | == Books and Resources on B == | ||
* [ | * [https://doi.org/10.1017/CBO9780511624162 The B-Book: Assigning programs to meanings, by Jean-Raymond Abrial] | ||
* [ | * [https://www.amazon.de/-/en/Steve-Schneider/dp/033379284X/ The B-Method: An Introduction, by Steve Schneider] ((Cornerstones of Computing) ) | ||
* [http://www.event-b.org/abook.html Modeling in Event-B: System and Software Engineering, by Jean-Raymond Abrial] (the Bee book) | * [http://www.event-b.org/abook.html Modeling in Event-B: System and Software Engineering, by Jean-Raymond Abrial] (the Bee book) | ||
* [https://www3.hhu.de/stups/handbook/rodin/current/html/ Rodin Users' Handbook] | |||
* Atelier-B Reference Manual (available as part of the [[https://www.atelierb.eu/en/atelier-b-support-maintenance/download-atelier-b/ Atelier-B download]) | |||
* [https://mooc.imd.ufrn.br/course/the-b-method MOOC: The B-Method: from specification to code] | |||
== Papers == | == Papers == | ||
Line 27: | 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] | ||
* [https://link.springer.com/chapter/10.1007/978-3-031-21595-7_9 Capella Validation Tool] | |||
* [http://www.beta-tool.info/user_guide.html Beta] | * [http://www.beta-tool.info/user_guide.html Beta] | ||
* [https://www.ros.hw.ac.uk/handle/10399/2685 HRemo (see chapter 4 of PhD thesis)] | * [https://www.ros.hw.ac.uk/handle/10399/2685 HRemo (see chapter 4 of PhD thesis)] | ||
Line 34: | Line 39: | ||
* [http://b4msecure.forge.imag.fr B4MSecure] | * [http://b4msecure.forge.imag.fr B4MSecure] | ||
* [http://genisis.forge.imag.fr GenISIS] | * [http://genisis.forge.imag.fr GenISIS] | ||
* [http://vasco.imag.fr/tools/meeduse/ MEEDUSE] | |||
* [https://hal.archives-ouvertes.fr/hal-00981811 VTG] (Vulnerability Test Generator, see [http://blog.aymericksavary.fr/wp-content/uploads/2011/10/presentation.pdf Rodin Workshop 2012 presentation] and [http://blog.aymericksavary.fr/wp-content/uploads/2014/06/Présentation.pdf 2014 presentation]) | * [https://hal.archives-ouvertes.fr/hal-00981811 VTG] (Vulnerability Test Generator, see [http://blog.aymericksavary.fr/wp-content/uploads/2011/10/presentation.pdf Rodin Workshop 2012 presentation] and [http://blog.aymericksavary.fr/wp-content/uploads/2014/06/Présentation.pdf 2014 presentation]) | ||
* CODA [https://arxiv.org/abs/1305.6112v1 arXiv article] | * CODA [https://arxiv.org/abs/1305.6112v1 arXiv article] | ||
Line 58: | Line 64: | ||
* [https://github.com/leuschel/bbedit-prob BBedit Language modules for B, TLA+, CSP and Prolog] | * [https://github.com/leuschel/bbedit-prob BBedit Language modules for B, TLA+, CSP and Prolog] | ||
* [https://en.wikipedia.org/wiki/List_of_model_checking_tools Model checking tools] | * [https://en.wikipedia.org/wiki/List_of_model_checking_tools Model checking tools] | ||
* [https://accelconf.web.cern.ch/icalepcs2021/doi/JACoW-ICALEPCS2021-WEPV042.html PLCverif] (CERN) | |||
== 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://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> | ||
Line 68: | Line 79: | ||
* ProB has been used “out-of-the-box” for Rodin theories by Thales for railway interlocking models, building ProB BMotionStudio visualizations on top. According to the [http://www.advance-ict.eu/sites/www.advance-ict.eu/files/Thales-Duesseldorf.pdf Thales slides of the Advance Industry Day 2014] ProB has a high technology readiness level (TRL). | * ProB has been used “out-of-the-box” for Rodin theories by Thales for railway interlocking models, building ProB BMotionStudio visualizations on top. According to the [http://www.advance-ict.eu/sites/www.advance-ict.eu/files/Thales-Duesseldorf.pdf Thales slides of the Advance Industry Day 2014] ProB has a high technology readiness level (TRL). | ||
* ProB [http://smtcomp.sourceforge.net/2016/results-NIA.shtml?v=1467112059 wins the NIA (non-linear integer arithmetic) division of the 2016 SMT competition] (this is ProB out-of-the-box, without tuning and where SMT formulas are translated to B) | * ProB [http://smtcomp.sourceforge.net/2016/results-NIA.shtml?v=1467112059 wins the NIA (non-linear integer arithmetic) division of the 2016 SMT competition] (this is ProB out-of-the-box, without tuning and where SMT formulas are translated to B) | ||
* [https://tel.archives-ouvertes.fr/tel-03215450 Analysis and formal specification of relay-based railway interlocking systems]: < | * [https://tel.archives-ouvertes.fr/tel-03215450 Analysis and formal specification of relay-based railway interlocking systems]: <i>"In this work, the formal specification of the ITCS case study was verified with the use of ProB by model checking. Besides, we verified the same formal specification a second time with the Atelier B by theorem proving. Both tools were able to automatically prove the system without any human intervention. The result of this verification states that no error or inconsistencieshave been found. Thus, one may conclude that the system will not lead to a dangerous state."</i> | ||
* [https://link.springer.com/chapter/10.1007/978-3-031-05814-1_10 Generating and Verifying Configuration Data with OVADO]: <i>"The second chain first produces a B abstract machine gathering data values and rules modeled as B properties and then calls the B model-checker ProB to evaluate the rules."</i> | |||
* [https://ieeexplore.ieee.org/document/9755408 Applying B and ProB to a Real-world Data Validation Project]: <i>In this paper, we present our experiences on applying B language and ProB tool to validate the correctness of the part of the section topology of Tram Line 1 of Guangzhou Huangpu in China.</i> ... <i>ProB is used to validate the correctness of the assertions, which is equivalent to checking that the data meet the rules. The validated topology improved the functional correctness of the tram control system.</i> | |||
* [https://link.springer.com/chapter/10.1007/978-3-031-16014-1_50 Xtend Transformation from PDDL to Event-B]: <i>Through the use of ProB animator, we can validate plan solutions. Unlike the VAL tool associated with PDDL, the animation with ProB allows locating errors of an incorrect plan solution.</i> | |||
== Other Links == | == Other Links == |