- 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)},
- }
|