From Software Specifications to Constraint Programming

Non-deterministic specifications play a central role in the use of formal methods for software development. Such specifications can be more readable, but hard to execute efficiently due to the usually large search space. Constraint programming offers advanced algorithms and heuristics for solving certain non-deterministic models. Unfortunately, this requires writing models in a form suitable for efficient solving where the readability typically required from a specification is lost. Tools like ProB attempt to bridge this gap by translating high-level first-order predicate logic specifications into formal models suitable for constraint solving. In this paper we study potential improvements to this methodology by (1) using refinement to transform specifications into models suitable for efficient solving, (2) translating first-order predicates directly into the OscaR framework and (3) using different kinds of solvers as a back end. Formal verification by proof ensures the correctness of the solution of the model with respect to the specification.