User:Nicolas/Collections/ADVANCE D3.4 Model Checking

Overview

TODO

Motivations / Decisions

B to TLA+

We are interested in validating the correctness of our translation from B to TLA+. Hence, we have conducted extensive tests to validate our approach. For example, we use a range of models encoding mathematical laws to stress test our translation. These have proven to be very useful for detecting bugs in our translation and libraries. In addition, we have uncovered a bug in the model checker TLC. Moreover, we use a wide variety of benchmarks, checking that ProB and TLC produce the same result and generate the same number of states.

The current version of our translator covers almost all operators of a abstract B machine. Moreover, TLC can be used to validate liveness properties (LTL formulas) for B specifications under fairness conditions. Our approach has been published at the ABZ’2014 conference in Toulouse. A technical report is available .

LTL Fairness

Fairness is a notion where the search for counterexamples is restricted to paths that do not ignore infinitely the execution of a set of enabled actions imposed by the user as fair constraints. One possibility to set fairness constraints in ProB is to encode them in the LTL^e formula intended to be checked. For example, for a given LTL^e formula "f" a set of weak fairness conditions {e1,…,en} (where e1,...,en are some events) can be given as follows:

(FG e(e1) => GF [e1]) & … & (FG e(en) => GF [en]) => f.

In a similar way, strong fairness constraints can be imposed expressed by means of an LTLe formula:

(GF e(e1) => GF [e1]) & … & (GF e(en) => GF [en]) => f.

Checking fairness in this way is very often considered to be inefficient as usually the number of atoms (the possible valuations of the property) of the LTL property is exponential in the size of the formula. [1] ,

For this reason, the search algorithm of the LTL model checker in ProB has been extended in order to allow fairness to be checked efficiently. In addition, new operators have been added to the ProB’s LTL parser for setting fairness constraints to an LTL^e property. The new operators are WF(-) and SF(-) and both accept as argument an operation. The fairness constraints must be given by means of implication: "fair => f", where "f" is the property to be checked and "fair" the fairness constraints.

In particular, "fair" can have one of the forms: "wfair", "sfair", "wfair & sfair", and "sfair & wfair", where "wfair" and "sfair" represent the imposed weak and strong fairness constraints, respectively.

Basically, "wfair" and "sfair" are expressed by means of logical formulas having the following syntax: Weak fair conditions ("wfair"): `WF(a)`, where `a` is an operation `&` and `or`: conjunction and disjunction Strong fair conditions ("sfair"): `SF(a)`, where `a` is an operation `&` and `or`: conjunction and disjunction

More information on setting fairness to LTL formulas and the LTL Model Checker is available on the ProB User Manual website .

Theory Support

Theory Support was relevant for a variety of case studies, and is relevant for simulation, model checking and proving. We ensured that the Disprover also works with theories We have also improved the constraint propagation of the ProB kernel for records and freetypes, which are used to represent Event-B inductive datatypes. (As a side note, this feature is also being used by another EU project to use ProB for validating VDM specifications within the Ouverture tool). Finally, the treatment of recursive functions within the ProB kernel has been improved, also in light of dealing with recursive operators of Event-B Theories.

Physical Units

The physical units analysis has been further stabilised, several reported bugs have been fixed. Support for physical units has been extended to theories along with the general theory-related improvements of ProB mentioned in the previous paragraph. The plug-in was ported to Rodin 3, all bugfixes and changes could be back ported to Rodin 2 successfully.

Further extension to the unit analysis include:

• Support for the analysis of units throughout refinement relations.
• Support for abstract units like "length" that can later be concretised to standard SI units.

Performance Improvements Various performance improvements have been made to the model checker and animator for Event-B models, both in terms of memory consumption and speed. For example, the Event-B model of the Early parser by JR Abrial is now running an order of magnitude faster than before the beginning of the project.

TODO

Available Documentation

ProB
The ProB Website is the place where we collect information on the ProB toolset. There are several tutorials on ProB available in the User manual section. We also supply documentation on extending ProB for developers.

In addition we run a bug tracking system to document known bugs, workarounds and feature requests.

TODO

Conclusion

TODO