User:Nicolas/Collections/ADVANCE D3.4 Model Checking: Difference between revisions
imported>Leuschel |
imported>Leuschel |
||
| Line 37: | Line 37: | ||
* Support for the analysis of units throughout refinement relations. | * Support for the analysis of units throughout refinement relations. | ||
* Support for abstract units like "length" that can later be concretised to standard SI units. | * 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}} | {{TODO}} | ||
Revision as of 12:21, 20 October 2014
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 [1].
LTL Fairness
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[2] 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[3] to document known bugs, workarounds and feature requests.
TODO
Conclusion
TODO
