From Animation to Data Validation: The ProB Constraint Solver 10 Years On


Various solvers are linked via reification and Prolog co-routines. The overall challenge of ProB is to solve constraints in full predicate logic with arithmetic, set theory and higher-order relations and functions for safety critical applications. In addition to the tool development, this chapter provides details about various industrial applications of the tool as well as the efforts in qualifying the tool for usage in safety critical contexts. It describes the experiences in applying alternate approaches, such as Systematic Approach to Training (SAT) or Satisfiability Modulo Theories (SMT). The B-method is a formal method for specifying safety critical systems, reasoning about those systems and generating code that is correct by construction. The ProB kernel can be viewed as a constraint solver for the basic datatypes of B and the various operators on it. It supports Booleans, integers, user-defined base types, pairs, records and inductively: sets, relations, functions and sequences.

In Formal Methods Applied to Complex Systems: Implementation of the B Method