Difference between pages "D45 Model Checking" and "D45 Prover Enhancement"

From Event-B
(Difference between pages)
Jump to navigationJump to search
imported>Tommy
 
imported>Tommy
m
 
Line 1: Line 1:
 
= Overview =
 
= Overview =
−
 
+
Concerning the prover performance, two tasks were performed: the addition of rewriting and inference rules, and the addition of a mechanism to allow the customization and the parameterization or combination of tactics.
−
We have implemented various improvements to the model checking and constraint-solving components of ProB, most in reaction to issues arising in the industrial case studies.
+
* {{TODO}} An overview of the contribution about the new rewriting and inference rules (Laurent Voisin)
−
These improvements are described below.
+
* {{TODO}} An overview of the contribution about advanced Preferences for auto-tactics (Nicolas Beauger)  
−
+
* {{TODO}} An overview of the contribution about the ProB Disprover (Daniel Plagge, Jens Bendiposto)
−
== State Space Reduction, Compression and Hashing ==
+
* {{TODO}} An overview of the contribution about the SMT Solver Integration (Laurent Voisin)
−
 
 
−
Driven by a case study from the space sector (a protocol modeled by SSF), where memory consumption was an issue, we have investigated ways to reduce ProB's memory consumption.
 
−
A first step was to implement a first version of state compression, whereby we simplify stored states so that they require less memory. This was achieved without compromising speed and is now always activated.
 
−
Furthermore, if the preference <tt>COMPRESSION</tt> is set to true, then ProB will also detect common (sub-)expressions in states and store the common expressions only once.
 
−
For example, when several states have the same same value for a given variable <tt>x</tt> then its value will only be stored just once. This is particularly useful when complicated variables only change infrequently.
 
−
 
 
−
Related to this aspect, the hashing of ProB states was improved on 64-bit architectures, which is also important in the context of detecting common subexpressions for sharing (common subexpressions are detected by hashing).
 
−
We have also implemented a cryptographic SHA1 hashing function for Prolog terms, but it is not yet used in the production version of ProB.
 
−
 
 
−
Finally, the most useful symmetry reduction technique of ProB is the so-called "hash marker" method.
 
−
Here, we have also improved the computation of the hash symmetry markers, both achieving a reduction in size and runtime.
 
−
 
 
−
== Constraint-Based Checking ==
 
−
 
 
−
Improved Constraint-based checking for deadlocks, invariants and event sequences (used in MBT).
 
−
In addition, many improvements in constraint solving kernel were implemented.
 
−
 
 
−
== New Features ==
 
−
=== Experiments with Theory Plugin ===
 
−
 
 
−
Animating models that use the Theory plug-in is currently not possible. However, we prepared ProB's translation from Event-B into its internal representation in order to support user defined operators from the Theory plug-in. The work on the feature is currently suspended until the Theory plug-in supports accessing the definitions.
 
−
 
 
−
=== Improved detection of infinite functions, and improved support for them===
 
−
 
 
−
 
 
−
ProB now detects much better when comprehension sets or lambda abstractions are infinite. In this case the set or function is kept symbolic and evaluated on demand.
 
−
 
 
−
In that light, ProB now also keeps track when an infinite set had to be approximated by a finite one and emits a warning.
 
−
For example, given a predicate <tt>!x.(x:NATURAL => x+1:NATURAL1)</tt>, ProB will check the quantified expression only for values of x from 0 to MAXINT.
 
−
These warnings are not yet displayed in the Rodin version, but are visible in probcli and ProB Tcl/Tk.
 
−
 
 
−
=== Support of finite operator===
 
−
 
 
−
The finite operator was previously ignored, as ProB only supported finite sets anyway.
 
−
Now, however, ProB can deal with certain infinite sets (in particular infinite functions such as <tt>%.x(x:INTEGER|x+1)</tt>), this could lead to wrong results.
 
−
ProB now supports the finite operator, and emits a warning if it cannot determine whether a comprehension set or lambda function is finite.
 
−
 
 
−
== Experiments ==
 
−
 
 
−
TLA+ and B share the common base of predicate logic, arithmetic and set theory.
 
−
We have conducted a translation of the non-temporal part of TLA+ to B, which makes it possible to feed TLA+ specifications into existing tools for B.
 
−
Part of this translation must include a type inference algorithm, in order to produce typed B specifications.
 
−
There are many other tricky aspects, such as translating modules as well as let and if-then-else expressions.
 
−
We also developed an integration of our translation into ProB.
 
−
ProB thus now provides a complementary tool to the explicit state model checker TLC, with convenient animation and constraint solving for TLA+.
 
−
More importantly for Deploy, we have conducted a series of case studies, highlighting the complementarity to TLC. In particular, we have highlighted the sometimes dramatic difference in performance when it comes to solving complicated constraints in TLA+. Also, the benchmarks have allowed us to pinpoint some areas where ProB could be further improved. This also led to some of the compression techniques mentioned earlier.
 
  
 
= Motivations =
 
= Motivations =
−
 
+
== New rewriting and inference rules ==
−
The motivations for the state space compression arose from experiments in WP3 (space), and from applications of ProB outside of Deploy.
+
{{TODO}} ''To be completed by Laurent Voisin''
−
 
+
== Advanced Preferences for Auto-tactics ==
−
The need for constraint-based deadlock checking arose in the automotive work package, more precisely during the elaboration of the cruise control system. Here, proving turned out to be impractical and ProB was used to find deadlocks and guide the development of the model.
+
{{TODO}} ''To be completed by Nicolas Beauger''
−
 
