Reasoned modelling critics: turning failed proofs into modelling guidance

Andrew Ireland, Gudmund Grov, Michael Butler

Research output: Chapter in Book/Report/Conference proceedingConference contribution

5 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 languageEnglish
Title of host publicationAbstract State Machines, Alloy, B and Z
Subtitle of host publicationProceedings of the Second International Conference, ABZ 2010, Orford, QC, Canada, February 22-25, 2010
EditorsMarc Frappier, Uwe Glässer, Sarfraz Khurshid, Régine Laleau, Steve Reeves
PublisherSpringer
Pages189-202
Number of pages14
ISBN (Electronic)978-3-642-11811-1
ISBN (Print)978-3-642-11810-4
DOIs
Publication statusPublished - 2010
Event2nd International Conference on Abstract State Machines, Alloy, B and Z - Orford, QC, Canada
Duration: 22 Feb 201025 Feb 2010

Publication series

NameLecture Notes in Computer Science
Volume5977
ISSN (Print)0302-9743

Conference

Conference2nd International Conference on Abstract State Machines, Alloy, B and Z
Abbreviated titleABZ 2010
CountryCanada
CityOrford, QC
Period22/02/1025/02/10

Fingerprint Dive into the research topics of 'Reasoned modelling critics: turning failed proofs into modelling guidance'. Together they form a unique fingerprint.

Cite this