Tech Reports Home Contact
Technical Report Series
Submit Report
Browse Reports
Information for Authors
Contact Details

Technical Report HW-MACS-TR-0076

TitleAutomatic Guidance for Refinement Based Formal Methods
AuthorsMaria Teresa Llano, Gudmund Grov, Andrew Ireland
AbstractRefinement 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.


Email Technical Report's Administrator
|MACS Home| Top of the Page

Department of Computer Science, Heriot-Watt University, Riccarton, Edinburgh, EH14 4AS, +44 (0) 131 4514152

Last Updated: 02 September 2003 Copyright Heriot-Watt University, Disclaimer