Discovery of invariants through automated theory formation

Maria Teresa Llano, Andrew Ireland, Alison Pease

Research output: Contribution to journalConference article

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 languageEnglish
Pages (from-to)1-19
Number of pages19
JournalElectronic Proceedings in Theoretical Computer Science, EPTCS
Volume55
DOIs
Publication statusPublished - 17 Jun 2011
Event15th International Refinement Workshop, Refine 2011 - Limerick, Ireland
Duration: 20 Jun 2011 → …

Fingerprint

Failure analysis
Experiments

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 = "6",
day = "17",
doi = "10.4204/EPTCS.55.1",
language = "English",
volume = "55",
pages = "1--19",
journal = "Electronic Proceedings in Theoretical Computer Science",
issn = "2075-2180",
publisher = "Open Publishing Association",

}

Discovery of invariants through automated theory formation. / Llano, Maria Teresa; Ireland, Andrew; Pease, Alison.

In: Electronic Proceedings in Theoretical Computer Science, EPTCS, Vol. 55, 17.06.2011, p. 1-19.

Research output: Contribution to journalConference article

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

VL - 55

SP - 1

EP - 19

JO - Electronic Proceedings in Theoretical Computer Science

JF - Electronic Proceedings in Theoretical Computer Science

SN - 2075-2180

ER -