Tech Reports Home Contact
Technical Report Series
Browse Reports
Information for Authors
Contact Details

Technical Report HW-MACS-TR-NNNN

Title Discovery of Invariants through Automated Theory Formation
Authors Maria Teresa Llano, Andrew Ireland and Alison Pease
Date 2012-02-10
Abstract Refinement is a powerful mechanism for mastering the complexities that arise when formally modelling systems. Refinement also brings with 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 how a general purpose automated theory formation tool, HR, can be used to automate the discovery of such properties within the context of the Event-B formal modelling framework. This gave rise to an integrated approach to automated invariant discovery. In addition to formal modelling and automated theory formation, our approach relies upon the simulation of system models 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. In addition, we present initial findings from a comparative study with Daikon -- a likely program invariant discovery system, and briefly describe other automated theory formation systems which might be applied to automated invariant discovery. 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.
Group DSG
Email Technical Report's Administrator
|MACS Home| Top of the Page

Department of Computer Science, Heriot-Watt University, Riccarton, Edinburgh, EH14 4AS, +44 (0) 131 4514152

Last Updated: 02 September 2003 Copyright Heriot-Watt University, Disclaimer