Experience at SSF Sample Clauses
Experience at SSF. 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 the non-‐modular experiments reported by [RD5]. 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 realistically model concurrency. • To deal with “module integration invariants”. Such an invariant refers to variables of more than one module. • Reasonable total proof effort (including time spent in “iterative optimisation”) without compromising the above goals. The final Event-‐B project [RD24] of the experiment can be understood to sufficiently meet all the above-‐mentioned goals, except possibly the proof effort reasonability goal. However, the proof effort was to a certain extent more reasonable than in some earlier Rodin Platform experiments. Much time in the experiment got spent in recognition and circumvention of bugs and dealing with other undesirable features. The problems that were reported during the experiment (see [RD22] and [RD23]) have been solved in later releases of the plug-‐in. Since October 2010, the plug-‐in has been in a good shape w.r.t. the features used in the experiment. In particular, usage of the platform in the modular experiment was not dominated by memory-‐consumption-‐based non-‐response phenomena. By following certain modelling conventions it is possible to significantly improve the usability of modularisation plug-‐in. The conventions are summarized below: -‐ Avoiding very large and complicated operation post conditions, especially involving existential quantifiers to simplify proofs. In general, complex post conditions can be simplified by introducing additional module variables and invariant properties on these variables -‐ Refraining from using operation calls to model returned exceptions. To achieve the same effect one might strengthen preconditions of calling events by checking external module variables. Rather than using returned composite values, which can include the status indicating success or a parti...