Information Technology Reference
In-Depth Information
Patterns for Refinement Automation
Alexei Iliasov
1
, Elena Troubitsyna
2
, Linas Laibinis
2
, and Alexander Romanovsky
1
1
Newcastle University, UK
2
Abo Akademi University, Finland
{
alexei.iliasov,alexander.romanovsky
}
@ncl.ac.uk,
{
linas.laibinis,elena.troubitsyna
}
@abo.fi
Abstract.
Formal modelling is indispensable for engineering highly dependable
systems. However, a wider acceptance of formal methods is hindered by their in-
sufficient usability and scalability. In this paper, we aim at assisting developers in
rigorous modelling and design by increasing automation of development steps.
We introduce a notion of refinement patterns - generic representations of typi-
cal correctness-preserving model transformations. Our definition of a refinement
pattern contains a description of syntactic model transformations, as well as the
pattern applicability conditions and proof obligations for verifying correctness
preservation. This work establishes a basis for building a tool that would support
formal system development via pattern reuse and instantiation. We present a pro-
totype of such a tool and some examples of refinement patterns for automated
development in the Event B formalism.
1
Introduction
Over the recent years model-driven development has become a leading paradigm in
software engineering. System development by stepwise refinement is a
formal
model-
driven development approach that advocates development of systems correct by con-
struction. Development starts from an abstract model, which is gradually transformed
into a specification closely resembling an implementation. Each model transformation
step, called a
refinement
step, allows a designer to incorporate implementation details
into the model. Correctness of refinement steps is validated by mathematical proofs.
The refinement approach significantly reduces the required testing efforts and, at the
same time, supports a clear traceability of system properties through various abstrac-
tion levels. However, it is still poorly integrated into the existing software engineering
process. Among the main reasons hindering its application are complexity of carrying
proofs, lack of expertise in abstract modelling, and insufficient scalability.
In this paper we propose an approach that aims at facilitating integration of formal
methods into the existing development practice by leveraging automation of refinement
process and increasing reuse of models and proofs. We aim at automating certain model
transformation steps via instantiation and reuse of prefabricated solutions, which we
call
refinement patterns
. Such patterns generalise certain typical model transformations
reoccurring in a particular development method. They can be thought of as “refinement
rules in large”.
In general, a refinement pattern is a generic model transformer. Essentially it consists
of three parts. The first part is the pattern applicability conditions, i.e., the syntactic and
