We are pleased to inform you that Atelier B 4.3.1 is available for download. It is exclusively reserved for maintenance holders, and is accessible from the account page.
This version contains 27 fixes and two new features: a new prover based on the ProB tool and the B Coding Rule Checker.
The integration of the ProB model-check (from the Heinrich-Heine University) provides a new proving capability similar to the existing Predicate Prover but with the capacity to find counter examples in the analyzed formula.
The new BCRC tool (B Coding Rule Checker) was developed with the support of Alstom. It provides the ability to check the conformance of a model versus a set of coding rules. For instance, those rules can precise if a special prefix or suffix must be present on operation argument, or can precise the set of allowed operators or substitutions for a particular project. The results of the analysis can be displayed directly in Atelier B for examination or correction, or can be exported to a document.
For further information, please check out the version release note