Refinement plans for informed formal design

Gudmund Grov, Andrew Ireland, Maria Teresa Llano Rodriguez

Research output: Chapter in Book/Report/Conference proceedingConference contribution

9 Citations (Scopus)


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 topdown 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.
Original languageEnglish
Title of host publicationAbstract State Machines, Alloy, B, VDM, and Z
Place of PublicationBerlin
Number of pages15
Publication statusPublished - 2012
EventAbstract State Machines, Alloy, B, VDM, and Z Third International Conference - Pisa, Italy
Duration: 18 Jun 201221 Jun 2012

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Verlag


ConferenceAbstract State Machines, Alloy, B, VDM, and Z Third International Conference


Dive into the research topics of 'Refinement plans for informed formal design'. Together they form a unique fingerprint.

Cite this