Reasoned modelling critics: turning failed proofs into modelling guidance

Andrew Ireland; Gudmund Grov; Michael Butler

doi:10.1007/978-3-642-11811-1_15

Reasoned modelling critics: turning failed proofs into modelling guidance

Andrew Ireland, Gudmund Grov, Michael Butler

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

6 Citations (Scopus)

Abstract

The activities of formal modelling and reasoning are closely related. But while the rigour of building formal models brings significant benefits, formal reasoning remains a major barrier to the wider acceptance of formalism within design. Here we propose reasoned modelling critics – a technique which aims to abstract away from the complexities of low-level proof obligations, and provide high-level modelling guidance to designers when proofs fail. Inspired by proof planning critics, the technique combines proof-failure analysis with modelling heuristics. Here, we present the details of our proposal and outline future plans.

Original language	English
Title of host publication	Abstract State Machines, Alloy, B and Z
Subtitle of host publication	Proceedings of the Second International Conference, ABZ 2010, Orford, QC, Canada, February 22-25, 2010
Editors	Marc Frappier, Uwe Glässer, Sarfraz Khurshid, Régine Laleau, Steve Reeves
Publisher	Springer
Pages	189-202
Number of pages	14
ISBN (Electronic)	978-3-642-11811-1
ISBN (Print)	978-3-642-11810-4
DOIs	https://doi.org/10.1007/978-3-642-11811-1_15
Publication status	Published - 2010
Event	2nd International Conference on Abstract State Machines, Alloy, B and Z - Orford, QC, Canada Duration: 22 Feb 2010 → 25 Feb 2010

Publication series

Name	Lecture Notes in Computer Science
Volume	5977
ISSN (Print)	0302-9743

Conference

Conference	2nd International Conference on Abstract State Machines, Alloy, B and Z
Abbreviated title	ABZ 2010
Country/Territory	Canada
City	Orford, QC
Period	22/02/10 → 25/02/10

Access to Document

10.1007/978-3-642-11811-1_15

Cite this

Ireland, A., Grov, G., & Butler, M. (2010). Reasoned modelling critics: turning failed proofs into modelling guidance. In M. Frappier, U. Glässer, S. Khurshid, R. Laleau, & S. Reeves (Eds.), Abstract State Machines, Alloy, B and Z: Proceedings of the Second International Conference, ABZ 2010, Orford, QC, Canada, February 22-25, 2010 (pp. 189-202). (Lecture Notes in Computer Science; Vol. 5977). Springer. https://doi.org/10.1007/978-3-642-11811-1_15

Ireland, Andrew ; Grov, Gudmund ; Butler, Michael. / Reasoned modelling critics : turning failed proofs into modelling guidance. Abstract State Machines, Alloy, B and Z: Proceedings of the Second International Conference, ABZ 2010, Orford, QC, Canada, February 22-25, 2010. editor / Marc Frappier ; Uwe Glässer ; Sarfraz Khurshid ; Régine Laleau ; Steve Reeves. Springer, 2010. pp. 189-202 (Lecture Notes in Computer Science).

@inproceedings{0932d4b78b1e48049aee416857b4df08,

title = "Reasoned modelling critics: turning failed proofs into modelling guidance",

abstract = "The activities of formal modelling and reasoning are closely related. But while the rigour of building formal models brings significant benefits, formal reasoning remains a major barrier to the wider acceptance of formalism within design. Here we propose reasoned modelling critics – a technique which aims to abstract away from the complexities of low-level proof obligations, and provide high-level modelling guidance to designers when proofs fail. Inspired by proof planning critics, the technique combines proof-failure analysis with modelling heuristics. Here, we present the details of our proposal and outline future plans.",

author = "Andrew Ireland and Gudmund Grov and Michael Butler",

year = "2010",

doi = "10.1007/978-3-642-11811-1_15",

language = "English",

isbn = "978-3-642-11810-4",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "189--202",

editor = "Frappier, {Marc } and Gl{\"a}sser, {Uwe } and Khurshid, {Sarfraz } and Laleau, {R{\'e}gine } and Reeves, {Steve }",

booktitle = "Abstract State Machines, Alloy, B and Z",

note = "2nd International Conference on Abstract State Machines, Alloy, B and Z, ABZ 2010 ; Conference date: 22-02-2010 Through 25-02-2010",

}

