Information Technology Reference
In-Depth Information
semantic conditions that should be fulfilled by the model to be eligible for a refinement
pattern application. The second part contains definition of syntactic manipulations over
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.
Application of refinement patterns is compositional. Hence some large model trans-
formation steps can be represented by a certain combination of refinement patterns, and
therefore can also be seen as refinement patterns per se. A possibility to compose pat-
terns significantly improves scalability of formal modelling. Moreover, reducing execu-
tion of a refinement step to a number of syntactic manipulations over a model provides
a basis for automation. Finally, our approach can potentially support reuse of not only
models but also proofs. Indeed, by proving that an application of a generic pattern pro-
duces a valid refinement of a generic model, we at the same time verify the correctness
of such a transformation for any of its instances. This might significantly reduce or even
avoid proving activity in a concrete development.
The theoretical work on defining refinement patterns presented in this paper estab-
lished a basis for building a prototype tool for automating refinement process in Event
B[13]. The tool has been developed as a plug-in for the RODIN platform [1] - an open
toolset for supporting modelling and refinement in the Event B framework. We be-
lieve that, by creating a large library of refinement patterns and providing automated
tool support for pattern matching and instantiation, we will make formal modelling and
verification more accessible for software engineers and hence facilitate integration of
formal methods into software engineering practice.
2
Towards Refinement Automation
In this paper we focus on automating the formal development process based on model
refinement. We start this section by giving a short overview on the notion of refinement
and the techniques allowing us facilitate the refinement process. Then we proceed by
describing our chosen formal framework - Event B.
2.1
Formal Development by Refinement
System development by refinement is a formal model-driven development process. Re-
finement allows us to ensure that a refined, i.e., more elaborated, model retains all the
essential properties of its abstract counterpart. Since refinement is transitive, the model-
driven refinement-based development process enables development of systems that are
correct-by-construction.
The precise definition of refinement depends on the chosen modelling framework
and hence might have different semantics and degree of rigor. The foundations of formal
reasoning about correctness and stepwise development by refinement were established
by Dijkstra [9] and Hoare [12], and then further developed by Back and von Wright [5]
as well as Morgan [16].
In the refinement calculus framework, a model is represented by a composition of
abstract statements. Formally, we say that the statement
S
is refined by the statement
