Discovery of invariants through automated theory formation

Maria Teresa Llano; Andrew Ireland; Alison Pease

doi:10.4204/EPTCS.55.1

Discovery of invariants through automated theory formation

Maria Teresa Llano, Andrew Ireland, Alison Pease

Computing

Research output: Contribution to journal › Conference article › peer-review

5 Citations (Scopus)

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 theory formation tool, HR, can be used to automate the discovery of such properties within the context of Event-B. Here we develop a heuristic approach to the automatic discovery of invariants and report upon a series of experiments that we undertook in order to evaluate our approach. The set of heuristics developed provides systematic guidance in tailoring HR for a given Event-B development. These heuristics are based upon proof-failure analysis, and have given rise to some promising results.

Original language	English
Pages (from-to)	1-19
Number of pages	19
Journal	Electronic Proceedings in Theoretical Computer Science, EPTCS
Volume	55
DOIs	https://doi.org/10.4204/EPTCS.55.1
Publication status	Published - 17 Jun 2011
Event	15th International Refinement Workshop, Refine 2011 - Limerick, Ireland Duration: 20 Jun 2011 → …

ASJC Scopus subject areas

Software

Access to Document

10.4204/EPTCS.55.1

Cite this

@article{24d9dd755a7b4533a57eb10738db0094,

title = "Discovery of invariants through automated theory formation",

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 theory formation tool, HR, can be used to automate the discovery of such properties within the context of Event-B. Here we develop a heuristic approach to the automatic discovery of invariants and report upon a series of experiments that we undertook in order to evaluate our approach. The set of heuristics developed provides systematic guidance in tailoring HR for a given Event-B development. These heuristics are based upon proof-failure analysis, and have given rise to some promising results.",

author = "Llano, {Maria Teresa} and Andrew Ireland and Alison Pease",

year = "2011",

month = jun,

day = "17",

doi = "10.4204/EPTCS.55.1",

language = "English",

volume = "55",

pages = "1--19",

journal = "Electronic Proceedings in Theoretical Computer Science, EPTCS",

issn = "2075-2180",

publisher = "Open Publishing Association",

note = "15th International Refinement Workshop, Refine 2011 ; Conference date: 20-06-2011",

}

TY - JOUR

T1 - Discovery of invariants through automated theory formation

AU - Llano, Maria Teresa

AU - Ireland, Andrew

AU - Pease, Alison

PY - 2011/6/17

Y1 - 2011/6/17

N2 - 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 theory formation tool, HR, can be used to automate the discovery of such properties within the context of Event-B. Here we develop a heuristic approach to the automatic discovery of invariants and report upon a series of experiments that we undertook in order to evaluate our approach. The set of heuristics developed provides systematic guidance in tailoring HR for a given Event-B development. These heuristics are based upon proof-failure analysis, and have given rise to some promising results.

AB - 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 theory formation tool, HR, can be used to automate the discovery of such properties within the context of Event-B. Here we develop a heuristic approach to the automatic discovery of invariants and report upon a series of experiments that we undertook in order to evaluate our approach. The set of heuristics developed provides systematic guidance in tailoring HR for a given Event-B development. These heuristics are based upon proof-failure analysis, and have given rise to some promising results.

UR - http://www.scopus.com/inward/record.url?scp=84889584084&partnerID=8YFLogxK

U2 - 10.4204/EPTCS.55.1

DO - 10.4204/EPTCS.55.1

M3 - Conference article

AN - SCOPUS:84889584084

SN - 2075-2180

VL - 55

SP - 1

EP - 19

JO - Electronic Proceedings in Theoretical Computer Science, EPTCS

JF - Electronic Proceedings in Theoretical Computer Science, EPTCS

T2 - 15th International Refinement Workshop, Refine 2011

Y2 - 20 June 2011

ER -

Discovery of invariants through automated theory formation

Abstract

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Cite this