D23 Decomposition

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.

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-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.

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:

• 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.
• 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 exchange 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 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.

• 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.

• 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.

• 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.