Refinement plans for informed formal design

Gudmund Grov, Andrew Ireland, Maria Teresa Llano

Research output: Chapter in Book/Report/Conference proceedingConference PaperResearchpeer-review

7 Citations (Scopus)

Abstract

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.

Original languageEnglish
Title of host publicationAbstract State Machines, Alloy, B, VDM, and Z - Third International Conference, ABZ 2012, Proceedings
Pages208-222
Number of pages15
DOIs
Publication statusPublished - 23 Jul 2012
Externally publishedYes
Event3rd International Conference on Abstract State Machines, Alloy, B, VDM, and Z, ABZ 2012 - Pisa, Italy
Duration: 18 Jun 201221 Jun 2012

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume7316 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference3rd International Conference on Abstract State Machines, Alloy, B, VDM, and Z, ABZ 2012
CountryItaly
CityPisa
Period18/06/1221/06/12

Cite this