Toggle Main Menu Toggle Search

Open Access padlockePrints

The Theory and Practice of Refinement-After-Hiding

Lookup NU author(s): Dr Jonathan Burton

Downloads


Abstract

In software or hardware development, we take an abstract view of a process or system - i.e. a specification - and proceed to render it in a more implementable form. The relationship between an implementation and its specification is characterised in the context of formal verification using a notion called refinement: this notion provides a correctness condition which must be met before we can say that a particular implementation is correct with respect to a particular specification. For a notion of refinement to be useful, it should reflect the ways in which we might want to make concrete our abstract specification. In process algebras, the notion that a process Q implements or refines a process P is based on the idea that Q is more deterministic than P: this means that every behaviour of the implementation must be possible for the specification. Consider the case that we build a (specification) network from a set of (specification) component processes, where communications or interactions between these processes are hidden. The abstract behaviour which constitutes these communications or interactions may be implemented using a particular protocol, replication of communication channels to mask possible faults or perhaps even parallel access to data structures to increase performance. These concrete behaviours will be hidden in the construction of the final implementation network and so the correctness of the final network may be considered using standard notions of refinement. However, we cannot directly verify the correctness of component processes in the general case, precisely because we may have done more than simply increase determinism in the move from specification to implementation component. Standard (process algebraic) refinement does not, therefore, fully reflect the ways in which we may wish to move from the abstract to the concrete at the level of such components. This has implications both in terms of the state explosion problem and also in terms of verifying in isolation the correctness of a component which may be used in a number of different contexts. We therefore introduce a more powerful notion of refinement, which we shall call refinement-after-hiding: this gives us the power to approach verification compositionally even though the behaviours of an implementation component may not be contained in those of the corresponding specification, provided that the (parts of the) behaviours which are different will be hidden in the construction of the final network. We explore both the theory and practice of this new notion and also present a means for its automatic verification. Finally, we use the notion of refinement-after-hiding, along with the means of verification, to verify the correctness of an important algorithm for asynchronous communication. The nature of the verification and the results achieved are completely new and quite significant.


Publication metadata

Author(s): Burton J

Publication type: Report

Publication status: Published

Series Title: School of Computing Science Technical Report Series

Year: 2005

Pages: 365

Print publication date: 01/04/2005

Source Publication Date: April 2005

Report Number: 904

Institution: School of Computing Science, University of Newcastle upon Tyne

Place Published: Newcastle upon Tyne

URL: http://www.cs.ncl.ac.uk/publications/trs/papers/904.pdf


Share