• TUCS Publication Series
• How to Publish in TUCS Series
• Publication Search
• Publication Graph
• Publication Input
• Publication Input Guide
• JuFo Browser

Patterns for Refinement Automation

Alexei Iliasov, Elena Troubitsyna, Linas Laibinis, Alexander Romanovsky, Patterns for Refinement Automation. In: Frank de Boer, Marcello Bonsangue, Stefan Hallerstede, Michael Leuschel (Eds.), Post-proceedings of FMCO 2009, Symposium on Formal Methods for Components and Objects 2009, Lecture Notes for Computer Science, Springer, 2010.

Abstract:

Formal modelling is indispensable for engineering highly dependable systems. However, a
wider acceptance of formal methods is hindered by their insufficient 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 typical 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 prototype of such a tool and
some examples of refinement patterns for automated development in the Event B formalism.

BibTeX entry:

@INPROCEEDINGS{inpIlTrLaRo10a,
  title = {Patterns for Refinement Automation},
  booktitle = {Post-proceedings of FMCO 2009, Symposium on Formal Methods for Components and Objects 2009},
  author = {Iliasov, Alexei and Troubitsyna, Elena and Laibinis, Linas and Romanovsky, Alexander},
  editor = {de Boer, Frank and Bonsangue, Marcello and Hallerstede, Stefan and Leuschel, Michael},
  publisher = {Lecture Notes for Computer Science, Springer},
  year = {2010},
}

Belongs to TUCS Research Unit(s): Distributed Systems Laboratory (DS Lab)

Edit publication