D23 Modularisation Plug-in
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 Modularisation Plug-in Release Notes.
