Difference between pages "ADVANCE D3.2 Model Checking" and "Code Generation Activity"

From Event-B
(Difference between pages)
Jump to navigationJump to search
imported>Leuschel
 
imported>Andy
 
Line 1: Line 1:
== Overview ==
+
+== Development Repository ==+
{{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)
+
The SVN repository for development of the code generation plug-in including transformation rules is here
  
* Continuous improvements of constraint solving capabilities of ProB
+
svn+ssh://svn.ecs.soton.ac.uk/projects/deploy-exploratory/trunk/CodeGeneration
  
* Work towards full support of Theory Plug-in: Support for external and recursive functions, translator, (work in progress)
+
=== Completed/Ongoing Work ===
 +
* Investigate Epsilon/ETL/EGL or ATL
 +
** Resulted in the choice of ETL for Model2Model Transformations
 +
** Choice for Model2Text is not concluded.
 +
* Experiment 1: Event-B Tasking to IL1 in ETL (main)
 +
** Nearly ready for experiments [4 May 2010]
 +
* Experiment 2: IL1 to text with EGL: ??
 +
** Not started
  
* Finish conversion to Kodkod, experiments with Kodkod and SMT translators
+
=== Metamodels ===
 +
* Tasking Metamodel - one for both single and multi-tasking?
 +
* Intermediate Language Metamodels based on Ada
 +
** Initial Version is IL1
 +
** Ready for experiments subject to decomposition. 
  
* Maybe: initial work on physical units supprt
+
* Metamodel re-structuring; will decompose into:
 +
** Algorithmic structures
 +
** Math. language
  
== Motivations / Decisions ==
+
=== Translation Rules ===
{{TODO|Fill this paragraph.}}
+
* Tasking Metamodel to IL1 translation rules [[http://wiki.event-b.org/images/Translation.pdf]]
 +
** Ready for experiments [4 May 2010] subject to decomposition into:
 +
*** Algorithmic structures
 +
*** Math. language
 +
*** Versions for Shared/Non-shared data
  
=== Improvements to Constraint-Solving ===
+
=== TODO ===
  
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.
+
* Control flow modelling assistant
It is thus important to improve this aspect of ProB.
+
* Infrastructure plugin
In particular, we have continuously improved the performance of the kernel, as can be seen in the figure showing the [[Image:performance of ProB on the N-Queens problem for 100 queens]].
+
* Initial version of:
Other improvements lie in better expansion of universal and existential quantifiers, reification for the the <tt>bool</tt> operator and support for infinite and recursive functions.
+
** IL1 to Ada backend plugin
The latter is particularly important in light of the Theory Plug-In work below.
+
* Small experiments: several small models, reader/writer, heater control, circular buffer
 
 
=== 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 ProB 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 support floats or reals, which will be important for certain cyber-physical systems.
 
 
 
On the technical side, we have extended the ProB internal representation of predicates and expressions to support the theory plug-in. As soon as the theory plug-in allows ProB to access the definitions (this is not yet implemented in the theory plug-in) we will finalize the implementation.
 
 
 
=== 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.
 
[http://bddbddb.sourceforge.net/ 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 [http://bddbddb.sourceforge.net/ 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 [http://bddbddb.sourceforge.net/ 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.}}
 
 
 
=== Constraint Solving ===
 
 
 
The improvements are available in the nightly builds of ProB.
 
 
 
Two specific pages have been added to the ProB user manual:  <ref>http://www.stups.uni-duesseldorf.de/ProB/index.php5/Recursively_Defined_Functions Recursive functions entry in ProB user manual</ref>,  <ref>http://www.stups.uni-duesseldorf.de/ProB/index.php5/External_Functions External functions entry in ProB user manual</ref>.
 
 
 
=== TLA2B ===
 
The TLA+ to B translation has been published at the iFM'2012 conference. A technical report is available<ref>http://www.stups.uni-duesseldorf.de/w/Special:Publication/HansenLeuschelTLA2012 Translating TLA+ to B for Validation with ProB. Technical Report, 2012.</ref>
 
A presentation at the FM'2012 TLA+ workshop will also be made.
 
A page has been added to the ProB user manual: <ref>http://www.stups.uni-duesseldorf.de/ProB/index.php5/TLA TLA2B entry in ProB user manual</ref>.
 
 
 
=== 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 <ref>http://www.stups.uni-duesseldorf.de/w/Special:Publication/PlaggeLeuschel_Kodkod2012 Validating B,Z and TLA+ using ProB and Kodkod. Technical Report, 2012.</ref> The paper has been accepted for FM'2012.
 
 
 
== Planning ==
 
{{TODO|Fill this paragraph.}}
 
 
 
== References ==
 
<references/>
 
 
 
[[Category:ADVANCE D3.2 Deliverable]]
 

Revision as of 11:09, 7 May 2010

+== Development Repository ==+

The SVN repository for development of the code generation plug-in including transformation rules is here

svn+ssh://svn.ecs.soton.ac.uk/projects/deploy-exploratory/trunk/CodeGeneration

Completed/Ongoing Work

  • Investigate Epsilon/ETL/EGL or ATL
    • Resulted in the choice of ETL for Model2Model Transformations
    • Choice for Model2Text is not concluded.
  • Experiment 1: Event-B Tasking to IL1 in ETL (main)
    • Nearly ready for experiments [4 May 2010]
  • Experiment 2: IL1 to text with EGL: ??
    • Not started

Metamodels

  • Tasking Metamodel - one for both single and multi-tasking?
  • Intermediate Language Metamodels based on Ada
    • Initial Version is IL1
    • Ready for experiments subject to decomposition.
  • Metamodel re-structuring; will decompose into:
    • Algorithmic structures
    • Math. language

Translation Rules

  • Tasking Metamodel to IL1 translation rules [[1]]
    • Ready for experiments [4 May 2010] subject to decomposition into:
      • Algorithmic structures
      • Math. language
      • Versions for Shared/Non-shared data

TODO

  • Control flow modelling assistant
  • Infrastructure plugin
  • Initial version of:
    • IL1 to Ada backend plugin
  • Small experiments: several small models, reader/writer, heater control, circular buffer