کد مقاله | کد نشریه | سال انتشار | مقاله انگلیسی | نسخه تمام متن |
---|---|---|---|---|
433416 | 1441706 | 2013 | 17 صفحه PDF | دانلود رایگان |
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.
Journal: Science of Computer Programming - Volume 78, Issue 3, 1 March 2013, Pages 293–309