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. © 2010 Springer.
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. © 2010 Springer.
UR - http://www.scopus.com/inward/record.url?scp=77950797731&partnerID=8YFLogxK
U2 - 10.1007/978-3-642-11811-1_15
DO - 10.1007/978-3-642-11811-1_15
M3 - Conference contribution
SN - 3642118100
SN - 9783642118104
VL - 5977 LNCS
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 189
EP - 202
BT - Abstract State Machines, Alloy, B and Z - Second International Conference, ABZ 2010, Proceedings
Y2 - 22 February 2010 through 25 February 2010
ER -