ADVANCE D3.2 Model Checking

Overview

TODO: Fill this paragraph.

• TLA to B conversion, support for TLA+ in ProB (motivation: TLA can deal with real numbers,...; extend reach of the project)

• Continuous improvements of constraint solving capabilities of ProB

• Work towards full support of Theory Plug-in: Support for external and recursive functions, translator, (work in progress)

• Finish conversion to Kodkod, experiments with Kodkod and SMT translators

• Maybe: initial work on physical units supprt

Motivations / Decisions

TODO: Fill this paragraph.

Kodkod

The motivation behind incorporating the relational logic solver "Kodkod" into ProB was to evaluate how other technologies can complement ProB's constraint solving capabilities. A tight integration into ProB makes it available as well for model checking, animation as well as for the disproving capabilities mentioned above. Our integration allows predicates from Event-B (and B, Z and TLA+ as well) to be solved using a mixture of SAT-solving and ProB's own constraint-solving capabilities developed using constraint logic programming: the first-order parts which can be dealt with by Kodkod and the remaining parts solved by the existing ProB kernel. We have conducted a first empirical evaluation and analyzed the respective merits of SAT-solving and classical constraint solving. We also compare to using SMT solvers via recently available translators for Event-B. Our experiments have shown that the translation can be highly beneficial for certain kinds of constraints, and as such opens up new ways to analyze and validate formal specifications in Event-B. However, the experiments have also shown that the constraint logic programming approach of ProB can be superior in a considerable number of scenarios; the translation to Kodkod and down to SAT is not (yet) the panacea. The same can be said of the existing translations from B to SMT. As such, we believe that much more research required to reap the best of both worlds (SAT/SMT and constraint programming). An interesting side-effect of our work is that the ProB toolset now provides a double-chain (relying on technology developed independently and using different programming languages and paradigms) of validation for first-order predicates, which should prove relevant in high safety integrity level contexts.

Available Documentation

TODO: Fill this paragraph.

Planning

TODO: Fill this paragraph.