PredicateB: a predicate animator

23 March 2013

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.

PredicateB has been used for the development of Brama (an Event-B model animator plugin of the Rodin platform) and Ovado (a railways data validation tool, property of RATP and aimed at safety critical software qualification).

PredicateB++ has been used for the development of DTVT (a railways data validation tool, property of Alstom and used as an engineering tool while developing safety critical software). Its capabilities have been slightly improved in term of performances and memory footprint.