Toggle Main Menu Toggle Search

Open Access padlockePrints

Patterns for Refinement Automation

Lookup NU author(s): Dr Alexei Iliasov, Dr Elena Troubitsyna, Professor Alexander Romanovsky

Downloads


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 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 verification of correctness preservation. This establishes a basis for building a tool supporting 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.


Publication metadata

Author(s): Iliasov A, Troubitsyna E, Laibinis L, Romanovsky A

Publication type: Report

Publication status: Published

Series Title: School of Computing Science Technical Report Series

Year: 2008

Pages: 18

Print publication date: 01/10/2008

Source Publication Date: October 2008

Report Number: 1125

Institution: School of Computing Science, University of Newcastle upon Tyne

Place Published: Newcastle upon Tyne

URL: http://www.cs.ncl.ac.uk/publications/trs/papers/1125.pdf


Share