PredicateB: un animateur de prédicats

25 mars 2013

PredicateB a été créé par ClearSy en 2005, afin de calculer des prédicats exprimés en utilisant le langage mathématique de la méthode formelle B. PredicateB a été initialement développé en Java et fait partie du framework Rodin hébergé sur sourceforge.

Une nouvelle version de PredicateB, PredicateB++, a été développée en 2008 en C++ sur les bibliothèques Qt, dans le but d’améliorer considérablement les performances.

PredicateB a été utilisé pour le développement de Brama (un animateur de modèle Event-B plugin de la plateforme Rodin) et d’Ovado (un outil de validation de données ferroviaires, propriété de la RATP et destiné à la qualification de logiciels critiques pour la sécurité).

PredicateB++ a été utilisé pour le développement de DTVT (un outil de validation de données ferroviaires, propriété d’Alstom et utilisé comme outil d’ingénierie lors du développement de logiciels critiques). Ses capacités ont été légèrement améliorées en termes de performances et d’encombrement mémoire.