Where academic tradition
meets the exciting future

Formal Refinement Automation

Alexei Iliasov, Elena Troubitsyna, Alexander Romanovsky, Linas Laibinis, Formal Refinement Automation. In: Muffy Calder Alice Miller (Ed.), Proceedings of Eighth International Workshop on Automated Verification of Critical Systems (AVOCS 2008), ENTCS, 2008.

Abstract:

Formal methods focus on a posteriori analysis and a modeller gets little assistance in
constructing a model which makes formal modelling more expensive and laborious than it could
be. In this paper we discuss a mechanism for automation of formal refinement based on reusable
refinement steps, called refinement patterns. Refinement patterns offer a constructive top-down
approach to formal modelling; for many patterns, correctness can be proved once-for-all. The
approach is illustrated with the discussion of Event-B refinement patterns and a tool supporting
pattern-based Event-B developments.

BibTeX entry:

@INPROCEEDINGS{inpIlTrRoLa08a,
  title = {Formal Refinement Automation},
  booktitle = {Proceedings of Eighth International Workshop on Automated Verification of Critical Systems (AVOCS 2008)},
  author = {Iliasov, Alexei and Troubitsyna, Elena and Romanovsky, Alexander and Laibinis, Linas},
  editor = {Alice Miller, Muffy Calder},
  publisher = {ENTCS},
  year = {2008},
}

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

Edit publication