Reasoned Modelling Critics: Turning Failed Proofs into Modelling Guidance

Andrew Ireland, Gudmund Grov, Michael J. Butler
Digital Printed Abstract View Cite
Type
Conference paper
Publication
2nd International Conference on ASM, Alloy, B, and Z (ABZ'10)

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.

Document

If you cannot see the document below, the PDF document is most likely not freely accessible. In this case, please try to access the document via this link.

Reference

% BibTex
@inproceedings{IrelandGB10,
  author       = {Andrew Ireland and
                  Gudmund Grov and
                  Michael J. Butler},
  editor       = {Marc Frappier and
                  Uwe Gl{\"{a}}sser and
                  Sarfraz Khurshid and
                  R{\'{e}}gine Laleau and
                  Steve Reeves},
  title        = {Reasoned Modelling Critics: Turning Failed Proofs into Modelling Guidance},
  booktitle    = {Abstract State Machines, Alloy, {B} and Z, Second International Conference,
                  {ABZ} 2010, Orford, QC, Canada, February 22-25, 2010. Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {5977},
  pages        = {189--202},
  publisher    = {Springer},
  year         = {2010},
  url          = {https://doi.org/10.1007/978-3-642-11811-1\_15},
  doi          = {10.1007/978-3-642-11811-1\_15},
  timestamp    = {Sun, 02 Jun 2019 21:23:59 +0200},
  biburl       = {https://dblp.org/rec/conf/asm/IrelandGB10.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}
ABZ'10

Related