Difference between pages "D23 Decomposition" and "D23 Improvements to Existing Provers"

From Event-B
(Difference between pages)
Jump to navigationJump to search
imported>Pascal
 
imported>Nicolas
m
 
Line 1: Line 1:
 
= Overview =
 
= Overview =
−
The Event-B model decomposition is a new feature in the Rodin platform.
 
  
−
Two methods have been identified in the DEPLOY project for model decomposition: the ''shared variable'' decomposition (or A-style decomposition, after Abrial), and the ''shared event'' decomposition (or B-style decomposition, after Butler). They both answer to the same requirement, namely the possibility to decompose a model <math>M</math> into several independent sub-models <math>M_1, ...,M_n</math>.
+
All along the lifecycle of the provers, the following improvements can be achieved :
 +
* adding new useful proof rules (to prove sequents that are hard to prove or even not provable at all)  
 +
* correcting bugs in implementations of existing proof rules
 +
* implementing new tools to help the user do proofs
 +
* evolving prover API to fit with the needs of prover plug-in developers
  
−
Academic (ETH Zurich, University of Southampton) and industrial (Systerel) partners were involved in the specifications and developments. Systerel, which could have useful discussions with Jean-Raymond Abrial on the topic, was more especially responsible of the A-style decomposition. The University of Southampton, where Michael Butler is professor, was in charge of the B-style decomposition.
+
Part of implemented rules and user interface features come from user feedback, mainly through SourceForge feature requests. SourceForge bugs are also an important source of input for corrections.
 +
Systerel is in charge of prover improvements.
  
 
= Motivations =
 
