Category Archives: Tools

ProB is an animator and model-checker for the B-method. It can be used to systematically check a specification for range of errors. The constraint-solving capabilities of ProB can also be used for model finding, deadlock checking and test-case generation.

Prob is developed by the team of Michael Leuschel, University of Dusseldorf, while commercial support is provided by the spin-off company Formal Mind.

ProB is now being used within Siemens and Alstom for data validation of complicated properties.

PredicateB was created by ClearSy in 2005, in order to calculate predicates expressed using the mathematical language of the B formal method. PredicateB has been initially developped in Java and is part of the Rodin framework hosted on sourceforge.

A new version of PredicateB, PredicateB++,  has been developed in 2008 in C++ on top of Qt libraries, with the aim of significantly improving performances.

Continue Reading →