Refinement plans for informed formal design

Gudmund Grov, Andrew Ireland, Maria Teresa Llano Rodriguez

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

6 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

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

  • Cite this

    Grov, G., Ireland, A., & Llano Rodriguez, M. T. (2012). Refinement plans for informed formal design. In Abstract State Machines, Alloy, B, VDM, and Z (Vol. 7316, pp. 208-222). (Lecture Notes in Computer Science). Springer.