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.

Improvements to Constraint-Solving

ProB's constraint solving capabilities are at the core of many of ProB's features: animation of high-level models with complicated predicates, model-based testing, constraint-based invariant and deadlock checking, etc. It is thus important to improve this aspect of ProB. The support for infinite and recursive functions is particularly important, also in light of the Theory Extension work below.

TLA2B

TLA+ and B share the common base of predicate logic, arithmetic and set theory. However, there are still considerable differences, such as very different approaches to typing and modularization. Some features of TLA+ are interesting in the context of cyber-physical systems, such as real numbers. There is also considerable difference in the available tool support. In particular, we wanted to compare ProB with TLC and gain insights about performance.

Physical Units

Formal models of cyber physical systems will contain variables which represent values with physical units. We are thus exploring to use the ProB model checker as a tool to infer and validate physical units usage in formal models. In particular, we want to make sure that the physical units in a model are used in a consistent way.

Theory Plug-in and Mathematical Extensions

In the core, we have improved ProB to better deal with infinite and recursive functions. This can be used to provide formal specifications for mathematical extensions which can be animated and model checked by ProB.

Using the newly developed external function mechanism, it should also be possible to implement floats or reals, which will be important for certain cyber-physical systems.

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.

Before starting our translation to Kodkod, we had experimented with several other alternate approaches to solve constraints in ProB. bddbddb offers the user a Datalog-like language that aims to support program analysis. It uses BDDs to represent relations and compute queries on these relations. In particular, one has to represent a state of the model as a bit-vector and events have to be implemented as relations between two of those bit-vectors. These relations have to be constructed by creating BDDs directly with the underlying BDD library (JavaBDD) and storing them into a file. Soon after starting experimenting with bddbddb it became apparent that due to the lack of more abstract data types than bit vectors, the complexity of a direct translation from B to bddbddb was too high, even for small models, and this avenue was abandoned.

SAL is a model-checking framework combining a range of tools for reasoning about systems. The SAL tool suite includes a state of the art symbolic (BDD-based) and bounded (SAT-based) model checkers. Some first results were encouraging for a small subset of the Event-B language, but the gap between B and SAL turned out to be too big in general and no realistic way was found to handle important B operators.

Kodkod has the advantage that is provides good support for relations and sets which play an essential role in Event-B's mathematical notation.

Available Documentation

TODO: Fill this paragraph.

TLA2B

The TLA+ to B translation has been published at the iFM'2012 conference. A technical report is available A presentation at the FM'2012 TLA+ workshop will also be made.

Physical Units

This work is still in progress. Full documentation will be made available later in the project. The latest nightly build of ProB contains an experimental version of the analysis.

Kodkod

A technical report has been published on the validation using ProB and Kodkod The paper has been accepted for FM'2012.

Planning

TODO: Fill this paragraph.