Reasoned modelling critics: Turning failed proofs into modelling guidance

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 — an approach 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, implement them in a prototype and outline future plans.

► Formalism brings rigour to the design of complex systems.
► Formalism also brings with it the need for proof, and the analysis of failed proofs.
► Proof failure analysis represents a major barrier to mainstream system designers.
► In our work we automate such a failure analysis, and provide design guidance.
► We report on our prototype implementation along with experimental results.