Article ID Journal Published Year Pages File Type
433416 Science of Computer Programming 2013 17 Pages PDF
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 — 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.

Related Topics
Physical Sciences and Engineering Computer Science Computational Theory and Mathematics
Authors
, , , ,