Information Technology Reference
In-Depth Information
When constructing a pattern, a user may wish to generate the set of pattern correct-
ness proof obligations. Proof obligations are constructed by the proof obligation gener-
ator component. The component combines a pattern declaration and the definitions of
the used model transformations to generate a complete list of proof obligations, based
on the rules given in Section 4.3. The result is a new context file populated with the-
orems corresponding to the pattern proof obligations. The standard Platform facilities
are used to analyse and discharge the theorems.
We believe it is important to facilitate pattern exchange and thus the tool includes
a component for interfacing with an on-line pattern library. The on-line pattern library
and the model transformation library are the two main extension points of the tool. The
pattern specification language can be extended by adding custom model transformations
to the library of model transformation; addition of a model transformation should not
affect the pattern instantiation engine and the proof obligation generator.
The current version of the tool is freely available from our web site [13]. Several
patterns developed with this tool were applied during formal modelling of the Ambient
Campus case study of the RODIN Project [14].
7
Conclusions
In this paper we proposed a theoretical basis for automation of refinement process. We
introduced the notion of refinement patterns - model transformers that generically rep-
resent typical refinement steps. Refinement patterns allow us to replace a process of
devising a refined model and discharging proof obligations by a process of pattern in-
stantiation. While instantiating refinement patterns, we reuse not only models but also
proofs. All together, this establishes a basis for automation. In this paper we also demon-
strated how to define refinement patterns for the Event B formalism and described a
prototype tool allowing us to automate refinement steps in Event B.
Our work was inspired by several works on automation of refinement process. The
Refinement Calculator tool [8] has been developed to support program development
using the Refinement Calculus theory by R.Back and J. von Wright. [5] The theory was
formalised in the HOL theorem prover, while specific refinement rules were proved as
HOL theorems. The HOL Window Inference library[11] has been used to to facilitate
transformational reasoning. The library allows us to focus on and transform a particular
part of a model, while guaranteeing that the transformation, if applicable, will produce
a valid refinement of the entire model.
A similar framework consisting of refinement rules (called tactics) and the tool
support for their application has been developed by Oliveira, Cavalcanti, and Wood-
cock [17]. The framework (called ArcAngel) provides support for the C.Morgan's ver-
sion of the Refinement Calculus. The obvious disadvantage of both these frameworks is
that the refinement rules that can be applied usually describe small, localised transfor-
mations. An attempt to perform several transformations on independent parts of the
model at once, would require deriving and discharging additional proof obligations
about the context surrounding transformed parts, that are rather hard to generalise.
However, while implementing our tool, we found the idea of using the transformational
approach for model refinement very useful.
 
Search WWH ::




Custom Search