Refinement is a powerful technique for tackling the complexities that arise when formally modelling systems. Here we focus on a posit-and-prove style of refinement, and specifically where a user requires guidance in order to overcome a failed refinement step. We take an integrated approach – combining the complementary strengths of top-down planning and bottom-up theory formation. In this paper we focus mainly on the planning perspective. Specifically, we propose a new technique called refinement plans which combines both modelling and reasoning perspectives. When a refinement step fails, refinement plans provide a basis for automatically generating modelling guidance by abstracting away from the details of low-level proof failures. The refinement plans described here are currently being implemented for the Event-B modelling formalism, and have been assessed on paper using case studies drawn from the literature. Longer-term, our aim is to identify refinement plans that are applicable to a range of modelling formalisms.
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.
% BibTex
@inproceedings{GrovIL12,
author = {Gudmund Grov and
Andrew Ireland and
Maria Teresa Llano},
editor = {John Derrick and
John S. Fitzgerald and
Stefania Gnesi and
Sarfraz Khurshid and
Michael Leuschel and
Steve Reeves and
Elvinia Riccobene},
title = {Refinement Plans for Informed Formal Design},
booktitle = {Abstract State Machines, Alloy, B, VDM, and {Z} - Third International
Conference, {ABZ} 2012, Pisa, Italy, June 18-21, 2012. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {7316},
pages = {208--222},
publisher = {Springer},
year = {2012},
url = {https://doi.org/10.1007/978-3-642-30885-7\_15},
doi = {10.1007/978-3-642-30885-7\_15},
timestamp = {Sun, 02 Jun 2019 21:23:59 +0200},
biburl = {https://dblp.org/rec/conf/asm/GrovIL12.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}