D23 Modularisation Plug-in: Difference between revisions

From Event-B
Jump to navigationJump to search
imported>Alexili
mNo edit summary
imported>Pascal
Line 1: Line 1:
= Overview =
= Overview =
Modularisation Plugin realises a support for structuring Event-B developments into modules. The objective is to achieve better structuring of models and proofs while also providing a facility for model reuse. It is expected that the structuring approach realised in the plugin would complement the functionality A/B-style decomposition plugin.
The Modularisation plug-in realises a support to structure Event-B developments into modules. The objective is to achieve better structuring of models and proofs while also providing a facility for model reuse. It is expected that the structuring approach realised in the plug-in would complement the functionality A/B-style decomposition plug-in.


The module concept is very close to the notion Event-B development (a refinement tree of Event-B machines). However, unlike a conventional development, a module is equipped with an interface. An interface defines the conditions on the way a module may be incorporated into another development (that is, another module). The plugin follows an approach where an interface is characterised by a list of operations specifying the services provided by the module. An integration of a module into a main development is accomplished by referring operations from Event-B machine actions using an intuitive procedure call notation.
The module concept is very close to the notion of Event-B development (a refinement tree of Event-B machines). However, unlike a conventional development, a module is equipped with an interface. An interface defines the conditions on the way a module may be incorporated into another development (that is, another module). The plug-in follows an approach where an interface is characterised by a list of operations specifying the services provided by the module. An integration of a module into a main development is accomplished by referring operations from Event-B machine actions using an intuitive procedure call notation.


The plugin was developed in Newcastle University in cooperation with Abo Academy and Space Systems Finland.   
The plug-in was developed in Newcastle University in cooperation with Abo Academy and Space Systems Finland.   


= Motivations =
= Motivations =
Line 12: Line 12:
One approach to decomposition is to identify a general theory that, once formally formulated, would contribute to the main development. For instance, a model realising a stack-based interpreter could be simplified by considering the stack concept in isolation, constructing a general theory of stacks and then reusing the results in the main development. Thus, an imported theory of stack contributes axioms and theorems assisting in reasoning about stacks.  
One approach to decomposition is to identify a general theory that, once formally formulated, would contribute to the main development. For instance, a model realising a stack-based interpreter could be simplified by considering the stack concept in isolation, constructing a general theory of stacks and then reusing the results in the main development. Thus, an imported theory of stack contributes axioms and theorems assisting in reasoning about stacks.  


Decomposition may also be achieved by splitting a system into a number of parts and then proceeding with independent development of each part. At some point, the model parts are recomposed to construct an overall final model. This decomposition style relies on the monotonicity of refinement in Event-B although some further constraints must be satisfied to ensure the validity of a recomposed model. A-style and B-style decompositions fit into this class.
Decomposition may also be achieved by splitting a system into a number of parts and then proceeding with independent development of each part. At some point, the model parts are recomposed to construct an overall final model. This decomposition style relies on the monotonicity of refinement in Event-B although some further constraints must be satisfied to ensure the validity of a recomposed model. A-style and B-style decompositions fit into this class.


Finally, decomposition may be realised by hierarchical structuring where some part of an overall system functionality is encapsulated in a self-conatined modelling unit embedded into another unit. The distinctive characteristic of this style is that recomposition of model parts happens at the same point where model is decomposed.  
Finally, decomposition may be realised by hierarchical structuring where some part of an overall system functionality is encapsulated in a self-contained modelling unit embedded into another unit. The distinctive characteristic of this style is that recomposition of model parts happens at the same point where model is decomposed.  


Modularisation plugin realises the latter approach. The procedure call concept is used to accomplish single point composition/decomposition. There are a number of reasons to try to split a development into modules. Some of them are:
The Modularisation plug-in realises the latter approach. The procedure call concept is used to accomplish single point composition/decomposition. There are a number of reasons to try to split a development into modules. Some of them are:


