Modularisation Clause Samples

Modularisation. Rodin platform's modularisation plug-in [RD7] (see also [RD11]), designed by Newcastle and Aabo as a part of WP3, provides facilities for structuring Event-B developments into logical units of modelling, called modules. The module concept is very close to the notion of classical B imports. However, unlike a conventional development, a module comes with an interface. An interface defines the conditions on how 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. There are at least the following reasons to split a development into modules. • Structuring large specifications: it is difficult to read and edit a large model; there is also a limit to the size of model that the Rodin 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) developer team. • Model reuse: modules may be exchanged and reused in different projects. The notion of interface makes it easier to integrate a module in a new context. A modularisation plug-in experiment on BepiColombo SIXS/MIXS OBSW requirements was carried out at SSF in August – September 2010 and was focused on a few of the requirements that had been considered in earlier non-modular experiments. The original goals of the experiment were as follows: • Systematic isolation of activity details and related conditions to modules in such a way that the machines using the modules do not replicate much of what is expressed inside the modules. • Precision of descriptions of the considered behaviour about as accurate as in the most detailed available non-modular Event-B model. • Avoidance of massive atomic activities. Long chains of atomic activities do not realistically model concurrency. • To deal with "module integration invariants". Such an invaria...