Show simple item record

dc.contributor.advisorIreland, Professor Andrew
dc.contributor.advisorGrov, Gudmund
dc.contributor.advisorPooley, Professor Robert J
dc.contributor.authorLlano Rodriguez, Maria Teresa
dc.date.accessioned2014-06-09T16:39:13Z
dc.date.available2014-06-09T16:39:13Z
dc.date.issued2013-05
dc.identifier.urihttp://hdl.handle.net/10399/2685
dc.description.abstractThe continuous growth of complex systems makes the development of correct software increasingly challenging. In order to address this challenge, formal methods o er rigorous mathematical techniques to model and verify the correctness of systems. Refinement is one of these techniques. By allowing a developer to incrementally introduce design details, refinement provides a powerful mechanism for mastering the complexities that arise when formally modelling systems. Here the focus is on a posit-and-prove style of refinement, where a design is developed as a series of abstract models introduced via refinement steps. Each refinement step generates proof obligations which must be discharged in order to verify its correctness – typically requiring a user to understand the relationship between modelling and reasoning. This thesis focuses on techniques to aid refinement-based formal modelling, specifically, when a user requires guidance in order to overcome a failed refinement step. An integrated approach has been followed: combining the complementary strengths of bottomup theory formation, in which theories about domains are built based on basic background information; and top-down planning, in which meta-level reasoning is used to guide the search for correct models. On the theory formation perspective, we developed a technique for the automatic discovery of invariants. Refinement requires the definition of properties, called invariants, which relate to the design. Formulating correct and meaningful invariants can be tedious and a challenging task. A heuristic approach to the automatic discovery of invariants has been developed building upon simulation, proof-failure analysis and automated theory formation. This approach exploits the close interplay between modelling and reasoning in order to provide systematic guidance in tailoring the search for invariants for a given model. On the planning perspective, we propose a new technique called refinement plans. Refinement plans provide a basis for automatically generating modelling guidance when a step fails but is close to a known pattern of refinement. This technique combines both modelling and reasoning knowledge, and, contrary to traditional pattern techniques, allow the analysis of failure and partial matching. Moreover, when the guidance is only partially instantiated, and it is suitable, refinement plans provide specialised knowledge to further tailor the theory formation process in an attempt to fully instantiate the guidance. We also report on a series of experiments undertaken in order to evaluate the approaches and on the implementation of both techniques into prototype tools. We believe the techniques presented here allow the developer to focus on design decisions rather than on analysing low-level proof failures.en_US
dc.language.isoenen_US
dc.publisherHeriot-Watt Universityen_US
dc.publisherMathematical and Computer Sciencesen_US
dc.rightsAll items in ROS are protected by the Creative Commons copyright license (http://creativecommons.org/licenses/by-nc-nd/2.5/scotland/), with some rights reserved.
dc.titleInvariant discovery and refinement plans for formal modelling in Event-Ben_US
dc.typeThesisen_US


Files in this item

Thumbnail

This item appears in the following Collection(s)

Show simple item record