|
|
Technical Report HW-MACS-TR-0092
| Title |
Refinement Plans for Informed Formal Design |
| Authors |
Gudmund Grov, Andrew Ireland and Maria Teresa Llano |
|---|
| Date |
2012-02-10 |
| 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.
|
| Group |
DSG |
| Notes |
|
| Download |
 
|
|
|