+
== Isabelle Plug-in ==
−
The work on infinite functions was motivated by models from the transportation section (WP2), where many models contained infinite functions encoding certain auxiliary computations.
+
{{TODO}} ''To be completed by Matthias Schmaltz''
 +
== ProB Disprover ==
 +
{{TODO}} ''Daniel Plagge, Jens Bendiposto''
 +
== SMT Solver Integration ==
 +
{{TODO}} ''Laurent Voisin''
  
 
= Choices / Decisions =
 
= Choices / Decisions =
−
 
+
== New rewriting and inference rules ==
−
Aggressive compression can also induce a performance penalty.
+
{{TODO}} ''To be completed by Laurent Voisin''
−
The new default mode was chosen such that there should be no performance penalty, with reduced memory usage.
+
== Advanced Preferences for Auto-tactics ==
−
(Indeed, the time for compression is regained by reduced time to store and retrieve the states.)
+
{{TODO}} ''To be completed by Nicolas Beauger''
−
 
+
== Isabelle Plug-in ==
−
A more aggressive setting can be forced by <tt>-p COMPRESSION TRUE</tt>. This will further reduce memory consumption, but may increase runtime (although quite often it does not).
+
{{TODO}} ''To be completed by Matthias Schmaltz''
 +
== ProB Disprover ==
 +
{{TODO}} ''Daniel Plagge, Jens Bendiposto''
 +
== SMT Solver Integration ==
 +
{{TODO}} ''Laurent Voisin''
  
 
= Available Documentation =
 
= Available Documentation =
−
 
+
* {{TODO}} Links for New rewriting and inference rules
−
* [http://www.stups.uni-duesseldorf.de/ProB/index.php5/Using_the_Command-Line_Version_of_ProB Command-Line Version of ProB]
+
* {{TODO}} Links for Advanced Preferences for Auto-tactics
−
* [http://www.stups.uni-duesseldorf.de/w/Special:Publication/HaLe2011 Constraint-Based Deadlock Checking of High-Level Specifications. In Proceedings ICLP'2011, Cambridge University Press, 2011.]
+
* {{TODO}} Links for Isabelle Plug-in
−
* [http://www.stups.uni-duesseldorf.de/w/Special:Publication/HansenLeuschelTLA2012 Translating TLA+ to B and experiments with TLC]
+
* {{TODO}} Links for ProB Disprover
 +
* {{TODO}} Links for SMT Solver Integration
  
 
= Status =
 
= Status =
−
 
+
== New rewriting and inference rules ==
−
All improvements, unless explicitly stated below, are accessible in the latest release of ProB.
+
{{TODO}} ''To be completed by Laurent Voisin''
−
For example, the improved hashing and light-weight state compression is available in the current release of ProB.
+
== Advanced Preferences for Auto-tactics ==
−
The SHA1 hash technique is not available in the current release.
+
{{TODO}} ''To be completed by Nicolas Beauger''
−
The research on further compression technique is ongoing and will be continued within the project ADVANCE[http://www.advance-ict.eu/].
+
== Isabelle Plug-in ==
−
The work on the Theory plug-in support is currently suspended until the Theory plug-in provides the features described earlier.
+
{{TODO}} ''To be completed by Matthias Schmaltz''
 +
== ProB Disprover ==
 +
{{TODO}} ''Daniel Plagge, Jens Bendiposto''
 +
== SMT Solver Integration ==
 +
{{TODO}} ''Laurent Voisin''
  
 
[[Category:D45 Deliverable]]
 
[[Category:D45 Deliverable]]

Revision as of 17:22, 18 November 2011

Overview

Concerning the prover performance, two tasks were performed: the addition of rewriting and inference rules, and the addition of a mechanism to allow the customization and the parameterization or combination of tactics.

  • TODO An overview of the contribution about the new rewriting and inference rules (Laurent Voisin)
  • TODO An overview of the contribution about advanced Preferences for auto-tactics (Nicolas Beauger)
  • TODO An overview of the contribution about the ProB Disprover (Daniel Plagge, Jens Bendiposto)
  • TODO An overview of the contribution about the SMT Solver Integration (Laurent Voisin)

Motivations

New rewriting and inference rules

TODO To be completed by Laurent Voisin

Advanced Preferences for Auto-tactics

TODO To be completed by Nicolas Beauger

Isabelle Plug-in

TODO To be completed by Matthias Schmaltz

ProB Disprover

TODO Daniel Plagge, Jens Bendiposto

SMT Solver Integration

TODO Laurent Voisin

Choices / Decisions

New rewriting and inference rules

TODO To be completed by Laurent Voisin

Advanced Preferences for Auto-tactics

TODO To be completed by Nicolas Beauger

Isabelle Plug-in

TODO To be completed by Matthias Schmaltz

ProB Disprover

TODO Daniel Plagge, Jens Bendiposto

SMT Solver Integration

TODO Laurent Voisin

Available Documentation

  • TODO Links for New rewriting and inference rules
  • TODO Links for Advanced Preferences for Auto-tactics
  • TODO Links for Isabelle Plug-in
  • TODO Links for ProB Disprover
  • TODO Links for SMT Solver Integration

Status

New rewriting and inference rules

TODO To be completed by Laurent Voisin

Advanced Preferences for Auto-tactics

TODO To be completed by Nicolas Beauger

Isabelle Plug-in

TODO To be completed by Matthias Schmaltz

ProB Disprover

TODO Daniel Plagge, Jens Bendiposto

SMT Solver Integration

TODO Laurent Voisin

Retrieved from ‘https://wiki.event-b.org/index.php?title=D45_Model_Checking&oldid=3105’