Contexts, refinement and determinism

In this paper we have been influenced by those who take an “engineering view” of the problem of designing systems, i.e. a view that is motivated by what someone designing a real system will be concerned with, and what questions will arise as they work on their design. Specifically, we have borrowed from the testing work of Hennessy, de Nicola and van Glabbeek, e.g. Hennessy, 1988 [13], de Nicola [5], de Nicola, 1992 [21] and van Glabbeek, 2001, 1990 [40] and [39].Here we concentrate on one fundamental part of the engineering view and where consideration of it leads. The aspects we are concerned with are computational entities in contexts, observed by users. This leads to formalising design steps that are often left informal, and that in turn gives insights into non-determinism and ultimately leads to being able to use refinement in situations where existing techniques fail.

Research highlights► We show how considering interfaces of entities, contexts and users gives clarity. ► We show how it relates to characterisations of systems via a notion of testing. ► We give examples of five refinement relations as instances of a general model. ► An example is refinement between broadcast and interactive branching programs. ► Refinement moves from abstract to concrete, preserving certain valuable guarantees.