Discovery of invariants through automated theory formation

Maria Teresa Llano Rodriguez, Andrew Ireland, Alison Pease

Research output: Contribution to journalArticle

5 Citations (Scopus)
20 Downloads (Pure)

Abstract

Refinement is a powerful mechanism for mastering the complexities that arise when formally modelling systems. Refinement also bringswith it additional proof obligations -- requiring a developer to discover properties relating to their design decisions. With the goal of reducing this burden, we have investigated howa general purpose automated theory formation tool, HR, can be used to automate the discovery of such properties within the context ofthe Event-B formal modelling framework. This gave rise to an integrated approach to automatedinvariant discovery. In addition to formal modelling and automatedtheory formation, our approach relies upon the simulation of systemmodels as a key input to the invariant discovery process. Moreover we have developed a set of heuristics which, when coupled with automated proof-failure analysis, have enabled us to effectively tailor HR to the needs of Event-B developments. Drawing in part upon case study material from the literature, we have achieved some promising experimental results. While our focus has been on Event-B, we believe that our approach could be applied more widely to formal modelling frameworks which support simulation.
Original languageEnglish
Pages (from-to)203–249
Number of pages47
JournalFormal Aspects of Computing
Volume26
Issue number2
Early online date20 Dec 2012
DOIs
Publication statusPublished - Mar 2014

Fingerprint Dive into the research topics of 'Discovery of invariants through automated theory formation'. Together they form a unique fingerprint.

Cite this