* Structuring large specifications: it is difficult to read and edit large model; there is also a limit to the size of model that the Platform may handle comfortably and thus decomposition is an absolute necessity for large scale developments.
* Structuring large specifications: it is difficult to read and edit a large model; there is also a limit to the size of a model that the platform may handle comfortably and thus decomposition is an absolute necessity for large scale developments.
* Decomposing proof effort: splitting helps to split verification effort. It also helps to reuse proofs: it is not unusual to return back in refinement chain and partially redo abstract models. Normally, this would invalidate most proofs in the dependent components. Model structuring helps to localise the effect of such changes.   
* Decomposing proof effort: splitting helps to split verification effort. It also helps to reuse proofs: it is not unusual to return back in refinement chain and partially redo abstract models. Normally, this would invalidate most proofs in the dependent components. Model structuring helps to localise the effect of such changes.   
* Team development: large models may only be developed by a (often distributed) developers team.  
* Team development: large models may only be developed by a (often distributed) developers team.  
* Model reuse: modules may be exchange and reused in different projects. The notion of interface make it easier to integrate a module in a new context.   
* Model reuse: modules may be exchanged and reused in different projects. The notion of interface make it easier to integrate a module in a new context.   
* Connection to library components
* Connection to library components.
* Code generation/legacy code
* Code generation/legacy code.


= Choices / Decisions =
= Choices / Decisions =


The pimary objective in the tool design was to provide a simple to use tool that could be used by a non-expert modeller. Of course, close integration with the core platform functionality was paramount.   
The primary objective in the tool design was to provide a simple to use tool that could be used by a non-expert modeller. Of course, close integration with the core platform functionality was paramount.   


* We have decided there is a need for a new type of Event-B component: interface. A decomposition based on explicit interface (rather than an implicit one such as in A-style decomposition) facilitates reuse of modules and makes it easier to provider a rich management infrastructure.  
* We have decided that there is a need for a new type of Event-B component: interface. A decomposition based on explicit interface (rather than on an implicit one, such as in A-style decomposition) facilitates the reuse of modules and makes it easier to provide a rich management infrastructure.  


* At some we had to make a decision of whether to make module integration more explicit and flexible or hide details under syntax sugar and thus achieve better model readability. We have decided that model readability should take priority over everything else. However, while model representation becomes more compact, it does not make proofs any easier.
* We have had to decide whether to make module integration more explicit and flexible or hide details under syntactic sugar and thus achieve better model readability. We have decided that model readability should take priority over everything else. However, while model representation becomes more compact, it does not make proofs easier.


* During the initial experiments we have identified a need for multiple module instantiation. This allows a modeller to use several copies of the some module using a qualifier prefix to distinguish between objects imported from the modules.
* During the initial experiments we have identified a need for multiple module instantiation. This allows a modeller to use several copies of the same module using a qualifier prefix to distinguish objects imported from the modules.


* One crucial point was realising modularisation support in such a way that structuring may be recursively applied within modules. Indeed, a module implemenation (module body) is a machine and thus it is self-similar to a caller context that is a machine.
* One crucial point was to realise modularisation support in such a way that structuring may be recursively applied within modules. Indeed, a module implementation (module body) is a machine and thus it is self-similar to a caller context that is a machine.


* For the current version, we have not implemented the generation of enabledness condition logically required for module implementation. This condition, in some form, should be present in the Platform core.     
* For the current version, we have not implemented the generation of enabledness condition logically required for module implementation. This condition, in some form, should be present in the platform core.     


= Available Documentation =
= Available Documentation =


There is a dedicated wiki page covering the plugin functionality. Also, we are working on further documentation and tutorial.
There is a dedicated wiki page covering the plug-in functionality. Also, we are working on further documentation and tutorial.


* [[Modularisation Plug-in|Plugin wiki]]
* [[Modularisation Plug-in|Plug-in wiki]]
* [[Modularisation Plug-in Tutorial|Plugin tutorial]]
* [[Modularisation Plug-in Tutorial|Plug-in tutorial]]
* [[Modularisation Plug-in Installation Instructions|Installation guide]]
* [[Modularisation Plug-in Installation Instructions|Installation guide]]