Ireland, A, Grov, G & Butler, M 2010, Reasoned modelling critics: turning failed proofs into modelling guidance. in M Frappier, U Glässer, S Khurshid, R Laleau & S Reeves (eds), Abstract State Machines, Alloy, B and Z: Proceedings of the Second International Conference, ABZ 2010, Orford, QC, Canada, February 22-25, 2010. Lecture Notes in Computer Science, vol. 5977, Springer, pp. 189-202, 2nd International Conference on Abstract State Machines, Alloy, B and Z, Orford, QC, Canada, 22/02/10. https://doi.org/10.1007/978-3-642-11811-1_15

Reasoned modelling critics: turning failed proofs into modelling guidance. / Ireland, Andrew; Grov, Gudmund; Butler, Michael.
Abstract State Machines, Alloy, B and Z: Proceedings of the Second International Conference, ABZ 2010, Orford, QC, Canada, February 22-25, 2010. ed. / Marc Frappier; Uwe Glässer; Sarfraz Khurshid; Régine Laleau; Steve Reeves. Springer, 2010. p. 189-202 (Lecture Notes in Computer Science; Vol. 5977).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

TY - GEN

T1 - Reasoned modelling critics

T2 - 2nd International Conference on Abstract State Machines, Alloy, B and Z

AU - Ireland, Andrew

AU - Grov, Gudmund

AU - Butler, Michael

PY - 2010

Y1 - 2010

N2 - The activities of formal modelling and reasoning are closely related. But while the rigour of building formal models brings significant benefits, formal reasoning remains a major barrier to the wider acceptance of formalism within design. Here we propose reasoned modelling critics – a technique which aims to abstract away from the complexities of low-level proof obligations, and provide high-level modelling guidance to designers when proofs fail. Inspired by proof planning critics, the technique combines proof-failure analysis with modelling heuristics. Here, we present the details of our proposal and outline future plans.

AB - The activities of formal modelling and reasoning are closely related. But while the rigour of building formal models brings significant benefits, formal reasoning remains a major barrier to the wider acceptance of formalism within design. Here we propose reasoned modelling critics – a technique which aims to abstract away from the complexities of low-level proof obligations, and provide high-level modelling guidance to designers when proofs fail. Inspired by proof planning critics, the technique combines proof-failure analysis with modelling heuristics. Here, we present the details of our proposal and outline future plans.

U2 - 10.1007/978-3-642-11811-1_15

DO - 10.1007/978-3-642-11811-1_15

M3 - Conference contribution

SN - 978-3-642-11810-4

T3 - Lecture Notes in Computer Science

SP - 189

EP - 202

BT - Abstract State Machines, Alloy, B and Z

A2 - Frappier, Marc

A2 - Glässer, Uwe

A2 - Khurshid, Sarfraz

A2 - Laleau, Régine

A2 - Reeves, Steve

PB - Springer

Y2 - 22 February 2010 through 25 February 2010

ER -

Ireland A, Grov G, Butler M. Reasoned modelling critics: turning failed proofs into modelling guidance. In Frappier M, Glässer U, Khurshid S, Laleau R, Reeves S, editors, Abstract State Machines, Alloy, B and Z: Proceedings of the Second International Conference, ABZ 2010, Orford, QC, Canada, February 22-25, 2010. Springer. 2010. p. 189-202. (Lecture Notes in Computer Science). doi: 10.1007/978-3-642-11811-1_15

Reasoned modelling critics: turning failed proofs into modelling guidance

Abstract

Publication series

Conference

Access to Document

Fingerprint

Cite this