Australasian Refinement Workshop 2001 Proceedings
http://www.itee.uq.edu.au/~arw/proceedings.html
Full Proceedings (Gzipped Postscript)
From synchronous communication to asynchronous communication with
transition refinement
Sibylle Peuker
The design of a distributed algorithm usually starts with a simple
non-distributed algorithm that has some desired properties. That algorithm
is then stepwise refined to a fully distributed algorithm such that the
desired properties are preserved in each step. In the refinement process,
we are often faced with the problem that a synchronous action of several
agents has to be distributed into asynchronous actions of the agents,
eg by message passing.
In this talk, we present the notion of transition refinement which is suitable for situations as these. Transition refinement is based on partial order semantics. A partial order semantics describes the causal dependencies between the actions of a system. It depends on the causal relations between a synchronous action and its environment, if a replacement of this action by a more complex (distributed) algorithm preserves the desired properties.
Because of their canonical partial order semantics, Petri nets are well suited for defining transition refinement. We introduce transition refinement by means of a simple communication protocol between two agents. Furthermore, we discuss how to prove that a replacement of a synchronous action is a transition refinement.
Refinement and the Z Schema Calculus
Lindsay Groves
It is well known that the principle operators in the Z schema calculus
are not monotonic with respect to refinement, which means that components
of schema expression cannot be safely replaced by their refinements.
The usual reaction to this observation is to remove all schema connectives
before performing any kind of refinement, or to move to a different formalism
such as the refinement calculus. A closer examinations shows exactly
how non-monotonicity arises, and reveals that under certain conditions
components of schema expressions can be safely replaced by their refinements.
(Slides)
Compilation by Refinement
Geoff Watson and Luke Wildman and Colin Fidge
A small case study extends the earlier work of Fidge and Lermer on
compilation by refinement.
We take as our target language a subset of the .NET assembly language. Selected .NET assembler instructions are given a semantics in terms of Guarded Command Language, and this is used to define refinement laws that convert high-level language commands to sequences of assembler instructions.
The case study is a concrete application of the "compilation by refinement"
strategy described in Fidge and Lermer's earlier papers, and demonstrates
this strategy in action - from a specification in GCL to runnable code.
(Paper)
The DOVE2000 Project
Brendan Mahony
The recently released DOVE99 is a graphical tool for the high-assurance
design and analysis of state machines. The rigour of the tool is provided
by a model of state machines as temporal-predicate transformers, implemented
in Isabelle99. The tool provides graphical tools for:
- constructing Isabelle theories which model specific state machine designs,
- for interfacing with Isabelle's standard goal-directed proof package so as to demonstrate safety properties, and
- for symbolic animation of the state machine design.
From Kleene Algebra to Refinement Algebra
Joakim von Wright
Systems, Properties and Refinement
within a Process Algebra Framework
Alex J Cowie
Refinement of Safety Requirements
Brenton Atchinson and Peter Lindsay and Paul Strooper
This talk will report on results from Brenton Atchison's PhD thesis
on Strategies for Software Safety Assurance. It considers two essentially
different approaches to verifying software against system-level safety
requirements. One approach involves specifying a software design, showing
(by specification animation) that it meets system safety requirements,
and then verifying source code against the specification. The other approach
involves deriving safety-related constraints on software functionality
(expressed in temporal logic) and then showing that source code satisfies
the constraints. A case study is used to illustrate and compare the two
approaches. Both approaches are supported by formal notations & rigorous
proofs.
The Development of a Toolkit to
Support the Probabilistic B Method
Thai Son Hoang and Annabelle McIver and Carroll Morgan and Ken Robinson
Tool Support for Verified Program
Compilation
Luke Wildman
(Paper)
Experience with the Use of the
B Method and B Toolkit in Undergraduate Software Engineering
Ken Robinson and Thai Son Hoang
Refinement-Robust Fairness
Hagen Voelzer
Formal models of concurrent systems often use some notion of fairness
to specify the set of all admissible computations of the system. Most prominent
examples for fairness notions are weak fairness (justice) and strong fairness
(compassion).
We argue that a fairness notion should be refinement-robust, that is a fair computation always refines to a fair computation and an unfair computation always refines to an unfair computation. Refinement-robustness has extensively been studied for several equivalence notions for distributed systems, where, however, fairness assumptions have not been taken into account.
We investigate two simple types of atomicity refinement in this paper. In the first type, called T-refinement, an action $a$ is refined into the sequential composition of two actions $a_1, a_2$. In the second type of refinement, called P-refinement, a condition $c$, such as $x=1$, is refined into the sequential composition of two conditions, start of $c$ and end of $c$.
We show that the traditional notions of weak and strong fairness are not robust under these types of refinement. Furthermore, we propose refinement-robust versions of weak and strong fairness. Moreover, we propose a whole hierarchy of increasingly strong, refinement-robust, fairness notions. Intuitively speaking, the fairness notions in that hierarchy express increasing ability to synchronise independent resources.
We show that the hierarchy separates different aspects of fairness, which are mixed up by the traditional notions of weak and strong fairness. We further motivate the hierarchy by a brief consideration of the computational power of different fairness notions: By assuming a stronger fairness notion we can solve more synchronisation- and coordination problems in a distributed system. While weak and strong fairness have roughly the same computational power, the new fairness hierarchy exhibits clear boundaries of computational power.
Our fairness notions are based on Petri nets and their partial-order semantics. We show, however, that these notions can be easily defined on interleaving sequences. The only crucial prerequisite to the approach is a notion of independence of actions in the model.
Validating Specifications by Combining Animation and Proof
Tracey Yao and Ray Nickson
Victoria University of Wellington, New Zealand
Although formal specifications provide us a potential starting point
for completely rigorous software development, the question as to whether
the formal specification correctly captures the client's requirements can
never be answered completely formally. Instead, we are limited to
a ``testing'' (or validation) approach, where the specification is tested
against certain criteria in the hope that any flaws in it will be exposed.
Two approaches to validating formal specifications are animation (where
the specification is executed using sample input data) and proof (where
the specification is shown to possess certain formal properties).
Neither approach is adequate in itself, and we advocate a combination of the two. A significant advantage of animation is that it allows a very rapid overview of a specification: indeed, animating a specification is much the same as building a prototype. The advantages for communicating with clients are obvious. A major disadvantage is that developers can be tempted to design their specifications specifically for execution by some particular animator, at the cost of clarity. Where a specification is naturally (or accidentally) nondeterministic, the animator might choose to resolve the nondeterminism in a way that is misleading.
On the other hand, with a theorem-proving approach to validation, it is not always easy to decide what to prove; and proofs do not always provide much help with understanding a specification. However, a proof is never misleading: it establishes some property without question.
We explore how a theorem prover may be linked with an animator to try and combine the advantages and trade off the disadvantages of both approaches. A Z animator (Jaza) provides the ``front-end'' for our combined system; it communicates with an interactive theorem prover (Ergo).
Taking Exceptions Seriously
Geoff Watson and Luke Wildman and Colin Fidge
Exception mechanisms are a feature of many high-level programming languages.
They can be viewed as a controlled "goto" construct and in practice are
very useful - separating the concerns of normal and abnormal behaviours.
However the standard refinement calculus must be extended to model them. Although, theoretically, exceptions may be eliminated by program transformation, this may result in much a more complicated program. Again, while compilation typically eliminates exception mechanisms in favour of explicit tests and jumps, the semantics of some assembler instructions may themselves include exceptional behaviour, such as the generation of interrupts.
Thus in a wide-spectrum setting, which includes realistic fragments of a high-level language and an assembly-level language, as well as specification constructs we need to be able to model exceptions.
Christian has shown how this can be done using an extension of the predicate transformer semantics, and King and Morgan have extended this to allow for nondeterminism.
We review the necessity to accommodate exceptions in our refinement repertoire, and give a small example which uses the King and Morgan semantics.
Analysing Z refinement
Steve Reeves
In this talk I shall describe some work which represents the beginning
of a long-term piece of research, the aim of which is to thoroughly investigate
refinement in the setting of languages which have partial relational models---Z
being the architypal example of such languages.
I shall describe formalisations of the four most widespread refinement notions for Z and show what our investigations based on those formalisations have so far revealed.
I shall also discuss what the results so far imply for refinement in Z, and look at alternative refinement notions that are suggested by this work. Finally, I shall outline our probable future work in this area.
Translating Refined Logic Programs to Mercury
Robert Colvin
A refinement calculus provides a method for transforming specifications
to executable code, maintaining the correctness of the code with respect
to its specification. In this paper we investigate the use of Mercury
as the target implementation language for a refinement calculus for logic
programs. We describe a prototype tool for translating programs in
our specification language to Mercury code. More generally, we investigate
the advantages that Mercury has over standard Prolog, with respect to developing
correct programs from specifications.
Refining Object-Oriented Invariants
and Dynamic Constraints.
Jamie Shield and Ian Hayes and David Carrington
Concurrency and Timing Path Analysis
Ian Hayes
The (sequential) real-time refinement calculus introduced the "deadline"
command, which allowed the expression of timing deadlines in a machine-independent
fashion. To produce code for a particular machine paths leading to deadlines
must be analysed to ensure they will always reach the deadline in time.
For concurrent programs deadlines deadlines play the same role, but
the timing path analysis becomes more complex because one needs to consider
paths that cross from one process to another via communication primitives.
In addition for finitely buffered communication, one needs to consider
blocking.
Please send comments and suggestions on this page to arw@itee.uq.edu.au
Last updated: 4 Dec 2001
Home