Refinement Strategy and Decomposition Clause Samples

Refinement Strategy and Decomposition. The refinement stategy in Problem Frames is not necessarily the same as in Event-B, but we get some orientation of the existing refinements, which is quite helpful. It is difficult to decide on a refinement strategy before the actual work on modelling is performed. The possiblity to decompose the model in Event-B is in particular re- quired if the model is large and more than one person has to work on it. The two decomposition styles (A-style and B-style) are not sufficient for our model. We chose A-style decomposition, but if a variable is shared, it cannot be refined further. Although there is the obvious difficulty to synchronize such a decomposition we require to have support for it in order to model the cruise control system.