Difference between revisions of "D23 Modularisation Plug-in"
imported>Alexili m (New page: = 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 prov...) |
imported>Alexili m |
||
| Line 2: | Line 2: | ||
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. | 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 plugin was developed in Newcastle University in cooperation with Abo Academy | + | 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 plugin was developed in Newcastle University in cooperation with Abo Academy and Space Systems Finland. | ||
= Motivations = | = Motivations = | ||
Revision as of 09:55, 18 November 2009
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 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 plugin was developed in Newcastle University in cooperation with Abo Academy and Space Systems Finland.
