Links

Books

• The B-Book: Assigning programs to meanings, by Jean-Raymond Abrial (link is to a review by Jonathan Bowen)
• The B-Method: An Introduction, by Steve Schneider
• Modeling in Event-B: System and Software Engineering, by Jean-Raymond Abrial (the Bee book)

Papers

• ProB Publications
• B-Method in Wikipedia
• B-Method Site from ClearSy
• Can FM tools manage large scale industrial problems ?
• Data Validation

ProB

• Examples for ProB (along with screenshots and explanations)
• Old web page of ProB (in Southampton; use for releases prior to 1.2)
• Link to Success Story (written by Cetic)

Tools using ProB

• SafeCap
• DTVT - Data Table Validation Tool
• iUML Statemachines
• MultiSimulation Plug-In for Rodin
• Beta
• HRemo (see PhD thesis)
• Message Choreography Model Animation and Test Case Generation (see PhD thesis; Chapters 5 and 6)
• B4MSecure
• VTG (Vulnerability Test Generator, see Rodin Workshop 2012 presentation and 2014 presentation)
• There is also some intitial effort to use ProB for implicit VDM specifications presented at the 12th Ouverture Workshop.
• BEval

Related Tools

• Atelier B
• Event-B and Rodin Wiki (Platform Releases, Documentation), Rodin Sourceforge Site
• jbtools
• B4Free tools for the development of B models
• Click n Prove
• B Toolkit
• U2B UML to B translation tool
• TLA+ (tools for TLA+)
• The fuzz type-checker for Z
• The FDR3 CSP refinement checker

Testimonials

• 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).