Patterns for Refinement Automation - Formal Methods for Components and Objects - page 72

S , written S S , if, whenever S establishes a certain postcondition, so does S [9].

Since statement composition is monotonic with respect to the refinement relation, re-
finement of a model statement is also refinement of the whole model. In general, the re-
finement process can be seen as a way to reduce non-determinism of the abstract model,
to replace abstract mathematical data structures by data structures implementable on a
computer, and, hence, gradually introduce implementation decisions.
There have been several attempts to facilitate the refinement process, by generalizing
the typical refinement transformations into a set of refinement rules [5,16]. These rules
can be seen as generic templates (or patterns) that define the general form of the state-
ment to be transformed, the resultant statement, and the proof obligations that should
be discharged to verify refinement for that particular transformation. However, a refine-
ment rule usually describes a small localized transformation of a certain model part.
Obviously, the tools developed to automate application of such refinement rules [8,17]
lack scalability.
On the other hand, such frameworks as Z, VDM, and Event B support the formal
development by model transformation of the entire system. For instance, the RODIN
platform - a tool supporting refinement in Event B - allows us to perform refinement
by introducing many changes at once and to verify by proofs that these changes result in
correct model refinement. Often a refinement step can be seen as a composition of ”stan-
dard” (frequently reoccurring) localized transformations distributed all over the model.
Additional research is needed, though, to answer the question whether we can employ
the transformational approach to fully automate execution of these transformations by
reusing the models and proofs that were constructed previously.
In this paper we propose to tackle this problem via definition and use of refinement
patterns. Our definition of refinement patterns builds on the idea of refinement rules.
In general, a refinement pattern is a model transformer. Unlike design patterns [10], a
refinement pattern is “dynamic” in a sense that the process of pattern application takes
a model as an input and produces a new model as an output. Moreover, both syntactic
and semantic information about models is used to precisely define a refinement pattern.
To formalize and automate the process of pattern application, we define a pattern as
a model transformer consisting of three parts. The first part is the pattern applicability
conditions, i.e., the syntactic and semantic conditions that should be fulfilled by the
model for a refinement pattern to be applicable. The second part contains a definition of
syntactic manipulations on the model to be transformed. Finally, the third part consists
of the proof obligations that should be discharged to verify that the performed model
transformation is indeed a refinement step. It is easy to see that a refinement pattern
manipulates a model on both syntactic and semantic level.
In principle, refinement patterns can be defined for any refinement-based modelling
framework. In this paper we present our proposal for refinement patterns in the Event B
formalism and also describe a prototype tool that implements them. We start by briefly
introducing the Event B language and giving semantic and syntactic views on its models.

2.2 Event B

In this section we introduce our formal framework - the B Method [2]. It is an ap-
proach for the industrial development of highly dependable software. The method has