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.

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.

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.

Links for TLA+ to B Translation:

• A technical report has been published on the extension of ProB for TLA+ by translating it to B The paper has been accepted for iFM'2012.

Links for ProB Kodkod Integration:

• 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.