Links: Difference between revisions

 
(41 intermediate revisions by 2 users not shown)
Line 1: Line 1:
== Books ==
== Books and Resources on B ==
* [http://www.jpbowen.com/publications/thes-b.html The B-Book: Assigning programs to meanings, by Jean-Raymond Abrial] (link is to a review by Jonathan Bowen)
* [https://doi.org/10.1017/CBO9780511624162 The B-Book: Assigning programs to meanings, by Jean-Raymond Abrial]
* [http://www.palgrave.com/science/computing/schneider/ The B-Method: An Introduction, by Steve Schneider]
* [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 ==
* [http://www.stups.uni-duesseldorf.de/w/Publications:ProB ProB Publications]  
* [https://www.cs.hhu.de/lehrstuehle-und-arbeitsgruppen/softwaretechnik-und-programmiersprachen/publikationen ProB Publications]  
* [http://en.wikipedia.org/wiki/B-Method B-Method in Wikipedia]  
* [http://en.wikipedia.org/wiki/B-Method B-Method in Wikipedia]  
* [http://www.bmethod.com/ B-Method Site] from ClearSy
* [http://www.bmethod.com/ B-Method Site] from ClearSy
Line 12: Line 15:


== ProB ==
== ProB ==
* [[ProB for Railways]]
* [[ProB History]]
* [[ProB Examples|Examples for ProB]] (along with screenshots and explanations)
* [[ProB Examples|Examples for ProB]] (along with screenshots and explanations)
* [http://www.ecs.soton.ac.uk/~mal/systems/prob.html Old web page of ProB] (in Southampton; use for releases prior to 1.2)
* [http://www.ecs.soton.ac.uk/~mal/systems/prob.html Old web page of ProB] (in Southampton; use for releases prior to 1.2)
Line 18: Line 23:


== Tools using ProB ==
== Tools using ProB ==
* [https://www.clearsy.com/en/our-tools/clearsy-data-solver/ ClearSy Data Solver]
* [http://www.data-validation.fr/data-validation-in-the-railways/ DTVT - Data Table Validation Tool] for Alstom by ClearSy
* OLAF data validation tool by ClearSy for Alstom and SNCF
* Dave data validation tool by ClearSy for General Electric Transportation
* [https://github.com/plues/plues PLUES] tool for university course validation
* [https://github.com/plues/plues PLUES] tool for university course validation
* [http://safecap.cs.ncl.ac.uk/index.php/Safecap_Project_Wiki SafeCap]
* [https://github.com/Joshua27/BSynthesis BSynthesis] tool for repair and generation  of formal models
* [http://www.data-validation.fr/data-validation-in-the-railways/ DTVT - Data Table Validation Tool]
* [https://safecap.co.uk SafeCap]
* [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]
* [http://www.macs.hw.ac.uk/~mtl4/Publications.html HRemo (see PhD thesis)]
* [https://www.ros.hw.ac.uk/handle/10399/2685  HRemo (see chapter 4 of PhD thesis)]
* [http://dx.doi.org/10.14279/depositonce-2502 Message Choreography Model Animation and Test Case Generation (see PhD thesis; Chapters 5 and 6)] [http://link.springer.com/article/10.1007%2Fs10270-012-0272-x SSM article (2014)]
* [http://dx.doi.org/10.14279/depositonce-2502 Message Choreography Model Animation and Test Case Generation (see PhD thesis; Chapters 5 and 6)] [http://link.springer.com/article/10.1007%2Fs10270-012-0272-x SSM article (2014)]
* [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://blog.aymericksavary.fr/?page_id=209 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])
* [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])
* CODA [https://arxiv.org/abs/1305.6112v1 arXiv article]
* CODA [https://arxiv.org/abs/1305.6112v1 arXiv article]
* There is also some intitial effort to [http://pure.au.dk/portal/en/publications/interpreting-implicit-vdm-specifications-using-prob(19de7f9f-1d9a-483c-b2e7-285c0d0edc63).html use ProB for implicit VDM specifications] presented at [http://wiki.overturetool.org/index.php/12th_Overture_Workshop the 12th Ouverture Workshop].
* There is also some intitial effort to [http://pure.au.dk/portal/en/publications/interpreting-implicit-vdm-specifications-using-prob(19de7f9f-1d9a-483c-b2e7-285c0d0edc63).html use ProB for implicit VDM specifications] presented at [http://wiki.overturetool.org/index.php/12th_Overture_Workshop the 12th Ouverture Workshop].
Line 37: Line 48:
* [http://bibbase.org/network/publication/lausdahl-ishikawa-larsen-interpretingimplicitvdmspecificationsusingprob-2015 Animating implicit VDM specifications inside Ouverture]
* [http://bibbase.org/network/publication/lausdahl-ishikawa-larsen-interpretingimplicitvdmspecificationsusingprob-2015 Animating implicit VDM specifications inside Ouverture]
* [http://www.ovado.net Ovado] (as second tool chain)
* [http://www.ovado.net Ovado] (as second tool chain)
* [https://github.com/tofische/cucumber-event-b Cucumber-Event-B] tool to run high-level tests


== Related Tools ==
== Related Tools ==
Line 42: Line 54:
* [http://www.event-b.org/ Event-B and Rodin Wiki] ([http://wiki.event-b.org/index.php/Rodin_Platform_Releases Platform Releases], [http://wiki.event-b.org/index.php/Main_Page  Documentation]), [http://sourceforge.net/projects/rodin-b-sharp/ Rodin Sourceforge Site]
* [http://www.event-b.org/ Event-B and Rodin Wiki] ([http://wiki.event-b.org/index.php/Rodin_Platform_Releases Platform Releases], [http://wiki.event-b.org/index.php/Main_Page  Documentation]), [http://sourceforge.net/projects/rodin-b-sharp/ Rodin Sourceforge Site]
* [https://github.com/utwente-fmt/ltsmin/releases LTSmin releases (including versions for prob)]
* [https://github.com/utwente-fmt/ltsmin/releases LTSmin releases (including versions for prob)]
* [http://lifc.univ-fcomte.fr/~btatibouet/PERSO/JBTOOLS/InstallPlugIn/InstallPlugIn.html jbtools]
* [http://www.b4free.com/ B4Free] tools for the development of B models
* [http://www.b4free.com/ B4Free] tools for the development of B models
* [http://www.loria.fr/~cansell/cnp.html Click n Prove]
* [https://hal.archives-ouvertes.fr/inria-00099836 Click n Prove]
* [https://github.com/edwardcrichton/BToolkit B Toolkit]
* [https://github.com/edwardcrichton/BToolkit B Toolkit]
* [http://www.ecs.soton.ac.uk/~cfs/umlb.html U2B] UML to B translation tool
* [http://www.ecs.soton.ac.uk/~cfs/umlb.html U2B] UML to B translation tool
* [http://research.microsoft.com/en-us/um/people/lamport/tla/tla.html TLA+] ([http://research.microsoft.com/en-us/um/people/lamport/tla/tools.html tools for TLA+])
* [http://research.microsoft.com/en-us/um/people/lamport/tla/tla.html TLA+] ([http://research.microsoft.com/en-us/um/people/lamport/tla/tools.html tools for TLA+])
* [https://spivey.oriel.ox.ac.uk/mike/fuzz/ The fuzz type-checker for Z]
* [https://spivey.oriel.ox.ac.uk/corner/Fuzz_typechecker_for_Z The fuzz type-checker for Z]
* [https://www.cs.ox.ac.uk/projects/fdr/ The FDR3 CSP refinement checker]
* [https://www.cs.ox.ac.uk/projects/fdr/ The FDR CSP refinement checker]
* [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://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 62: Line 76:
* 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]: <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 ==


* [https://github.com/klar42/railground/ Railground Event-B Model]
* [https://github.com/klar42/railground/ Railground Event-B Model]
* [https://www.irit.fr/EBRP/ EBRP Project]


== Translating to Logic ==
== Translating to Logic ==
Line 72: Line 91:
* [http://pages.cs.wisc.edu/~dyer/cs540/notes/fopc.html Lecture Notes on Translating to First-Order Logic]
* [http://pages.cs.wisc.edu/~dyer/cs540/notes/fopc.html Lecture Notes on Translating to First-Order Logic]
* [http://cs.nyu.edu/faculty/davise/guide.html Guide to Axiomatizing in First-Order Logic]
* [http://cs.nyu.edu/faculty/davise/guide.html Guide to Axiomatizing in First-Order Logic]
== General ==
* [[Privacy Policy|Privacy Policy (Datenschutz)]]

Latest revision as of 08:03, 8 August 2023

Books and Resources on B

Papers

ProB

Tools using ProB

Related Tools

Testimonials

  • The 4SECURail Formal Methods Demonstrator, Franco Mazzanti and Dimitri Belli ""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."
  • The 4SECURail approach to formalizing standard interfaces between signalling systems components, Belli et al. "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"
  • Data validation at Siemens, Jérôme Falampin: ""The work done with ProB is a great success. Thanks to the automatization and ProB, the wayside data validation is quicker, easier and complete." More details and academic papers can be found on our page Siemens Data Validation with ProB.
  • Pacemaker model by Mery and Singh: "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."
  • Reverse engineering using ProB at ClearSy: "Data validation principles have been applied recently to a railways reverse-engineering project with great success. B and ProB have demonstrated again how efficient they are when used in combination."..."This problem was solved elegantly by using data validation principles: a B model representing the two graphs and their properties were elaborated, and ProB used for finding a solution."
  • Safecap tool paper by Iliasov, Lopatkin and Romanovsky: "One of the larger examples we have tackled is the Carlisle Citadel station with the North, South, and Caldew junctions. The modelled fragment is 2.6km long and comprises 70 train detection circuits, 63 points, 79 routes and 161 valid paths. The translation from a scanned PDF drawing and printed control tables took 45 man-hours. The verification of the topology theory constraints using ProB took just over 6 minutes on a PC with i7 3730 CPU and utilized just under 2GB of RAM. The Why3 verification of the same theory takes approximately 70 minutes. The control table theory is verified under 20 seconds by ProB and not verified completely, with the current translation of conditions, using Why3."
  • Innovative Approach for Requirements Verification of Closed Systems by Reis, Bicknell, Butler, Colley: "The Event-B model can be animated within Rodin using the BMotion Studio tool, which is part of ProB. Using the tool, it is possible to generate an animated front-end to the simulation of the model in the form of a user-friendly graphical interface, which corresponds to the system’s GUI (see Figure 4). The user can interact directly with this animated front-end, while the tool continues to run the formal analysis in the background, reacting to user choices and checking the model and invariants at each step. This was utilised during the case study, to produce a representation of the GIU provided as part of the end-user system. As this graphical representation is tied to the underlying Event-B model, it can not only be used to run through the model and confirm that the model is the correct representation of the system, but can also be used to explore further scenarios. This graphical representation of the system can be used without necessarily requiring any experience with the Event-B language or the toolset."
  • ProZ for Modelling Safety Properties of Interactive Medical Systems by Bowen and Reeves: "In this paper we have shown how temporal logic and invariants describing safety properties of interactive medical devices can be investigated within the ProZ tool. We have given examples of checking for such properties against a model of the T34 syringe pump and discussed some of the results and challenges we have encountered using this approach. We believe that using techniques such as these, and other model-checking functionalities, contributes to supporting safer use of interactive medical devices. That is we can use such techniques not just to help develop better and safer systems (where such techniques are most typically used) but also, as we have shown here, to investigate existing devices to ensure they can be safely used within the clinical setting."
  • 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 Thales slides of the Advance Industry Day 2014 ProB has a high technology readiness level (TRL).
  • ProB 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)
  • Analysis and formal specification of relay-based railway interlocking systems: "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."
  • Generating and Verifying Configuration Data with OVADO: "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."
  • Applying B and ProB to a Real-world Data Validation Project: 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. ... 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.
  • Xtend Transformation from PDDL to Event-B: 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.

Other Links

Translating to Logic

General