Two small-scale examples are available:
Two small-scale examples are available:
* [[http://iliasov.org/modplugin/ticketmachine.zip]] - a model of queue based on two ticket machine module instantiations (very basic)
* [[http://iliasov.org/modplugin/ticketmachine.zip]] - A model of queue based on two ticket machine module instantiations (very basic).
* [[http://iliasov.org/modplugin/doors.zip]] - two doors sluice controller specification that is decomposed into a number of independent developments (few first steps only)
* [[http://iliasov.org/modplugin/doors.zip]] - Two doors sluice controller specification that is decomposed into a number of independent developments (few first steps only).


= Planning =
= Planning =
The plugin is available since Platform version 1.1. See the [[Modularisation Plug-in Release Notes|release notes]].
The plug-in is available since the release 1.1 of the platform. See the [[Modularisation Plug-in Release Notes|release notes]].


[[Category:D23 Deliverable]]
[[Category:D23 Deliverable]]

Revision as of 11:36, 4 December 2009

Overview

The Modularisation plug-in realises a support to structure Event-B developments into modules. The objective is to achieve better structuring of models and proofs while also providing a facility for model reuse. It is expected that the structuring approach realised in the plug-in would complement the functionality A/B-style decomposition plug-in.

The module concept is very close to the notion of Event-B development (a refinement tree of Event-B machines). However, unlike a conventional development, a module is equipped with an interface. An interface defines the conditions on the way a module may be incorporated into another development (that is, another module). The plug-in follows an approach where an interface is characterised by a list of operations specifying the services provided by the module. An integration of a module into a main development is accomplished by referring operations from Event-B machine actions using an intuitive procedure call notation.

The plug-in was developed in Newcastle University in cooperation with Abo Academy and Space Systems Finland.

Motivations

There are several conceptual approaches to decomposition. To contrast our proposal, let us consider some of them.

One approach to decomposition is to identify a general theory that, once formally formulated, would contribute to the main development. For instance, a model realising a stack-based interpreter could be simplified by considering the stack concept in isolation, constructing a general theory of stacks and then reusing the results in the main development. Thus, an imported theory of stack contributes axioms and theorems assisting in reasoning about stacks.

Decomposition may also be achieved by splitting a system into a number of parts and then proceeding with independent development of each part. At some point, the model parts are recomposed to construct an overall final model. This decomposition style relies on the monotonicity of refinement in Event-B although some further constraints must be satisfied to ensure the validity of a recomposed model. A-style and B-style decompositions fit into this class.

Finally, decomposition may be realised by hierarchical structuring where some part of an overall system functionality is encapsulated in a self-contained modelling unit embedded into another unit. The distinctive characteristic of this style is that recomposition of model parts happens at the same point where model is decomposed.

The Modularisation plug-in realises the latter approach. The procedure call concept is used to accomplish single point composition/decomposition. There are a number of reasons to try to split a development into modules. Some of them are:

  • Structuring large specifications: it is difficult to read and edit a large model; there is also a limit to the size of a model that the platform may handle comfortably and thus decomposition is an absolute necessity for large scale developments.
  • Decomposing proof effort: splitting helps to split verification effort. It also helps to reuse proofs: it is not unusual to return back in refinement chain and partially redo abstract models. Normally, this would invalidate most proofs in the dependent components. Model structuring helps to localise the effect of such changes.
  • Team development: large models may only be developed by a (often distributed) developers team.
  • Model reuse: modules may be exchanged and reused in different projects. The notion of interface make it easier to integrate a module in a new context.
  • Connection to library components.
  • Code generation/legacy code.

Choices / Decisions

The primary objective in the tool design was to provide a simple to use tool that could be used by a non-expert modeller. Of course, close integration with the core platform functionality was paramount.

  • We have decided that there is a need for a new type of Event-B component: interface. A decomposition based on explicit interface (rather than on an implicit one, such as in A-style decomposition) facilitates the reuse of modules and makes it easier to provide a rich management infrastructure.
  • We have had to decide whether to make module integration more explicit and flexible or hide details under syntactic sugar and thus achieve better model readability. We have decided that model readability should take priority over everything else. However, while model representation becomes more compact, it does not make proofs easier.
  • During the initial experiments we have identified a need for multiple module instantiation. This allows a modeller to use several copies of the same module using a qualifier prefix to distinguish objects imported from the modules.
  • One crucial point was to realise modularisation support in such a way that structuring may be recursively applied within modules. Indeed, a module implementation (module body) is a machine and thus it is self-similar to a caller context that is a machine.
  • For the current version, we have not implemented the generation of enabledness condition logically required for module implementation. This condition, in some form, should be present in the platform core.

Available Documentation

There is a dedicated wiki page covering the plug-in functionality. Also, we are working on further documentation and tutorial.

Two small-scale examples are available:

  • [[1]] - A model of queue based on two ticket machine module instantiations (very basic).
  • [[2]] - Two doors sluice controller specification that is decomposed into a number of independent developments (few first steps only).

Planning

The plug-in is available since the release 1.1 of the platform. See the release notes.