Refinement of State Based Systems
Research by
part of
the EPSRC RefineNET network
with contributions from Kent collaborators
Ralph Miarka,
Chris Taylor,
Howard Bowman,
and Maarten Steen.
Project
suggestions for future collaborators.
External contributors have been
Graeme Smith,
Gerhard Schellhorn,
Heike Wehrheim, and
Willem-Paul de Roever.
Summary
To investigate the theoretical and methodological aspects of refinement
of state based systems, with an eye towards their usage in describing
distributed systems.
Best recent paper
Book
The research up to 2001 is consolidated into a book
entitled
Refinement
in Z and Object-Z: Foundations and Advanced Applications, which
appeared in May 2001 in
the Springer FACIT series (ISBN 1-85233-245-X).
The book's web page.
An overview of many of the generalisations of refinement discussed
in the book is given in "Liberating Data Refinement", presented at MPC 2000.
A somewhat more recent overview is Recent Advances in Refinement, presented at ASM
2003.
In recent years, we put a significant effort into
Relational Concurrent
Refinement, see below.
Original motivation: Viewpoints (1995-2000)
One could consider the Refinement research a spin-off of our
research in the
Cross
Viewpoint Consistency in Open Distributed Processing ("Consistency")
project (Bowman, Derrick, Boiten, Steen, Linington). In
this project we investigated how to define and check consistency for
specifications consisting of multiple interrelated viewpoints. As our
specification languages we used (Object-)Z and process algebra in the
form of LOTOS. For various reasons, including traceability (see
"
Managing
Inconsistency and Promoting Consistency") it appeared that
development relations between specifications provide a better
basis for consistency checking than the logical definition.
Consistency is defined as the existence of a specification which is a
development of each of the viewpoint specifications.
Of course,
refinement is a prime example of such a development
relation.
A selection of relevant general papers (more on the
Consistency project publications page and on the pages of the follow-on projects
OpenViews and
A Constructive Framework for Partial
Specification):
Refinement as Semantics (1996-2003)
A crucial observation is that if we take consistency to be the existence
of a common development, implicitly we have taken as the semantics of a
specification the collection of all its refinements. In other words: the
refinement relation we use determines what a (partial) specification
means.
A paper investigating these issues is Loose
specification and refinement in Z. Z has both a set-theoretic
semantics and a refinement relation; the two are formally hardly
related, but could they be?
This paper was presented at ZB 2002 "in reverse", concentrating on
"universal" and "existential" parameters of specifications, see
slides.
A consequence of "refinement as semantics"
is that if we want to change our interpretation of
partial specifications, we have to change our refinement relation. A
major part of our subsequent work has been concerned with exactly that.
Work on consistency in UML (to mention a well-known example of a
language where semantics is an open issue) has been strongly based on
this approach, see "A Framework for UML
Consistency" and
"Exploring UML refinement through
Unification".
Constructive Refinement (1995-2003)
One way of establishing constructively that two specifications
are consistent is to exhibit a common development of them.
Moreover, for consistency checking with further specifications, it is
important that this common development is the "most abstract" one. Such
a most abstract (or least developed) common refinement we have called a
unification.
We have investigated unifications for specifications in Z and in LOTOS,
and later also in UML.
- In "Viewpoints and Objects" we
presented an informal construction of unifications for Z. This can also
be found in other early papers of the Consistency project - this one
also connects to the idea of inheritance as refinement.
-
"Constructive consistency checking for partial
specification in Z"
formalises the construction, fills in the
details, and contains the proofs. A previous version has
appeared as
"Consistency and Refinement for Partial
Specification in Z".
- "Coupling Schemas: Data Refinement and
View(point) Composition" explores the relation between unification,
refinement, and "view composition", a simpler syntactic composition
of specifications in Z.
- "Composition of LOTOS Specifications"
demonstrates how, on the other hand, in process algebras, with their
various development relations, it is generally impossible to define
unifications at the syntactic level.
- "Exploring UML refinement through
Unification" compares intuitive UML unifications with the Z
unifications under a simple translation, in order to characterise
properties required for UML refinement.
The papers on Z listed above demonstrate that it is possible to
describe syntactically:
- the least common refinement of two specifications, given a
description of how they relate;
- the least data refinement of a specification, given a relation
between concrete and abstract state spaces.
However, they are restricted to what is called
forwards (or
downwards) simulation refinement. The semantic characterisation of
refinement implies that for completeness one needs
backwards
simulation refinement as well.
It is well known that it is not possible to find a single complete
refinement rule using retrieve relations that link points in the
concrete specification to points in the abstract specification.
However, if we link concrete values to
sets of abstract values
("powersimulations") a single complete rule can be derived.
Constructive Refinement of Tests (1998-2003)
Techniques exist for generating test cases from state based specifications.
In "
Testing Refinements by Refining Tests"
(which won joint best paper at ZUM'98)
we employ the techniques for
calculating data refinements to generate tests for a refined
specification by refining the test for the original specification.
An extended version of this has been published as
"
Testing refinements of state-based formal
specifications".
Testing on the basis of abstraction over input and output is described
in the technical report
Input/Output Abstraction of State Based
Systems.
Relating Behaviour and State, and Weak Refinement (1996-)
Our interest in relating behavioural and state based formalisms also
derives from the Consistency project: specifications may be written
using combinations of behavioural and state based formalisms.
There are essentially two ways of dealing with this.
- In both of these approaches, one needs to ensure compatibility of
semantics. In the viewpoints approach, this boils down to compatibility
of development relations, which is explored in
"Comparing LOTOS and Z Refinement
Relations".
However, Z lacks one important feature of process algebras which is
often needed for specification of concurrent systems: the
internal operation.
- "Weak Refinement in Z" provides an
interpretation of internal operations in Z by defining a "weak"
refinement relation for specifications that may contain internal
operations. An extended version of this, "Specifying and Refining internal operations in Z",
has appeared in Formal Aspects of Computing.
The refinement rules given there are constrained not to introduce
divergence through livelock. More general results are given under the
next heading, of Relational Concurrent Refinement.
The final aspect of relating behaviour and state is the link between
temporal
logics and specifications.
Relational Concurrent Refinement (2002-)
Inspired by the discovery by Bolton and Davies that there is a gap
between traditional Z refinement and failures-divergences refinement, we
have reconstructed failures-divergences refinement from a modified
relational embedding of Z. Observing refusals at finalisation, we
were able to derive the correct simulation rules for
failures-divergences refinement expressed in Z.
This work inspired some more foundational work on relational refinement:
- Getting to the Bottom of Relational
Refinement: Relations and Correctness, Partial and Total (Boiten and
De Roever) looks at the role of a fictitious "bottom" element in
relational refinement theories.
- Incompleteness of Relational Simulations in the Blocking Paradigm
(submitted) puts the last nail in the coffin for the blocking paradigm:
the model isn't equal to failures (Bolton and Davies), not to single failures
(Reeves and Streader), and its simulations aren't complete (this
paper).
We have now also derived failures-divergences rules for Z-style
specifications
with internal operations, superceding and
improving upon our earlier results on weak refinement.
- Relational Concurrent Refinement with
Internal Operations (Refine 2006) gives an overview of the state
of the art in relating relational and concurrent refinement.
It also gives our first
derivation of failures-divergences simulations with internal operations,
which is improved upon and extended in the next paper.
- Relational Concurrent Refinement II:
Internal Operations and Outputs (FACJ 2008) gives a general scheme
for relational concurrent specifications including both divergence and
deadlock. Simulation rules for failures-divergences refinement with
internal operations are derived from this. Gerhard Schellhorn is the
third author of this paper - his main role has been the formal
specification and verification of this theory using the interactive
theorem prover KIV.
- More relational concurrent refinement: traces and partial relations
(REFINE 2008, to appear in ENTCS) looks at further process algebra
refinement relations, such as completed traces and failure traces.
- Modelling divergence in Relational Concurrent Refinement
(submitted) considers issues around divergence.
Interface Refinement (1998-2004)
Standard refinement in Z does not allow changes in input and output
parameters of operations. "
IO-Refinement in Z"
gives a long list of reasons (including object orientation
and viewpoint specification)
why it would be desirable to allow this. Then it shows how the required
more liberal refinement relation can actually be derived from the semantic
characterisation.
These results have further informed the work on non-atomic refinement and
refinement for Object-Z.
Testing on the basis of abstraction over input and output is described
in Input/Output Abstraction of State Based
Systems - IO refinement is its formal justification.
Refinement and Decomposition(1999-)
"
Separating component and context specification
using promotion" describes how refinement between
specifications can be preserved when these specifications are considered
in larger contexts, created either by
promotion or higher level
structuring provided by a process algebra like CSP.
This approach is taken further in
"
Combining Component specifications in
Object-Z and CSP.
"Non-atomic refinement in Z"
describes a first
investigation into refinement relations for Z that do not require every
abstract operation to be matched by exactly one concrete operation.
"Refinement of objects and operations in Object-Z"
takes this further by investigating the decomposition of objects as
well as operations in an Object-Z context. In order to verify refinements
where a single class is broken down into a number of interacting objects
or components the idea of a simulation is extended to a class simulation.
"Using coupled simulations in non-atomic
refinement" (Derrick and Wehrheim)
looks at a definition of non-atomic
refinement using the notion of coupled simulations. These simulations
record
operations that have started but not yet been completed, and
requirements on
them constrain the notion of non-atomic refinement to rule out
some unwanted
decompositions.
Grey Box Refinement (1998)
"
Grey Box Data Refinement" presents
a generalisation of data
refinement which takes into account that certain components of the state
are
visible. This is done by interpreting these so-called
grey box specifications as ordinary ("black box") specifications
with additional operations, and simplifying the traditional refinement
conditions for those.
Alternative Logics (1998-2002)
Ralph Miarka's work has concentrated on alternative interpretations of Z
that allow explicit underspecification and inconsistencies. These are
described in
Guards, Preconditions, and Refinement in Z
and
Handling inconsistencies in Z using quasi-classical logic.
Related projects
Past research projects in our group are
A new project is
-
which also includes our recent work on approximate refinement and work
with Dan Grundy on "Reduction and Refinement".