ProB: un model-checker pour la validation de données

26 mars 2013

ProB est un animateur et un vérificateur de modèles pour la méthode B. Il peut être utilisé pour vérifier systématiquement une spécification pour les erreurs de gamme. Il peut être utilisé pour vérifier systématiquement une gamme d’erreurs dans une spécification. Les capacités de résolution de contraintes de ProB peuvent également être utilisées pour la recherche de modèles, la vérification d’impasses et la génération de cas de test.

ProB est développé par l’équipe de Michael Leuschel, de l’université de Düsseldorf, tandis que le soutien commercial est assuré par l’entreprise dérivée Formal Mind.

ProB est actuellement utilisé par Siemens et Alstom pour la validation des données de propriétés complexes.