= Motivations =
−
One of the most important feature of the Event-B approach is the possibility to introduce new events and data-refinement of variables during refinement steps.
 
  
−
It however results in an increasing complexity of the refinement process when having to deal with many events, many state variables, and consequently many proof obligations.
+
Areas of improvement for provers can be summarized as follows:
−
This is well illustrated in the ''Event build-up'' slide of the Wright presentation during the Rodin Workshop 2009.
+
* reducing proving time and effort
−
: See [http://wiki.event-b.org/index.php/Image:Steve_Wright_Quite_Big_Model_Presentation.pdf http://wiki.event-b.org/index.php/Image:Steve_Wright_Quite_Big_Model_Presentation.pdf].
+
: New Proof Rules
 +
* reflecting prover implementation corrections
 +
: Reasoner Versioning
 +
* reducing proof storage space
 +
: Proof Purging
 +
: Proof Simplifying
 +
: Non textual Database Storage
 +
* facilitating manual proof review or reuse
 +
: Proof Skeleton View
 +
: Copy paste from skeleton to edited proof
 +
* Prover API evolution
 +
: New Tactic Provider API
  
−
The purpose of the Event-B model decomposition is precisely to give a way to address such a difficulty, by cutting a large model <math>M</math> into smaller sub-models <math>M_1, ..., M_n</math>. The sub-models can then be refined separately and more comfortably than the whole. The constraint that shall be satisfied by the decomposition is that these refined models might be recomposed into a whole model <math>MR</math> in a way that guarantees that <math>MR</math> refines <math>M</math>.
 
  
−
The model decomposition leads to some interesting benefits:
+
= Choices / Decisions =
−
* Design/architectural decision. It applies in particular when it is noticed that it is not necessary to consider the whole model for a given refinement step, because only a few events and variables are involved instead.
 
−
* Complexity management. In other words, it alleviates the complexity by splitting the proof obligations over the sub-models.
 
−
* Team development. More precisely, it gives a way for several developers to share the parts of a decomposed model, and to work independently and possibly in parallel on them.
 
  
−
Note that the possibility of team development is among the current priorities for all industrial partners. The model decomposition is a first answer to this issue.
+
Proof storage in database ? {{TODO}}
 +
A more generical way to contribute tactics (New tactic provider API)
  
−
= Choices / Decisions =
 
−
The main decision concerning the implementation of the Event-B model decomposition in the Rodin platform is to make available both decomposition styles (''shared variables'' vs. ''shared events'') through one single plug-in. These approaches are indeed complementary and the end-user may take advantage of the former or of the latter, depending on the model (eg. the ''shared variables'' approach seems more suitable when modelling parallel system and the ''shared events'' approach seems more suitable when modelling message-passing distributed systems).
 
  
−
Choices, either related to the plug-in core or to the plug-in graphical user interface, have been made with the following constraints in mind:
+
= Available Documentation =
−
* Planning. Some options, such as using the Graphical Modelling Framework for the decomposition visualization, or outsourcing the context decomposition, have not been explored (at least in the first instance), mainly because of time constraints (according to the DEPLOY description of work, the decomposition support was expected by the end of 2009).
 
−
* Easy-to-use (however not simplistic) tool. It applies on the one hand to the tool implementation (decomposition wizard, configuration file to replay the decomposition) and on the other hand to the tool documentation (the purpose of the user's guide is to provide useful information for beginners and for more advanced users, in particular through a ''Tips and Tricks'' section).
 
−
* Modularity and consistency. In particular, the developments have not been performed in the Event-B core. Instead the Eclipse extension mechanisms have been used to keep the plug-in independent (eg. the static checker, the proof obligation generator and the editor have been extended).
 
−
* Performance.
 
−
* Recursivity. Thus, it is possible to decompose a previously decomposed model.
 
  
−
Other technical decisions are justified in the specification wiki pages.
+
The following pages give useful information about prover improvements:
 +
* Prover Rules
 +
: See [http://wiki.event-b.org/index.php/Inference_Rules http://wiki.event-b.org/index.php/Inference_Rules]
 +
: See [http://wiki.event-b.org/index.php/All_Rewrite_Rules http://wiki.event-b.org/index.php/All_Rewrite_Rules]
 +
* Proof Skeleton View
 +
: See [http://wiki.event-b.org/index.php/Proof_Skeleton_View http://wiki.event-b.org/index.php/Proof_Skeleton_View]
 +
* Proof Purger
 +
: See [http://wiki.event-b.org/index.php/Proof_Purger_Interface http://wiki.event-b.org/index.php/Proof_Purger_Interface]
 +
* Prover API evolution
 +
: See [http://wiki.event-b.org/index.php/New_Tactic_Providers http://wiki.event-b.org/index.php/New_Tactic_Providers]
 +
* Versioned Reasoners
 +
: See [http://wiki.event-b.org/index.php/Versioned_Reasoners http://wiki.event-b.org/index.php/Versioned_Reasoners]
  
−
= Available Documentation =
 
−
The following wiki pages have been respectively written for developers and end-users to document the Event-B model decomposition:
 
−
* Shared variables (A-style) decomposition specification.
 
−
:See [[Event_Model_Decomposition | http://wiki.event-b.org/index.php/Event_Model_Decomposition]].
 
−
* Decomposition plug-in user's guide.
 
−
:See [[Decomposition_Plug-in_User's_Guide | http://wiki.event-b.org/index.php/Decomposition_Plug-in_User's_Guide]].
 
  
 
= Planning =
 
= Planning =
−
The decomposition plug-in is available since release 1.2 of the platform.
+
 
−
:See [[Rodin_Platform_1.2_Release_Notes | http://wiki.event-b.org/index.php/Rodin_Platform_1.2_Release_Notes]].
+
Proof storage in database ? {{TODO}}
 +
 
 +
 
 +
[[Category:D23 Deliverable]]

Revision as of 10:57, 17 November 2009

Overview

All along the lifecycle of the provers, the following improvements can be achieved :

  • adding new useful proof rules (to prove sequents that are hard to prove or even not provable at all)
  • correcting bugs in implementations of existing proof rules
  • implementing new tools to help the user do proofs
  • evolving prover API to fit with the needs of prover plug-in developers

Part of implemented rules and user interface features come from user feedback, mainly through SourceForge feature requests. SourceForge bugs are also an important source of input for corrections. Systerel is in charge of prover improvements.

Motivations

Areas of improvement for provers can be summarized as follows:

  • reducing proving time and effort
New Proof Rules
  • reflecting prover implementation corrections
Reasoner Versioning
  • reducing proof storage space
Proof Purging
Proof Simplifying
Non textual Database Storage
  • facilitating manual proof review or reuse
Proof Skeleton View
Copy paste from skeleton to edited proof
  • Prover API evolution
New Tactic Provider API


Choices / Decisions

Proof storage in database ? TODO A more generical way to contribute tactics (New tactic provider API)


Available Documentation

The following pages give useful information about prover improvements:

  • Prover Rules
See http://wiki.event-b.org/index.php/Inference_Rules
See http://wiki.event-b.org/index.php/All_Rewrite_Rules
  • Proof Skeleton View
See http://wiki.event-b.org/index.php/Proof_Skeleton_View
  • Proof Purger
See http://wiki.event-b.org/index.php/Proof_Purger_Interface
  • Prover API evolution
See http://wiki.event-b.org/index.php/New_Tactic_Providers
  • Versioned Reasoners
See http://wiki.event-b.org/index.php/Versioned_Reasoners


Planning

Proof storage in database ? TODO

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