D23 Modularisation Plug-in: Difference between revisions
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 mNo edit summary |
||
| 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.
