Informatics Report Series


Report   

EDI-INF-RR-1371


Related Pages

Report (by Number) Index
Report (by Date) Index
Author Index
Institute Index

Home
Title:Automatic Guidance for Refinement Based Formal Methods
Authors: Maria Teresa Llano ; Gudmund Grov ; Andrew Ireland
Date:Apr 2010
Publication Title:AFM10 (Automated Formal Methods)
Publication Type:Other Publication Status:Submitted
Abstract:
Refinement is a technique used to model systems at different abstraction levels to handle the complexity of large systems. It is used in many different methods, and independent of the method applied, many users find it difficult to identify the correct level of abstraction and steps of refinements. To achieve a correct refinement, the step has to be justified -- often by formal proof. Such proofs represent an additional challenge, typically requiring a user to understand the relationship between modelling and reasoning. To address these challenges, we introduce the notion of refinement plans, a technique that combines proof and modelling patterns of refinement, with the aim of automatically providing modelling guidance when refinement fails.
Copyright:
2010 by The University of Edinburgh. All Rights Reserved
Links To Paper
No links available
Bibtex format
@Misc{EDI-INF-RR-1371,
author = { Maria Teresa Llano and Gudmund Grov and Andrew Ireland },
title = {Automatic Guidance for Refinement Based Formal Methods},
year = 2010,
month = {Apr},
note = {AFM10 (Automated Formal Methods)},
}


Home : Publications : Report 

Please mail <reports@inf.ed.ac.uk> with any changes or corrections.
Unless explicitly stated otherwise, all material is copyright The University of Edinburgh