D45 Prover Enhancement: Difference between revisions
imported>Leuschel |
imported>Tommy |
||
(56 intermediate revisions by 2 users not shown) | |||
Line 1: | Line 1: | ||
= Overview = | = Overview = | ||
Two tasks concerned the prover performance from the core platform: the addition of rewriting and inference rules, and the addition of a mechanism to allow the customization and the parametrization or combination of tactics. While the addition of rewriting and inference rules has always been a regular task to enhance the Rodin integrated prover during DEPLOY lifetime, a new way to manage tactics has been implemented. In fact, the user is now able to define various types of tactics called 'profiles' which could be customized and parameterized tactics to discharge some specific proof obligations.<br> | |||
The ProB plug-in allows to find and visualize counter examples to the invariant and deadlock preservation proof obligations. ProB has also been used for finding count examples to proof rules of the industrial partner Siemens.<br> | |||
The SMT Solvers plug-in allowing to use the SMT solvers within Rodin is an effective alternative to the Atelier-B provers, particularly when reasoning on linear arithmetic.<br> | |||
The Isabelle/HOL integration plug-in allows to extend the Rodin proving capabilities through the definition of tactic written in Isabelle/HOL and thus, provides help to automatically discharge proof obligations, but also allows the verification of the new extensions of the Rodin sequent prover written in java through the translation of their corresponding rules. | |||
= Motivations = | = Motivations = | ||
== New rewriting and inference rules == | == New rewriting and inference rules == | ||
In an Event-B development, more than 60% of the time is spent on proofs. It has been a continuous aim to increase the number of automatically discharged proof obligations (POs) by improving the capabilities of the integrated sequent prover through the addition of rewriting and inference rules. These rules were provided through tactics, or existing or newly created. These tactics were automatic, or manual, or sometimes both. Providing new proving rules, even if it sometimes does not increase directly the number of automatically discharged POs aims to help the user to interactively discharge them and spare his time. | In an Event-B development, more than 60% of the time is spent on proofs. It has been a continuous aim to increase the number of automatically discharged proof obligations (POs) by improving the capabilities of the integrated sequent prover through the addition of rewriting and inference rules. Naturally all of the industrial partners in DEPLOY are keen for the proofs to be as automatic as possible. These rules were provided through tactics, or existing or newly created. These tactics were automatic, or manual, or sometimes both. Providing new proving rules, even if it sometimes does not increase directly the number of automatically discharged POs aims to help the user to interactively discharge them and spare his time. | ||
== Advanced Preferences for Auto-tactics == | == Advanced Preferences for Auto-tactics == | ||
Line 19: | Line 20: | ||
== Isabelle Plug-in == | == Isabelle Plug-in == | ||
At the beginning of the DEPLOY project, the user had three choices when valid proof obligations are not discharged automatically: (1) do manual proofs, (2) reorganise the model to make it "simpler" for Rodin's theorem provers, or (3) implement an extension of Rodin's theorem provers in Java. None of these options is fully satisfactory for models at industrial scale: | |||
#The number of undischarged proof obligations is typically very high, which makes manual proving an expensive task; in particular, users have reported that they had to enter very similar proofs again and again (for different proof obligations), which they found frustrating. | |||
#Reorganising the model helps in some situations, but it does not help in others, and it requires considerable experience and a deep understanding of Rodin's theorem provers. | |||
#Extending Rodin's theorem provers is quite effective in principle. However, prover extensions need be definned in Java in a procedural style; the source code of prover extensions is therefore hard to read and write. Moreover, it is quite difficult to ensure that prover extensions are sound. If a model has been verified with an extended version of Rodin's theorem provers, it is therefore questionable whether the model is indeed correct. | |||
The integration of Isabelle/HOL<ref>T. Nipkow, L. C. Paulson, and M. Wenzel. Isabelle/HOL - A Proof Assistant for Higher-Order Logic, volume 2283 of Lecture Notes in Computer Science. Springer, 2002.</ref> into Rodin is one solution to this problem. Isabelle/HOL is the instantiation of the generic theorem prover Isabelle<ref>L. C. Paulson. The foundation of a generic theorem prover. Journal of Automated Reasoning, 5(3):363-397, 1989.</ref> to higher-order logic<ref>P. B. Andrews. An Introduction to Mathematical Logic and Type Theory. Springer,2002.</ref><ref>A. Church. A formulation of the simple theory of types. Journal of Symbolic Logic,5(2):56-68, 1940.</ref><ref>M. J. C. Gordon and T. F. Melham. Introduction to HOL. Cambridge University Press, 1993.</ref>. The main advantage of Isabelle is to provide a high degree of extensibility whilst ensuring soundness. In a nutshell, every proof in Isabelle has to be approved by Isabelle's core, which has matured over several decades and is therefore most likely correct. In Isabelle, user supplied prover extensions are sound by construction. | |||
Isabelle comes with a vast collection of automated proof tactics that can be customised by the user in a declarative manner, i.e., by declaring new inference and rewrite rules. It provides link-ups to several competition winning automated theorem provers such as Z3 <ref>L. M. de Moura and N. Bjørner. Z3: An efficient SMT solver. In TACAS, volume 4963 of Lecture Notes in Computer Science, pages 337-340. Springer, 2008.</ref> and Vampire<ref>A. Riazanov and A. Voronkov. The design and implementation of Vampire. AI Communications, 15(2-3):91-110, 2002.</ref>. Last but not least, the default configuration of Isabelle's proof tactics has matured over years or decades and has been applied in numerous verification projects. | |||
== ProB Disprover == | == ProB Disprover == | ||
Line 25: | Line 32: | ||
This feature relies on the constraint solving capabilities of the ProB kernel. It is available from the ProB plugin after loading an Event-B model. | This feature relies on the constraint solving capabilities of the ProB kernel. It is available from the ProB plugin after loading an Event-B model. | ||
Within the context of WP2 (Transportation) ProB has also been used to try and find counterexamples to individual proof rules in the Siemens proof rule database. | |||
For this, the ProB command line tool has been extended to load proof rule files (using a Prolog parser to avoid the JVM startup time) and then applies the ProB constraint solver to try and find counter examples to each proof rule. | For this, the ProB command line tool has been extended to load proof rule files (using a Prolog parser to avoid the JVM startup time) and then applies the ProB constraint solver to try and find counter examples to each proof rule. | ||
== SMT Solver Integration == | == SMT Solver Integration == | ||
Line 36: | Line 39: | ||
== Incorporating SAT Solvers via Kodkod == | == Incorporating SAT Solvers via 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. | 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 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. | 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. | 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. | 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. | ||
Line 55: | Line 53: | ||
= Choices / Decisions = | = Choices / Decisions = | ||
== New rewriting and inference rules == | == New rewriting and inference rules == | ||
During the last year of DEPLOY, rewriting (over 150) and inference rules were implemented into the built-in prover. The implementation was scheduled and prioritized according to the ratio importance/complexity of the rule. | |||
== Advanced Preferences for Auto-tactics == | == Advanced Preferences for Auto-tactics == | ||
Line 65: | Line 64: | ||
== Isabelle Plug-in == | == Isabelle Plug-in == | ||
The Isabelle plug-in translates a proof obligation to Isabelle/HOL and then invokes a custom Isabelle tactic and reports the result back to Rodin. Most of the work that has been done concerned the study of Event-B theory and its translation to HOL. Unlike translations to other theorem provers (such as PP, newPP, and ML), the translation to HOL preserves provability: the translations of provable proof obligations are provable and the translations of unprovable proof obligations are unprovable. (This claim rests on the assumption that the implementation of the translation is correct. We regard this a reasonable assumption, as the implementation of the translation is quite straightforward and concise.) | |||
The performance of the default configuration can be tweaked regarding some specific situations and users can inspect the translated proof obligations in Isabelle/HOL, test the behaviour of various proof tactics, and declare new inference and rewrite rules to meet the desired performance goals. | |||
The Isabelle plug-in was evaluated on the BepiColombo model<ref>K. Varpaaniemi. Bepicolombo models v6.4 http://deploy-eprints.ecs.soton.ac.uk/244</ref> by Space Systems Finland. Isabelle discharged some of the proof obligations out of the box that could not be discharged automatically by Rodin. The automation rate could be drastically increased by declaring new inference and rewrite rules. This proceeding had an important advantage over directly entering manual proofs: by declaring new rules, we did not only make Isabelle’s automated tactics prove the proof obligation under investigation, but also other proof obligations that we had not yet looked at. | |||
== ProB Disprover == | == ProB Disprover == | ||
Line 76: | Line 78: | ||
* ProB can find out which of the axioms are theorems and ignore them. Indeed in the old ProB disprover approach all of the assumptions were fed, and ProB did not know which ones are relevant to find correct values for the constants and variables. In fact, some of the theorems turned out to be very complicated to check, and prevented ProB from finding counterexamples. | * ProB can find out which of the axioms are theorems and ignore them. Indeed in the old ProB disprover approach all of the assumptions were fed, and ProB did not know which ones are relevant to find correct values for the constants and variables. In fact, some of the theorems turned out to be very complicated to check, and prevented ProB from finding counterexamples. | ||
Similarly, the constraint-based deadlock checker is run from the ProB plug-in on a loaded model. As Rodin does not currently generate the deadlock freedom proof obligations, this was an obvious choice. Also, it enables the user to type in additional predicates to find "particularly interesting" counter examples (see ICLP'2011 article below). | Similarly, the constraint-based deadlock checker is run from the ProB plug-in on a loaded model. As Rodin does not currently generate the deadlock freedom proof obligations, this was an obvious choice. Also, it enables the user to type in additional predicates to find "particularly interesting" counter examples (see ICLP'2011 article below<ref name="ICLP"/>). | ||
Also, another advantage is that, again, the counter example can be inspected using the ProB interface. | Also, another advantage is that, again, the counter example can be inspected using the ProB interface. | ||
== SMT Solver Integration == | == SMT Solver Integration == | ||
The translation of Event-B language into the SMT-LIB language is the main issue of this integration. Two approaches were developed for this. The more efficient one is based on the translation capabilities of the integrated predicate prover of the Rodin platform (PP). It is completed by translating membership using an uninterpreted predicate symbol, refined with an axiom of the set theory. | The translation of Event-B language into the SMT-LIB language is the main issue of this integration. Two approaches were developed for this. The more efficient one is based on the translation capabilities of the integrated predicate prover of the Rodin platform (PP). It is completed by translating membership using an uninterpreted predicate symbol, refined with an axiom of the set theory. | ||
Technically, the plug-in classes extend the existing XProverCall, XProverInput, | Technically, the plug-in classes uses the XProver API along with the ISimpleSequent framework, and extend the existing XProverCall, XProverInput, XProverReasoner2, AbstractLazilyConstrTactic and ITacticParametizer classes which make it easy to integrate new tactics, reasoners and external prover calls. | ||
== Incorporating SAT Solvers via Kodkod == | == Incorporating SAT Solvers via Kodkod == | ||
Before starting our translation to Kodkod, we had experimented with several other alternate approaches to solve constraints in ProB. | 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. | [http://bddbddb.sourceforge.net/ bddbddb] offers the user a Datalog-like language that aims to support program analysis. | ||
Line 96: | Line 96: | ||
The SAL tool suite includes a state of the art symbolic (BDD-based) and bounded (SAT-based) model checkers. | 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. | 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 = | = Available Documentation = | ||
Links for New rewriting and inference rules: | |||
* | Two lists are available on the wiki | ||
* | *The list of all the defined rewrite rules<ref>http://wiki.event-b.org/index.php/All_Rewrite_Rules</ref> | ||
* | *The list of all the defined inference rules<ref>http://wiki.event-b.org/index.php/Inference_Rules</ref> | ||
* | Links for Advanced Preferences for Auto-tactics: | ||
* A page concerning tactic profiles is available in the user manual<ref>http://handbook.event-b.org/current/html/preferences.html</ref> | |||
* | Links for Isabelle Plug-in: | ||
*A wiki page is dedicated to the Isabelle Plug-in <ref>http://wiki.event-b.org/index.php/Isabelle_for_Rodin</ref>. | |||
*Some of the theoretical foundations are described in <ref>http://www.springerlink.com/content/b7286q3k52180v68 Matthias Schmalz. Term Rewriting in Logics of Partial Functions. ICFEM 2011</ref> | |||
*More information will become available in <ref>Formalizing the Logic of Event-B. Partial Functions, Definitional Extensions, and Automated Theorem Proving. Submitted as PhD thesis to ETH Zurich.</ref> | |||
Links for ProB Disprover: | |||
* A paper on constraint-based deadlock checking had been published.<ref name="ICLP">Constraint-Based Deadlock Checking of High-Level Specifications. In Proceedings ICLP'2011, Cambridge University Press, 2011. http://www.stups.uni-duesseldorf.de/w/Special:Publication/HaLe2011</ref> | |||
Links for ProB Kodkod Integration: | |||
* A technical report has been published in 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> | |||
Links for SMT Solver Integration: | |||
*A wiki page is dedicated to the SMT Solver integration plug-in<ref>http://wiki.event-b.org/index.php/SMT_Solvers_Plug-in</ref>. | |||
= Status = | = Status = | ||
== New rewriting and inference rules == | == New rewriting and inference rules == | ||
By the end of the DEPLOY project: | |||
*there are 477 rewrite rules expressed, 423 of them were implemented. (80 were defined at the beginning of DEPLOY, 32 implemented) | |||
*there are 115 inference rules expressed, 98 of them were implemented. (54 were defined at the beginning of DEPLOY, 51 implemented) | |||
== Advanced Preferences for Auto-tactics == | == Advanced Preferences for Auto-tactics == | ||
Line 117: | Line 130: | ||
== Isabelle Plug-in == | == Isabelle Plug-in == | ||
During the DEPLOY project, a way of customising Rodin’s theorem provers on the user level has been developed, namely the theory plug-in (see General Platform Maintenance section). The theory plug-in avoids the overhead of integrating an external tool into Rodin and therefore has the potential of being faster and easier to use. Whether the Isabelle or the theory plug-in (or a combination of the two) is more suitable for | |||
a given task, should be determined based on preliminary experiments. That said, Isabelle/HOL improves over the current theory plug-in in the following ways: | |||
* The theory plug-in is yet unable to express certain rules involving numerals, enumerated sets, binders, and Boolean connectives whereas Isabelle/HOL does not have such limitations. | |||
* Isabelle/HOL provides a default configuration of automated tactics that has proved itself over years. | |||
* Isabelle’s generic rewriter and classical reasoner are more powerful than the corresponding tactics of the theory plug-in. | |||
* The theory plug-in has exhibited several unsoundness bugs. Unsoundness bugs in the Isabelle plug-in are unlikely (and have not been observed) because of the maturity of Isabelle and the intuitive nature of the translation. | |||
The Isabelle plug-in adds a theorem prover with a very good automation, and high degree of extensibility and soundness to Rodin. | |||
However, in order to fully benefit from its power, familiarity with Isabelle/HOL is required. | |||
== ProB Disprover == | == ProB Disprover == | ||
Line 129: | Line 150: | ||
== SMT Solver Integration == | == SMT Solver Integration == | ||
Since the version 0.8 of the SMT Solvers integration plug-in, released in February 2012, the SMT-Solver veriT is fully integrated and distributed within the plug-in. Therefore, it is not necessary (but still possible) to install another copy of the solver. An Auto-Tactic with SMT profile is available. Thus, it is not necessary (but still possible) to create a new tactic profile to use SMT solvers tactics. However, it can be valuable to create such new profile to parameterize the SMT tactic. The integration was successfully tested with the following solvers: | |||
* Alt-Ergo 0.93 | |||
* Cvc3 2011-11-21 | |||
* veriT (included in the plug-in) | |||
* z3 3.2 | |||
* Cvc4 2011-12-11 (but few theories are available for now) | |||
This integration shown good results in the field of linear integer arithmetic with uninterpreted sort and function symbols, and good support of basic set theory. The full set theory still needs to be better supported. All the results showed the SMT-Solvers Plug-in was a good alternative to the Atelier-B provers. | |||
== Incorporating SAT Solvers via Kodkod == | == Incorporating SAT Solvers via Kodkod == | ||
The Kodkod integration is available in the latest nightly build version of ProB (1.3.5-beta7). | The Kodkod integration is available in the latest nightly build version of ProB (1.3.5-beta7). | ||
The scope of the translations is being extended, the work has been partially carried out within the ADVANCE project and will be continued within that project. | The scope of the translations is being extended, the work has been partially carried out within the ADVANCE project and will be continued within that project. | ||
=References= | |||
<references/> | |||
[[Category:D45 Deliverable]] | [[Category:D45 Deliverable]] |
Latest revision as of 21:20, 20 April 2012
Overview
Two tasks concerned the prover performance from the core platform: the addition of rewriting and inference rules, and the addition of a mechanism to allow the customization and the parametrization or combination of tactics. While the addition of rewriting and inference rules has always been a regular task to enhance the Rodin integrated prover during DEPLOY lifetime, a new way to manage tactics has been implemented. In fact, the user is now able to define various types of tactics called 'profiles' which could be customized and parameterized tactics to discharge some specific proof obligations.
The ProB plug-in allows to find and visualize counter examples to the invariant and deadlock preservation proof obligations. ProB has also been used for finding count examples to proof rules of the industrial partner Siemens.
The SMT Solvers plug-in allowing to use the SMT solvers within Rodin is an effective alternative to the Atelier-B provers, particularly when reasoning on linear arithmetic.
The Isabelle/HOL integration plug-in allows to extend the Rodin proving capabilities through the definition of tactic written in Isabelle/HOL and thus, provides help to automatically discharge proof obligations, but also allows the verification of the new extensions of the Rodin sequent prover written in java through the translation of their corresponding rules.
Motivations
New rewriting and inference rules
In an Event-B development, more than 60% of the time is spent on proofs. It has been a continuous aim to increase the number of automatically discharged proof obligations (POs) by improving the capabilities of the integrated sequent prover through the addition of rewriting and inference rules. Naturally all of the industrial partners in DEPLOY are keen for the proofs to be as automatic as possible. These rules were provided through tactics, or existing or newly created. These tactics were automatic, or manual, or sometimes both. Providing new proving rules, even if it sometimes does not increase directly the number of automatically discharged POs aims to help the user to interactively discharge them and spare his time.
Advanced Preferences for Auto-tactics
The proportion of automatically discharged proof obligations heavily depends on Auto-Tactic configuration. Sometimes, the automatic prover fails because the tactics are applied in a 'wrong' order - 'wrong' for a given PO - even though all needed tactics are present. Early version of Rodin provided preferences for automatic tactics that enabled to reorder them, but the ordering was lost at each change: one could not record a particular tactic order in order to reuse it later.
Another issue is to have more than one possibility to combine the tactics. Indeed, the only implicit combination of tactics available consisted in trying to apply them in turn for every open node of a proof. In the proving area, there exists a notion of tactic combinators, also called tacticals, that allow to combine tactics in various specific manners, thus providing a sort of tactic arithmetic.
The advanced preferences for auto-tactics solved these two issues.
Isabelle Plug-in
At the beginning of the DEPLOY project, the user had three choices when valid proof obligations are not discharged automatically: (1) do manual proofs, (2) reorganise the model to make it "simpler" for Rodin's theorem provers, or (3) implement an extension of Rodin's theorem provers in Java. None of these options is fully satisfactory for models at industrial scale:
- The number of undischarged proof obligations is typically very high, which makes manual proving an expensive task; in particular, users have reported that they had to enter very similar proofs again and again (for different proof obligations), which they found frustrating.
- Reorganising the model helps in some situations, but it does not help in others, and it requires considerable experience and a deep understanding of Rodin's theorem provers.
- Extending Rodin's theorem provers is quite effective in principle. However, prover extensions need be definned in Java in a procedural style; the source code of prover extensions is therefore hard to read and write. Moreover, it is quite difficult to ensure that prover extensions are sound. If a model has been verified with an extended version of Rodin's theorem provers, it is therefore questionable whether the model is indeed correct.
The integration of Isabelle/HOL[1] into Rodin is one solution to this problem. Isabelle/HOL is the instantiation of the generic theorem prover Isabelle[2] to higher-order logic[3][4][5]. The main advantage of Isabelle is to provide a high degree of extensibility whilst ensuring soundness. In a nutshell, every proof in Isabelle has to be approved by Isabelle's core, which has matured over several decades and is therefore most likely correct. In Isabelle, user supplied prover extensions are sound by construction. Isabelle comes with a vast collection of automated proof tactics that can be customised by the user in a declarative manner, i.e., by declaring new inference and rewrite rules. It provides link-ups to several competition winning automated theorem provers such as Z3 [6] and Vampire[7]. Last but not least, the default configuration of Isabelle's proof tactics has matured over years or decades and has been applied in numerous verification projects.
ProB Disprover
ProB can be used to find counterexamples to invariant preservation and deadlock preservation proof obligations. This feature relies on the constraint solving capabilities of the ProB kernel. It is available from the ProB plugin after loading an Event-B model.
Within the context of WP2 (Transportation) ProB has also been used to try and find counterexamples to individual proof rules in the Siemens proof rule database. For this, the ProB command line tool has been extended to load proof rule files (using a Prolog parser to avoid the JVM startup time) and then applies the ProB constraint solver to try and find counter examples to each proof rule.
SMT Solver Integration
The integration of SMT solvers into the Rodin platform is motivated by two main reasons. On the one hand, the enhancement of its proving capability, especially in the field of arithmetics. On the other hand, the ability of extracting some useful informations from the proofs produced by these solvers, such as unsatisfiable cores, in order to significantly decrease the time necessary to prove a modified model.
Incorporating SAT Solvers via 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.
Choices / Decisions
New rewriting and inference rules
During the last year of DEPLOY, rewriting (over 150) and inference rules were implemented into the built-in prover. The implementation was scheduled and prioritized according to the ratio importance/complexity of the rule.
Advanced Preferences for Auto-tactics
Since Rodin 2.1, one can create his own tactic profiles. A tactic profile allows to set and record a particular order of chosen basic tactics. Furthermore, a profile can be applied either globally (as before), or specifically for a given project.
Since Rodin 2.3, tacticals and parameterization have been added to the profiles, thus increasing the potential of such proving feature. A tactic profile may now be composed of tacticals, that combine any number of basic tactics and other profiles. The parameterization allows for example to set a custom timeout on external provers such as AtelierB P1.
Isabelle Plug-in
The Isabelle plug-in translates a proof obligation to Isabelle/HOL and then invokes a custom Isabelle tactic and reports the result back to Rodin. Most of the work that has been done concerned the study of Event-B theory and its translation to HOL. Unlike translations to other theorem provers (such as PP, newPP, and ML), the translation to HOL preserves provability: the translations of provable proof obligations are provable and the translations of unprovable proof obligations are unprovable. (This claim rests on the assumption that the implementation of the translation is correct. We regard this a reasonable assumption, as the implementation of the translation is quite straightforward and concise.) The performance of the default configuration can be tweaked regarding some specific situations and users can inspect the translated proof obligations in Isabelle/HOL, test the behaviour of various proof tactics, and declare new inference and rewrite rules to meet the desired performance goals. The Isabelle plug-in was evaluated on the BepiColombo model[8] by Space Systems Finland. Isabelle discharged some of the proof obligations out of the box that could not be discharged automatically by Rodin. The automation rate could be drastically increased by declaring new inference and rewrite rules. This proceeding had an important advantage over directly entering manual proofs: by declaring new rules, we did not only make Isabelle’s automated tactics prove the proof obligation under investigation, but also other proof obligations that we had not yet looked at.
ProB Disprover
Currently the constraint based invariant and deadlock checker is run from within the ProB plug-in and not from the prover interface on individual proof obligations. Indeed, for invariant preservation the disprover thus checks an event for all invariants, rather than being applied on individual proof obligations related to that event. However, ProB does know which invariants have already been proven to be preserved by that particular event. The rationale for running the invariant preservation checks in this way is that:
- the counterexample is a full valuation of the models variables and constants which can be displayed using the ProB interface,
- the invariants and guards truth values can be inspected in detail using the ProB interface, make the counter-example intelligible to the user,
- ProB can find out which of the axioms are theorems and ignore them. Indeed in the old ProB disprover approach all of the assumptions were fed, and ProB did not know which ones are relevant to find correct values for the constants and variables. In fact, some of the theorems turned out to be very complicated to check, and prevented ProB from finding counterexamples.
Similarly, the constraint-based deadlock checker is run from the ProB plug-in on a loaded model. As Rodin does not currently generate the deadlock freedom proof obligations, this was an obvious choice. Also, it enables the user to type in additional predicates to find "particularly interesting" counter examples (see ICLP'2011 article below[9]). Also, another advantage is that, again, the counter example can be inspected using the ProB interface.
SMT Solver Integration
The translation of Event-B language into the SMT-LIB language is the main issue of this integration. Two approaches were developed for this. The more efficient one is based on the translation capabilities of the integrated predicate prover of the Rodin platform (PP). It is completed by translating membership using an uninterpreted predicate symbol, refined with an axiom of the set theory. Technically, the plug-in classes uses the XProver API along with the ISimpleSequent framework, and extend the existing XProverCall, XProverInput, XProverReasoner2, AbstractLazilyConstrTactic and ITacticParametizer classes which make it easy to integrate new tactics, reasoners and external prover calls.
Incorporating SAT Solvers via Kodkod
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
Links for New rewriting and inference rules: Two lists are available on the wiki
Links for Advanced Preferences for Auto-tactics:
- A page concerning tactic profiles is available in the user manual[12]
Links for Isabelle Plug-in:
- A wiki page is dedicated to the Isabelle Plug-in [13].
- Some of the theoretical foundations are described in [14]
- More information will become available in [15]
Links for ProB Disprover:
- A paper on constraint-based deadlock checking had been published.[9]
Links for ProB Kodkod Integration:
- A technical report has been published in the validation using ProB and Kodkod [16]
Links for SMT Solver Integration:
- A wiki page is dedicated to the SMT Solver integration plug-in[17].
Status
New rewriting and inference rules
By the end of the DEPLOY project:
- there are 477 rewrite rules expressed, 423 of them were implemented. (80 were defined at the beginning of DEPLOY, 32 implemented)
- there are 115 inference rules expressed, 98 of them were implemented. (54 were defined at the beginning of DEPLOY, 51 implemented)
Advanced Preferences for Auto-tactics
Advanced Preferences for Auto-tactics are functional in Rodin 2.3. This release provides a first set of tacticals and parameterization options.
Further releases may offer additional tacticals and options, according to user feedback.
Isabelle Plug-in
During the DEPLOY project, a way of customising Rodin’s theorem provers on the user level has been developed, namely the theory plug-in (see General Platform Maintenance section). The theory plug-in avoids the overhead of integrating an external tool into Rodin and therefore has the potential of being faster and easier to use. Whether the Isabelle or the theory plug-in (or a combination of the two) is more suitable for a given task, should be determined based on preliminary experiments. That said, Isabelle/HOL improves over the current theory plug-in in the following ways:
- The theory plug-in is yet unable to express certain rules involving numerals, enumerated sets, binders, and Boolean connectives whereas Isabelle/HOL does not have such limitations.
- Isabelle/HOL provides a default configuration of automated tactics that has proved itself over years.
- Isabelle’s generic rewriter and classical reasoner are more powerful than the corresponding tactics of the theory plug-in.
- The theory plug-in has exhibited several unsoundness bugs. Unsoundness bugs in the Isabelle plug-in are unlikely (and have not been observed) because of the maturity of Isabelle and the intuitive nature of the translation.
The Isabelle plug-in adds a theorem prover with a very good automation, and high degree of extensibility and soundness to Rodin. However, in order to fully benefit from its power, familiarity with Isabelle/HOL is required.
ProB Disprover
The ProB constraint-based invariant and deadlock checkers are available in the current release of ProB for Rodin. The deadlock checker has been applied successfully on a very large industrial model within WP1 (automotive). There is of course always the scope to improve the capabilities of the tool by improving the constraint solving capabilities. In particular, further simplification of existential quantifiers will be important for the deadlock checker to be applied effectively on certain models.
The Siemens proof rule database validation work is still ongoing. This work has already identified several errors in the Siemens rule database. However, a current issue is the addition of explicit well-definedness conditions into the proof rules, as well as the fact that some proof rules use substations inside predicates.
SMT Solver Integration
Since the version 0.8 of the SMT Solvers integration plug-in, released in February 2012, the SMT-Solver veriT is fully integrated and distributed within the plug-in. Therefore, it is not necessary (but still possible) to install another copy of the solver. An Auto-Tactic with SMT profile is available. Thus, it is not necessary (but still possible) to create a new tactic profile to use SMT solvers tactics. However, it can be valuable to create such new profile to parameterize the SMT tactic. The integration was successfully tested with the following solvers:
- Alt-Ergo 0.93
- Cvc3 2011-11-21
- veriT (included in the plug-in)
- z3 3.2
- Cvc4 2011-12-11 (but few theories are available for now)
This integration shown good results in the field of linear integer arithmetic with uninterpreted sort and function symbols, and good support of basic set theory. The full set theory still needs to be better supported. All the results showed the SMT-Solvers Plug-in was a good alternative to the Atelier-B provers.
Incorporating SAT Solvers via Kodkod
The Kodkod integration is available in the latest nightly build version of ProB (1.3.5-beta7). The scope of the translations is being extended, the work has been partially carried out within the ADVANCE project and will be continued within that project.
References
- ↑ T. Nipkow, L. C. Paulson, and M. Wenzel. Isabelle/HOL - A Proof Assistant for Higher-Order Logic, volume 2283 of Lecture Notes in Computer Science. Springer, 2002.
- ↑ L. C. Paulson. The foundation of a generic theorem prover. Journal of Automated Reasoning, 5(3):363-397, 1989.
- ↑ P. B. Andrews. An Introduction to Mathematical Logic and Type Theory. Springer,2002.
- ↑ A. Church. A formulation of the simple theory of types. Journal of Symbolic Logic,5(2):56-68, 1940.
- ↑ M. J. C. Gordon and T. F. Melham. Introduction to HOL. Cambridge University Press, 1993.
- ↑ L. M. de Moura and N. Bjørner. Z3: An efficient SMT solver. In TACAS, volume 4963 of Lecture Notes in Computer Science, pages 337-340. Springer, 2008.
- ↑ A. Riazanov and A. Voronkov. The design and implementation of Vampire. AI Communications, 15(2-3):91-110, 2002.
- ↑ K. Varpaaniemi. Bepicolombo models v6.4 http://deploy-eprints.ecs.soton.ac.uk/244
- ↑ 9.0 9.1 Constraint-Based Deadlock Checking of High-Level Specifications. In Proceedings ICLP'2011, Cambridge University Press, 2011. http://www.stups.uni-duesseldorf.de/w/Special:Publication/HaLe2011
- ↑ http://wiki.event-b.org/index.php/All_Rewrite_Rules
- ↑ http://wiki.event-b.org/index.php/Inference_Rules
- ↑ http://handbook.event-b.org/current/html/preferences.html
- ↑ http://wiki.event-b.org/index.php/Isabelle_for_Rodin
- ↑ http://www.springerlink.com/content/b7286q3k52180v68 Matthias Schmalz. Term Rewriting in Logics of Partial Functions. ICFEM 2011
- ↑ Formalizing the Logic of Event-B. Partial Functions, Definitional Extensions, and Automated Theorem Proving. Submitted as PhD thesis to ETH Zurich.
- ↑ http://www.stups.uni-duesseldorf.de/w/Special:Publication/PlaggeLeuschel_Kodkod2012 Validating B,Z and TLA+ using ProB and Kodkod. Technical Report, 2012.
- ↑ http://wiki.event-b.org/index.php/SMT_Solvers_Plug-in