@COMMENT{{This file has been generated by bib2bib 1.88}}
@COMMENT{{Command line: /usr/bin/bib2bib -ob pubs.bib -oc pubs-cites -c 'not $key : "TRX$"' ../pubs-html.bib}}
@INPROCEEDINGS{ASWEC09,
author = {Brijesh Dongol and Ian J. Hayes},
title = {Enforcing Safety and Progress Properties:
An Approach to Concurrent Program Derivation},
booktitle = {Australian Software Engineering Conference 2009},
editor = {Colin Fidge},
publisher = {IEEE Computer Society},
oisbn = {???},
note = {Accepted},
rfcd = {280302 (Software Engineering)},
seo = {700199 (Computer Software and Services n.e.c.)},
project = {TBTR-FTRT},
year = {2009}
}
@INPROCEEDINGS{IFM09,
author = {Robert Colvin and Ian J. Hayes},
title = {{CSP} with Hierarchical State},
booktitle = {Integrated Formal Methods 2009},
series = {Lecture Notes in Computer Science},
publisher = {Springer Verlag},
oisbn = {???},
note = {Accepted},
rfcd = {280302 (Software Engineering)},
seo = {700199 (Computer Software and Services n.e.c.)},
project = {DCCS},
year = {2009}
}
@INCOLLECTION{DDFvIC,
author = {Ian Hayes},
title = {Dynamically Detecting Faults via Integrity Constraints},
booktitle = {Methods, Models, and Tools for Fault Tolerance},
editor = {Michael Butler and Cliff Jones and Alexander Romanovsky and Elena Troubitsyna},
volume = {5454},
publisher = {Springer Verlag},
oisbn = {1-920682-20-1},
series = {Lecture Notes in Computer Science},
abstract = {Control programs for safety-critical systems are required
to tolerate
faults in the devices they control.
In this paper we examine a systematic approach to devising code to
detect faulty devices at runtime.
The approach is centred around the
use of \emph{integrity constraints},
which are invariants on the state of a
system's variables, including its inputs and outputs.
Under normal operation \integritycon s should always hold,
but they are designed to fail to hold if there is a fault.
By adding variables to capture
the previous state of variables or
the time of significant events,
additional integrity constraints can be devised to check for
faults in state transitions or
faults with the rate of progress of the system.
We discuss techniques for devising integrity constraints as well as
efficiently evaluating the constraints.
When an error is detected via the failure of an integrity constraint,
the integrity constraint(s) that failed can help diagnose the
likely fault.
We illustrate the approach using controller software written in the
action system style,
but it is equally applicable to other state machine approaches such as
Event-B and TLA.},
rfcd = {280302 (Software Engineering)},
seo = {700199 (Computer Software and Services n.e.c.)},
project = {FTRT},
year = {2008}
}
@INPROCEEDINGS{serene08,
author = {Ian J. Hayes},
title = {Towards reasoning about teleo-reactive programs for robust real-time systems},
booktitle = {SERENE '08: Proceedings of the 2008 RISE/EFTS Joint International Workshop on Software Engineering for Resilient Systems},
editors = {Nicolas Guelfi and Henry Muccini and Patrizio Pelliccione and
Alexander Romanovsky},
isbn = {978-1-60558-275-7},
pages = {87--94},
location = {Newcastle upon Tyne, United Kingdom},
doi = {http://doi.acm.org/10.1145/1479772.1479789},
publisher = {ACM},
address = {New York, NY, USA},
rfcd = {280302 (Software Engineering)},
seo = {700199 (Computer Software and Services n.e.c.)},
project = {FTRT},
year = {2008}
}
@INPROCEEDINGS{PCiRA,
author = {Larissa Meinicke and Ian J. Hayes},
title = {Probabilistic Choice in Refinement Algebra},
booktitle = {Mathematics of Program Construction (MPC)},
editor = {Philippe Audebaud and Christine Paulin-Mohring},
pages = {243--267},
series = {Lecture Notes in Computer Science},
volume = {5133},
publisher = {Springer Verlag},
doi = {10.1007/978-3-540-70594-9_14},
rfcd = {280302 (Software Engineering)},
seo = {700199 (Computer Software and Services n.e.c.)},
project = {FTRT},
keywords = {Kleene algebra, probability, refinement algebra, total-correctness},
abstract = {The term refinement algebra refers to a set of abstract algebra,
similar to Kleene algebra with tests, that are suitable for reasoning
about programs in a total-correctness framework.
Abstract algebraic reasoning also works well when probabilistic programs
are concerned, and a refinement algebra that is suitable for such
programs has been defined.
This refinement algebra does not contain a probabilistic choice operator,
and has been used to define commonalities between a variety of
different -- both probabilistic and non-probabilistic -- program models.
Although it is possible to algebraically verify a large and interesting
group of theorems for probabilistic programs without explicit reference
to probabilistic choices, there are circumstances in which reasoning
directly about probabilistic choices may be useful.
In this paper we investigate how probabilistic choice may be
characterised abstract-algebraically in refinement algebra.
That is, we propose a new refinement algebra in which probabilistic
choice, probabilistic guards and assertions may be expressed.
Two operators for modelling probabilistic enabledness and termination
are also introduced.},
year = {2008}
}
@ARTICLE{ARfPASaWL,
author = {Larissa Meinicke and Ian J. Hayes},
title = {Algebraic reasoning for probabilistic action systems and while-loops},
journal = {Acta Informatica},
publisher = {Springer Verlag},
volume = {45},
number = {5},
odoi = {dx.doi.org/10.1007/s00236-008-0073-4},
pages = {321--382},
issn = {0001-5903},
accepted = {Accepted for publication 10 March 2008},
doi = {10.1007/s00236-008-0073-4},
rfcd = {280302 (Software Engineering)},
seo = {700199 (Computer Software and Services n.e.c.)},
project = {FTRT},
abstract = {Back and von Wright have developed algebraic laws for
reasoning about
loops in a total correctness framework using the refinement
calculus. We extend their work to reasoning about probabilistic loops
in the probabilistic refinement calculus. We apply our algebraic
reasoning to derive transformation rules for probabilistic action
systems and probabilistic while-loops. In particular we focus on
developing data refinement rules for these two constructs. Our
extension is interesting since some well known transformation rules
that are applicable to standard programs are not applicable to
probabilistic ones: we identify some of these important differences
and we develop alternative rules where possible.
},
keywords = {Kleene algebra, probability, refinement algebra, total-correctness},
year = {2008}
}
@ARTICLE{CMiCLPR,
author = {R. Colvin and I.J. Hayes and P.A. Strooper},
title = {Calculating modules in contextual logic program refinement},
journal = {Theory and Practice of Logic Programming},
editor = {A. Bossi},
publisher = {Cambridge University Press},
doi = {10.1017/S1471068407003043},
url = {http://journals.cambridge.org/action/displayAbstract?fromPage=online&aid=1459272&fulltextType=RA&fileId=S1471068407003043},
eprint = {http://journals.cambridge.org/article\_S1471068407003043},
volume = {8},
number = {01},
pages = {1--31},
rfcd = {280302 (Software Engineering)},
seo = {700199 (Computer Software and Services n.e.c.)},
project = {RefLP},
abstract = {
The refinement calculus for logic programs is a framework for deriving
logic programs from specifications.
It is based on a wide-spectrum language that
can express both specifications and code, and a refinement relation that
models the notion of correct implementation.
In this paper we extend and generalise earlier work on \emph{contextual
refinement}.
Contextual refinement
simplifies the refinement process by abstractly
capturing the context of a subcomponent of a program,
which typically includes information about the values of the
free variables.
This paper also extends and generalises \emph{module refinement}.
A \emph{module} is a collection of procedures that operate
5B
on a common data type;
module refinement between a specification
module $A$ and an implementation module $C$
allows calls to the procedures of $A$ to be systematically replaced with
calls to the corresponding procedures of $C$.
Based on the conditions for module refinement, we present a method for
\emph{calculating} an implementation module from a specification module.
Both contextual and
module refinement within the refinement calculus have been generalised
from earlier work and the results are presented in a unified framework.},
keywords = {Logic programs, refinement, modules, context},
year = {2008}
}
@TECHREPORT{TSftOGTIwtPLfU07-TR,
author = {Brijesh Dongol and Ian J. Hayes},
title = {Trace Semantics for the {Owicki-Gries} Theory Integrated with the Progress Logic from UNITY},
number = {SSE-2007-02},
institution = {Division of Systems and Software Engineering Research, School of Information Technology and Electrical Engineering, The University of Queensland},
year = {2007}
}
@ARTICLE{ZVDM06,
author = {I. J. Hayes and C. B. Jones and J. E. Nicholls},
journal = {{FACS} {FACTS}},
pages = {56--78},
title = {Understanding the differences between {VDM} and {Z}},
volume = {2006-2},
year = 2006
}
@INPROCEEDINGS{JHJ07,
author = {Cliff B. Jones and Ian J. Hayes and Michael A. Jackson},
booktitle = {Formal Methods and Hybrid Real-Time Systems},
obooktitle = {Formal Methods and Hybrid Real-Time Systems:
Essays in Honour of {D}ines {B}j{\o}rner and {Z}hou {C}haochen on the Occassion of their 70th Birthdays},
date-modified = {2007-10-18 15:45:50 +0100},
editor = {Cliff B. Jones and Zhiming Liu and Jim Woodcock},
pages = {364--390},
publisher = {Springer Verlag},
series = {Lecture Notes in Computer Science},
title = {Deriving Specifications for Systems That are Connected to the Physical World},
volume = {4700},
ibsn = {978-3-540-75220-2},
doi = {10.1007/978-3-540-75221-9},
abstract = {Well understood methods exist for developing programs from formal
specifications.
Not only do such methods offer a precise check that certain sorts of deviations
from their specifications are absent from implementations
but they can also increase the productivity of the development process by
careful use of layers of abstraction and refinement in design.
These methods, however, presuppose a
specification from which to begin the development.
For tasks that are fully described in terms of the symbolic values
within a machine, inventing a specification is not difficult
but there is an
increasing demand for systems in which programs interact with an
external physical world.
Here, the task of fixing the specification for the ``silicon package''
can be more challenging than the development itself.
Such applications include control programs that attempt to bring
about changes in the physical world via actuators and measure things
in that external (to the silicon package) world via sensors.
Furthermore, most systems of this class must tolerate failures in the
physical components outside the computer:
it then becomes even harder
to achieve confidence that the specification is appropriate.
This paper offers a systematic way to {\em derive\/} the specification of
a control program.
Furthermore, our approach leads to recording
assumptions about the physical world.
We also discuss separating the detection and
management of faults from system operation in the absence of faults.
This discussion is linked to the distinction between
``normal'' and ``radical'' design.},
year = 2007
}
@TECHREPORT{ASfBT-TR,
author = {R. Colvin and I.J. Hayes},
title = {A Semantics for Behavior Trees},
institution = {ARC Centre for Complex Systems (ACCS)},
type = {ACCS Technical Report},
number = {ACCS-TR-07-01},
url = {http://www.accs.edu.au/documents/TechnicalReports/ACCS_TR_07_01},
month = {April},
project = {DCCS},
year = {2007}
}
@ARTICLE{PaPitRTPRC,
author = {I.J. Hayes},
title = {Procedures and Parameters in the Real-time Program Refinement Calculus},
journal = {Science of Computer Programming},
issn = {0167-6423},
volume = {64},
number = {3},
month = {February},
pages = {286--311},
doi = {10.1016/j.scico.2006.06.002},
project = {FTRT/CRTR},
rfcd = {280302 (Software Engineering)},
seo = {700199 (Computer Software and Services n.e.c.)},
year = {2007},
abstract = {The real-time refinement calculus is a formal method for the
systematic derivation of real-time programs from real-time
specifications in a style similar to the non-real-time refinement
calculi of Back and Morgan.
In this paper we extend the real-time refinement calculus with
procedures and provide refinement rules for refining real-time
specifications to procedure calls.
A real-time specification can include constraints on,
not only what outputs are produced,
but also when they are produced.
The derived programs can also include time constraints on when certain
points in the program must be reached;
these are expressed in the form of deadline commands.
Such programs are machine independent.
An important consequence of the approach taken is that,
not only are the specifications machine independent,
but the whole refinement process is machine independent.
To implement the machine independent code on a target machine
one has a separate task of showing that the compiled machine code
will reach all its deadlines before they expire.
For real-time programs, externally observable input and output
variables are essential.
These differ from local variables in that their values are observable
over the duration of the execution of the program.
Hence procedures require input and output parameter mechanisms
that are references to the actual parameters so that changes to
external inputs are observable within the procedure and changes to
output parameters are externally observable.
In addition, we allow value and result parameters.
These may be auxiliary parameters,
which are used for reasoning about the correctness of real-time programs
as well as in the expression of timing deadlines,
but do not lead to any code being generated for them by a compiler.
},
keywords = {Real-time programming; Procedures and parameters;
refinement calculus}
}
@INPROCEEDINGS{RAaPL-ICFEM06,
author = {L. Meinicke and I. J. Hayes},
title = {Reasoning Algebraically about Probabilistic Loops},
booktitle = {ICFEM},
editor = {Zhiming Liu and Jifeng He},
series = {LNCS},
volume = {4260},
publisher = {Springer Verlag},
city = {Berlin},
isbn = {3-540-47460-9},
issn = {0302-9743},
pages = {380--399},
conference = {1--3 November 2006, Macau, PRC},
doi = {10.1007/11901433_21},
url = {http://dx.doi.org/10.1007/11901433\_21},
rfcd = {280302 (Software Engineering)},
seo = {700199 (Computer Software and Services n.e.c.)},
project = {FTRT},
year = {2006},
abstract = {
Back and von Wright have developed algebraic laws for reasoning
about loops in the refinement calculus. We extend their work to
reasoning about probabilistic loops in the probabilistic refinement
calculus.
We apply our algebraic reasoning to derive transformation rules
for probabilistic action systems. In particular we focus on developing
data refinement rules for probabilistic action systems. Our extension is
interesting since some well known transformation rules that are applicable
to standard programs are not applicable to probabilistic ones: we
identify some of these important differences and we develop alternative
rules where possible. In particular, our probabilistic action system data
refinement rules are new.}
}
@INPROCEEDINGS{CASR-MPC06,
author = {Larissa Meinicke and Ian J. Hayes},
title = {Continuous Action System Refinement},
booktitle = {Mathematics of Program Construction: Proceedings 8th International Conference (MPC 2006)},
editor = {T. Uustalu},
series = {LNCS},
volume = {4014},
publisher = {Springer Verlag},
city = {Berlin},
isbn = {3-540-35631-2},
issn = {0302-9743},
pages = {316--337},
conference = {3--5 July 2006, Kuressaare, Estonia},
doi = {10.1007/11783596_19},
url = {http://dx.doi.org/10.1007/11783596_19},
rfcd = {280302 (Software Engineering)},
seo = {700199 (Computer Software and Services n.e.c.)},
project = {FTRT},
year = {2006},
abstract = {
Action systems are a framework for reasoning about discrete
reactive systems. Back, Petre and Porres have extended these action sys-
tems to continuous action systems, which can be used to model hybrid
systems. In this paper we define a refinement relation, and develop prac-
tical refinement rules for continuous action systems.
The meaning of continuous action systems is expressed in terms of a
mapping from continuous action systems to action systems. First, we
present a new mapping from continuous action systems to action systems,
such that the definition of trace refinement is correct with respect to it.
Second, we present a stream semantics that is compatible with the trace
semantics, but is preferable to it because it is more general. Although
action system trace refinement rules are applicable to continuous action
systems with a stream semantics, they are not complete. Finally, we
introduce a new data refinement rule that is valid with respect to the
stream semantics and can be used to prove refinements that are not
possible in the trace semantics, and we analyse the completeness of our
new rule in conjunction with the existing trace refinement rules.}
}
@INPROCEEDINGS{UTP06,
author = {Ian J. Hayes},
title = {Termination of real-time programs: definitely, definitely not or maybe},
booktitle = {UTP 2006: First Int.\ Symp.\ on Unifying Theories of Programming},
editor = {S.E. Dunne and W.J. Stoddart},
series = {LNCS},
volume = {4010},
isbn = {3-540-34750-X},
issn = {0302-9743},
publisher = {Springer Verlag},
pages = {141--154},
conference = {6--7 Feb 2006, Darlington, UK},
acceptance = {invited paper},
rfcd = {280302 (Software Engineering)},
seo = {700199 (Computer Software and Services n.e.c.)},
project = {FTRT},
year = {2006},
abstract = {Real-time control programs are often used in contexts where
(conceptually)
they run forever.
Repetitions within such programs (or their specifications) may either
(i) be guaranteed to terminate,
(ii) be guaranteed to never terminate (loop forever),
or
(iii) may possibly terminate.
In dealing with real-time programs and their specifications,
we need to be able to represent these possibilities,
and define suitable refinement orderings.
A refinement ordering based on Dijkstra's weakest precondition only
copes with the first alternative.
Weakest liberal preconditions allow
one to constrain behaviour provided the program terminates,
which copes with the third alternative to some extent.
However, neither of these handles the case when a program does not
terminate.
To handle this case a refinement ordering based on relational
semantics can be used.
In this paper we explore these issues
and
the definition of loops for real-time programs
as well as corresponding refinement laws.}
}
@TECHREPORT{BurnsEt05,
author = {A. Burns and I. J. Hayes and G. Baxter and C. J. Fidge},
title = {Modelling Temporal Behaviour in Complex Socio-Technical Systems},
year = {2005},
institution = {University of York},
oinstitution = {Department of Computer Science, University of York},
number = {YCS~390}
}
@PROCEEDINGS{FM05,
editor = {J. Fitzgerald and I.J. Hayes and A. Tarlecki},
title = {FM 2005: Formal Methods -- Proceedings
13th International Symposium of Formal Methods Europe,
Newcastle, UK, July 2005},
ibsn = {3-540-27882-6},
issn = {0302-9743},
volume = {3582},
series = {Lecture Notes in Computer Science},
publisher = {Springer Verlag},
city = {Berlin},
month = {July},
conference = {Newcastle, UK, 18--22 July 2005},
project = {ACCS},
rfcd = {280302 (Software Engineering)},
seo = {700199 (Computer Software and Services n.e.c.)},
year = {2005}
}
@ARTICLE{ATfETDiRTP,
author = {K. Lermer and C. J. Fidge and I. J. Hayes},
title = {A Theory for Execution Time Derivation in Real-time Programs},
journal = {Theoretical Computer Science},
issn = {0304-3975},
volume = {346},
number = {1},
month = {November},
pages = {3--27},
snote = {Special issue on Quantitative Aspects of Programming Languages},
project = {TPA/CRTR/ACCS},
rfcd = {280302 (Software Engineering)},
seo = {700199 (Computer Software and Services n.e.c.)},
year = {2005},
abstract = {We provide an abstract command language
for real-time programs and
outline how a partial correctness semantics
can be used to
compute
execution times.
The notions of a timed command, refinement of a timed command,
the command traversal condition,
and the worst-case and best-case execution time
of a command are
formally introduced and investigated with the
help of an underlying
weakest liberal precondition semantics.
The central result is a theory for the computation of worst-case
and best-case
execution times from the underlying semantics based
on supremum and infimum calculations.
The framework is applied to the
analysis of a message transmitter
program
and its implementation.},
keywords = {Real-time programming; Control-flow analysis;
Execution-time derivation and prediction;
Predicate transformer semantics; Partial correctness}
}
@INPROCEEDINGS{IoGPATiaSDE,
author = {Erica Glynn and I.J. Hayes and Anthony MacDonald},
title = {Integration of generic program analysis tools into a software development environment},
booktitle = {Computer Science 2005:
Proceedings 28th Australasian Computer Science Conference (ACSC2005)},
volume = {38},
publisher = {Australian Computer Society},
isbn = {1-920682-20-1},
issn = {1445-1336},
series = {Conferences in Research and Practice in Information Technology},
editor = {V. Estivill-Castro},
pages = {249--257},
conference = {31 Jan--3 Feb 2005, Newcastle},
acceptance = {41/122 for full papers},
rfcd = {280302 (Software Engineering)},
seo = {700199 (Computer Software and Services n.e.c.)},
project = {CRTR/ACCS/Erica Honours},
year = {2005},
abstract = {
Support for program understanding in development and maintenance tasks
can be facilitated by program analysis techniques.
Both control-flow and data-flow analysis can support program
comprehension by augmenting the program text with additional
information that may either be displayed with the program or
used to allow more sophisticated navigation of the program,
e.g., from an identifier's use to its definition.
This paper outlines the addition of generic program analysis
support to a generic, language-based, software development environment.
The analysis tools are implemented in two phases:
a language-dependent phase that extracts basic information from
the program, such as its control-flow graph;
and
a language-independent phase that performs a more sophisticated
analysis of the basic information.
This separation allows program analysis tools to be easily generated
for a new language.}
}
@TECHREPORT{BaFICBE05,
author = {Cook, Phil and Welsh, Jim and Hayes, Ian J.},
title = {Building a Flexible Incremental Compiler Back-End},
number = {SSE-2005-02},
institution = {Division of Systems and Software Engineering Research, School of Information Technology and Electrical Engineering, The University of Queensland},
year = {2005}
}
@TECHREPORT{ISEfIS05,
author = {Cook, Phil and Welsh, Jim and Hayes, Ian J.},
title = {Incremental Semantic Evaluation for Interactive Systems: Inertia, Pre-emption, and Relations},
number = {SSE-2005-01},
institution = {Division of Systems and Software Engineering Research, School of Information Technology and Electrical Engineering, The University of Queensland},
year = {2005}
}
@INPROCEEDINGS{AEfBaSOoiR,
author = {Cameron Smith and Kirsten Winter and I.J. Hayes and R.G. Dromey and P. Lindsay and D.A. Carrington},
title = {An environment for building a system out of its requirements},
booktitle = {Proceedings 19th IEEE International Conference on Automated Software Engineering},
publisher = {IEEE},
oisbn = {??},
pages = {398--399},
conference = {??},
rfcd = {280302 (Software Engineering)},
seo = {700199 (Computer Software and Services n.e.c.)},
project = {DCCS},
year = {2004}
}
@INCOLLECTION{DLPfSUSR,
author = {R. Colvin and L. Groves and I.J. Hayes and D. Hemer and R. Nickson and P.A. Strooper},
title = {Developing Logic Programs from Specifications Using Stepwise Refinement},
booktitle = {Program Development in Computational Logic: A Decade of Research Advances in Logic-Based Program Development},
series = {Lecture Notes in Computer Science},
volume = {3049},
editor = {Bruynooghe, Maurice and Lau, Kung-Kiu},
isbn = {3-540-22152-2},
issn = {0302-9743},
publisher = {Springer Verlag},
city = {Berlin},
pages = {66--89},
totalchap = {15},
rfcd = {280302 (Software Engineering)},
seo = {700199 (Computer Software and Services n.e.c.)},
project = {refLP},
year = {2004},
abstract = {In this paper we demonstrate a refinement calculus for logic
programs, which is a framework for developing logic programs from
specifications.
The paper is written in a tutorial-style, using a running example to
illustrate how the refinement calculus is used to develop logic programs.
The paper also presents an overview of some of the advanced features of
the calculus,
including the introduction of higher-order procedures and the refinement
of abstract data types.}
}
@INPROCEEDINGS{TPIRTS,
author = {I.J. Hayes},
title = {Towards Platform-Independent Real-Time Systems},
booktitle = {ASWEC},
editor = {P.A. Strooper},
publisher = {IEEE Computer Society},
city = {Los Alamitos, California},
pages = {192--200},
conference = {13-16 April 2004, Melbourne},
acceptance = {36/79 for full papers},
isbn = {0-7695-2089-8},
issn = {1530-0803},
rfcd = {280302 (Software Engineering)},
seo = {700199 (Computer Software and Services n.e.c.)},
project = {CRTR},
year = {2004},
abstract = {
Real-time software systems are rarely developed once and left to run.
They are subject to changes of requirements as the applications
they support expand, and they commonly outlive the platforms
they were designed to run on.
A successful real-time system will be duplicated and
adapted to a variety of applications---it becomes a product line.
Current methods for real-time software development are commonly based
on low-level programming languages and involve considerable
duplication of effort when a similar system is to be developed or the
hardware platform changes.
To provide more dependable, flexible and maintainable real-time
systems at a lower cost what is needed is a platform-independent
approach to real-time systems development.
The development process is composed of two phases:
a platform-independent phase, that defines the desired system
behaviour and develops a platform-independent design and
implementation,
and
a platform-dependent phase that maps the implementation onto the
target platform.
The last phase should be highly automated.
For critical systems, assessing dependability is crucial.
The partitioning into platform dependent and independent phases has to
support verification of system properties through both phases.}
}
@INPROCEEDINGS{PaP,
author = {I.J. Hayes},
title = {Programs as paths: An approach to timing constraint analysis},
booktitle = {ICFEM},
editor = {Jin Song Dong and Jim Woodcock},
publisher = {Springer Verlag},
city = {Berlin},
series = {LNCS},
volume = {2885},
pages = {1--15},
conference = {5--7 November 2003, Singapore},
acceptance = {34/91 for full papers},
isbn = {3-540-20461-X},
rfcd = {280302 (Software Engineering)},
seo = {700199 (Computer Software and Services n.e.c.)},
project = {CRTR},
year = {2003},
abstract = {A program can be decomposed into a set of possible execution
paths.
These can be described in terms of primitives such as
assignments, assumptions and coercions,
and composition operators such as
sequential composition and nondeterministic choice
as well as finitely or infinitely iterated sequential composition.
Some of these paths cannot possibly be followed
(they are dead or infeasible),
and they may or may not terminate.
Decomposing programs into paths provides a foundation for
analyzing properties of programs.
Our motivation is timing constraint analysis of real-time programs,
but the same techniques can be applied in other areas such as
program testing.
In general the set of execution paths for a program is infinite.
For timing analysis we would like to decompose a program into a finite
set of subpaths that covers all possible execution paths,
in the sense that we only have to analyze the subpaths in
order to determine suitable timing constraints that cover all
execution paths.}
}
@ARTICLE{LAoETC,
author = {K. Lermer and C.J. Fidge and I.J. Hayes},
title = {Linear Approximation of Execution-Time Constraints},
journal = {Formal Aspects of Computing},
volume = {15},
number = {4},
month = {December},
pages = {319--348},
trnumber = {02-31},
xnote = {in Special Issue on Semantic Foundations of Engineering Design Languages},
project = {TPA/CRTR},
year = {2003},
abstract = {This paper defines an algorithm for predicting
worst-case and best-case execution times, and
determining execution-time
constraints of control-flow paths
through real-time programs using their
partial correctness
semantics.
The algorithm
produces
a linear
approximation of path traversal conditions,
worst-case and best-case
execution times and strongest postconditions
for timed paths in abstract real-time programs.
We further derive techniques to determine
the set
of control-flow paths with
decidable worst-case and best-case execution times.
The approach is based on a
weakest liberal precondition
semantics
and relies on supremum and infimum calculations
similar
to standard computations from
linear programming and Presburger
arithmetic. The methodology is generic in that it is
applicable to any executable language that
can be supplied with a predicate
transformer semantics and hence
provides a verification
basis for
high level as well as assembler level execution-time
analysis techniques.},
keywords = {Real-time program analysis; Timing-path analysis;
Timing prediction; Worst-case and best-case execution times;
Automatic constraint determination.}
}
@INPROCEEDINGS{DtSoaCSftoiE,
author = {I.J. Hayes and M.A. Jackson and C.B. Jones},
title = {Determining the Specification of a Control System from that of its Environment},
booktitle = {{FME 2003}: Formal Methods},
editor = {K. Araki and S. Gnesi and D. Mandrioli},
publisher = {Springer Verlag},
city = {Berlin},
series = {LNCS},
volume = {2805},
pages = {154--169},
pdf = {../Papers/fme03.pdf},
conference = {10-12 September 2003, Pisa, Italy},
acceptance = {44/144 for full papers},
isbn = {3-540-40828-2},
rfcd = {280302 (Software Engineering)},
seo = {700199 (Computer Software and Services n.e.c.)},
project = {DCCS},
year = {2003},
abstract = {Well understood methods exist for developing
programs from given specifications. A formal
method identifies proof obligations at each
development step: if all such proof obligations
are discharged, a precisely defined class of
errors can be excluded from the final program.
For a class of ``closed'' systems such methods
offer a gold standard against which less formal
approaches can be measured.
For ``open'' systems --those
which interact with the physical world-- the
task of obtaining the program specification can
be as challenging as the task of deriving the
program. And, when a system of this class must
tolerate certain kinds of unreliability in the
physical world, it is still more challenging to
reach confidence that the specification obtained
is adequate. We argue that widening the notion
of software development to include specifying
the behaviour of the relevant parts of the
physical world gives a way to derive the
specification of a control system and also to
record precisely the assumptions being made
about the world outside the computer.}
}
@INPROCEEDINGS{lp-ho,
author = {R. Colvin and I. J. Hayes and D. Hemer and P.A. Strooper},
title = {Refinement of higher-order logic programs},
booktitle = {{Proceedings of the International Workshop on
Logic-based Program Synthesis and Transformation (LOPSTR 2002)}},
editor = {M. Leuschel},
publisher = {Springer},
city = {Berlin},
series = {Lecture Notes in Computer Science},
volume = {2664},
pages = {126--143},
acceptance = {15/40 for full papers},
project = {RefLP},
year = {2003},
abstract = {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 extend
the refinement calculus for logic programs to include higher-order
programming capabilities in specifications and programs, such as
procedures as terms and lambda abstraction. We use a higher-order type
and term system to describe programs, and provide a semantics for the
higher-order language and refinement. The calculus is illustrated by
refinement examples.}
}
@INPROCEEDINGS{RaDiCRTP,
author = {Sibylle Peuker and Ian Hayes},
title = {Reasoning about Deadlines in Concurrent Real-Time Programs},
booktitle = {Workshop on Formal Methods for Parallel Programming (FMPP 2003) in Proc.\ 17th International Parallel and Distributed Processing Symposium},
editor = {Michel Charpentier and Beverly Sanders},
publisher = {IEEE CS Press},
pages = {1-8},
isbn = {0-7695-1926-1},
conference = {Workshop on Formal Methods for Parallel Programming (FMPP 2003)},
url = {http://www.cs.unh.edu/~charpov/FMPPTA/},
svrctr = {02--37},
rfcd = {280302 (Software Engineering)},
seo = {700199 (Computer Software and Services n.e.c.)},
project = {CRTR},
year = {2003},
abstract = {We propose a method for the timing analysis of concurrent
real-time programs with hard deadlines. We divide the analy\-sis into
a machine-independent and a machine-dependent task. The latter takes
into account the execution times of the program on a particular
machine. Therefore, our goal is to make the machine-dependent phase of
the analysis as simple as possible.
We succeed in the sense that the machine-dependent phase remains the
same as in the analysis of sequential programs. We shift the
complexity introduced by concurrency completely to the
machine-in\-de\-pen\-dent phase.}
}
@INPROCEEDINGS{FSfPP,
author = {K. Lermer and C. J. Fidge and I. J. Hayes},
title = {Formal Semantics for Program Paths},
booktitle = {Computing: The Australian Theory Symposium (CATS) 2003},
editor = {J. Harland},
publisher = {Elsevier},
series = {Electronic Notes in Theoretical Computer Science (ENTCS)},
volume = {78},
pages = {1--24},
isbn = {0444510850},
conference = {4--7 February, 2003, Adelaide, Australia},
month = FEB,
url = {http://www.elsevier.nl/locate/entcs/volume78.html},
svrctr = {SVRC-TR-02-05},
project = {TPA/CRTR},
year = {2003},
abstract = {This paper provides the syntax and semantics for a
systematic approach
to the problem of analysing
control-flow paths in computer programs.
We give an abstract syntax and a partial
correctness semantics
for program control-flow paths
as a generic model for path analysis
and constraint derivation.
This approach is formally based on a predicate transformer
semantics over
a boolean-valued predicate space and an
abstract command language.
The notions of a command,
dead commands, the entry and exit
conditions of a command and the inverse of a command
are formally defined and investigated on the base of the
semantics. A notion of command refinement
is introduced capturing the abstraction
process in program development
from specification to implementation with
partial correctness.
Furthermore, command-reduction theorems and
characterisations for command refinement are
derived using the underlying semantics.
Finally we verify the equivalence
of weakest liberal precondition and strongest
postcondition semantics for program commands in terms
of the ordering relation they define on the command language.
The approach is generic in that it is
applicable to any program language that can be
supplied with a predicate transformer semantics.},
keywords = {Control-flow path analysis; Partial correctness semantics;
Path refinement;
Weakest liberal precondition semantics; Strongest postconditions.}
}
@INCOLLECTION{APSfRTR,
author = {I. J. Hayes},
title = {A Predicative Semantics for Real-Time Refinement},
booktitle = {Programming Methodology},
editor = {A. McIver and C. C. Morgan},
publisher = {Springer Verlag},
city = {New York},
ochapter = {6},
pages = {109--133},
isbn = {0-387-95349-3},
totalchap = {20},
rfcd = {280302 (Software Engineering)},
seo = {700199 (Computer Software and Services n.e.c.)},
svrctr = {01-15},
project = {HertZ},
year = {2003},
abstract = {Real-time systems play an important role in many safety-critical
systems.
Hence it is essential to have a formal basis for the
development of real-time software.
In this chapter we present a predicative semantics
for a real-time language.
The semantics includes a special variable representing the current time,
and uses timed traces to present the values of external input and
outputs over time so that reactive control systems can be handled.
Because a real-time control system may be a nonterminating process,
we allow the specification of nonterminating programs and the
development of nonterminating repetitions. }
}
@TECHREPORT{ICSEiC-TR,
author = {Phil Cook and Jim Welsh and Ian J. Hayes},
title = {Incremental Context-Sensitive Evaluation in Context},
institution = {Software Verification Research Centre, The University of
Queensland},
number = {02-11},
project = {Phil PhD},
year = {2002}
}
@INPROCEEDINGS{lp-ho-EXTABS,
author = {R. Colvin and I. J. Hayes and D. Hemer and P. Strooper},
title = {Extended abstract: Refinement of higher-order logic programs},
booktitle = {{Pre-Proceedings of the International Workshop on
Logic-based Program Synthesis and Transformation (LOPSTR 2002)}},
editor = {M. Leuschel and F. Bueno},
publisher = {School of Computer Science, Technical University of Madrid},
pages = {136--141},
conference = {17-20 September 2002, Technical University of Madrid},
note = {Extended abstract},
project = {RefLP},
year = {2002}
}
@TECHREPORT{BSAG-TR,
author = {Ian J. Hayes},
title = {Block-Structured (Attribute) Grammars},
institution = {Software Verification Research Centre, The University of Queensland},
number = {02-47},
month = DEC,
project = {},
code = {K (Research report)},
rfcd = {280303 (Programming Languages)},
seo = {700199 (Computer Software and Services n.e.c.)},
year = {2002},
abstract = {
Most computing languages are highly structured but
conventional (flat) grammars
do not make that structure explicit.
To address this issue, we examine adding block structure
to grammars.
We allow a production in a grammar to have local productions
associated with it.
The local productions are accessible only via that production.
Local productions for one construct may be nested within
local productions for higher level constructs to form a
tree-structured hierarchy.
If block structuring is used with an attribute grammar one
can also avoid explicit copying of inherited attributes
through intermediate nodes in the parse tree that do not
modify or make use of the attribute.
For example, in the definition of an expression in a
programming language grammar one may have an environment
attribute that is identical for all nodes in the expression
subtree.
The explicit passing down of the environment attribute
through the intermediate nodes
can be avoided by allowing direct reference to the
environment attribute of the top-level expression
nonterminal.
},
keywords = {Block structure; attribute grammars; L-attribute grammars;
upward remote attributes.}
}
@INPROCEEDINGS{ROOIaDC,
author = {Jamie Shield and Ian J. Hayes},
title = {Refining Object-Oriented Invariants and Dynamic Constraints},
rfcd = {280303 (Programming Languages)},
seo = {700199 (Computer Software and Services n.e.c.)},
pages = {52--61},
booktitle = {Asian-Pacific Software Engineering Conference (APSEC)},
isbn = {0-7695-1850-8},
editor = {P.A. Strooper and P. Muenchaisri},
conference = {Ninth APSEC, 4--6 December 2002, Gold Coast, Queensland, Australia},
issn = {1530-1362},
publisher = {IEEE Computer Society},
svrctr = {02-25},
classification = {E},
project = {Jamie PhD},
ocity = {Los Alamitos, California},
convenor = {Australian Computer Society},
url = {http://computer.org},
year = {2002},
abstract = {An invariant is a constraint on a class
which holds for each externally accessible state of its
instances. A dynamic constraint is a dual-state
property dictating before to after state behaviour that
all methods must adhere to. Both invariants and
dynamic constraints are of practical benefit as they
allow explicit declaration of high-level behavioural
constraints on a class and all its sub-classes. In
this paper, formalisations of invariants and dynamic
constraints are provided in the refinement calculus.
Each is separated into coerced (specification) and
extant (implemented or documentation) categories.
Refinement rules are provided for strengthening
invariants and dynamic constraints. Two separate
development paths are identified: (behavioural)
sub-classing and private refinement.
Refining a class may violate its invariant or dynamic
constraint. Sub-classing is a constrained form of
refinement that maintains these properties.
Revised refinement laws are provided.
Private refinement is an alternative to
(behavioural) sub-classing. It also maintains
properties such as invariants and dynamics constraints
and foregoes the constraints of sub-classing. The
disadvantage is that private refinement can only be
used to implement a class.},
keywords = {Object-Oriented, Refinement Calculus, Invariants,
History Properties}
}
@INPROCEEDINGS{TaRCfCRTP,
author = {S. Peuker and I.J. Hayes},
title = {Towards a Refinement Calculus for Concurrent Real-Time Programs},
editor = {C. George and Huaikou Miao},
booktitle = {Formal Methods and Software Engineering (ICFEM)},
conference = {Proceedings 4th Int. Conf. on Formal Engineering Methods
(ICFEM 2002), Shanghai, China, October 2002},
pages = {335--347},
publisher = {Springer-Verlag},
city = {Berlin},
series = {LNCS},
issn = {0302-9743},
isbn = {3-540-00029-1},
volume = {2495},
svrctr = {02-09},
project = {CRTR},
year = {2002},
abstract = {We define a language and a predicative semantics
to model concurrent real-time programs.
We consider different communication pa\-ra\-digms between the
concurrent components of a program: communication via shared variables
and asynchronous message passing (for different models of channels).
The semantics is the basis for a refinement calculus to derive
machine-in\-de\-pen\-dent concurrent real-time programs from
specifications. We give some examples of refinement laws that deal
with concurrency.}
}
@INPROCEEDINGS{TRTRCaFfMIRTP,
author = {I. J. Hayes},
title = {The Real-Time Refinement Calculus: A Foundation for Machine-Independent Real-Time Programming},
booktitle = {Proceedings 23rd International Conference on the Application and Theory of Petri Nets},
editor = {J. Esparza and C. Lakos},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
ocity = {Berlin},
conference = { 24-30 June 2002, Adelaide, Australia},
volume = {2360},
pages = {44--58},
issn = {0302-9743},
isbn = {3-540-43787-8},
note = {Invited keynote paper},
code = {E1 (Invited keynote paper in refereed proceedings)},
www = {http://www.springer.de},
rfcd = {280302 (Software Engineering)},
seo = {700199 (Computer Software and Services n.e.c.)},
project = {CRTR},
year = {2002},
abstract = {
The real-time refinement calculus is an extension of the standard
refinement calculus in which programs are developed from a
pre-condition plus post-condition style of specification.
In addition to adapting standard refinement rules to be valid in the
real-time context,
specific rules are required for the timing constructs such as delays
and deadlines.
Because many real-time programs may be nonterminating,
a further extension is to allow nonterminating repetitions.
A real-time specification constrains not only what values should
be output,
but when they should be output.
Hence for a program to implement such a specification,
it must guarantee to output values by the specified times.
With standard programming languages such guarantees cannot be made
without taking into account the timing characteristics of the
implementation of the program on a particular machine.
To avoid having to consider such details during the refinement process,
we have extended our real-time programming language
with a deadline command.
The deadline command takes no time to execute and always guarantees
to meet the specified time;
if the deadline has already passed the deadline command is infeasible
(miraculous in Dijkstra's terminology).
When such a real-time program is compiled for a particular machine,
one needs to ensure that all execution paths leading to a deadline are
guaranteed to reach it by the specified time.
We consider this checking as part of an extended compilation phase.
The addition of the deadline command restores for the real-time
language the advantage of machine independence enjoyed by
non-real-time programming languages.}
}
@INPROCEEDINGS{RaT,
author = {I. J. Hayes},
title = {Reasoning about Timeouts},
booktitle = {Proc.\ Mathematics of Program Construction},
editor = {Eerke A. Boiten and Bernhard M\"{o}ller},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
ocity = {Berlin},
doi = {http://dx.doi.org/10.1007/3-540-45442-X_7},
volume = {2386},
pages = {94--116},
issn = {0302-9743},
isbn = {3-540-43857-2},
www = {http://www.springer.de},
rfcd = {280302 (Software Engineering)},
seo = {700199 (Computer Software and Services n.e.c.)},
project = {TPA},
year = {2002},
abstract = {
In real-time programming a timeout mechanism allows exceptional behaviour,
such as a lack of response,
to be handled effectively,
while not overly affecting the programming for the normal case.
For example, in a pump controller if the water level has
gone below the minimum level and the pump is on and hence pumping in more
water, then the water level should rise above the minimum level within
a specified time.
If not, there is a fault in the system and it should
be shut down and an alarm raised.
Such a situation can be handled by normal case code that determines
when the level has risen above the minimum,
plus a timeout case handling the situation when the specified time to
reach the minimum has passed.
In this paper we introduce a timeout mechanism,
give it a formal definition in terms of more basic real-time commands,
develop a refinement law for introducing a timeout clause to
implement a specification,
and
give an example of using the law to introduce a timeout.
The framework used is a machine-independent real-time programming
language, which makes use of a deadline command to represent timing
constraints in a machine-independent fashion.
This allows a more abstract approach to handling timeouts.}
}
@ARTICLE{aRCfLP,
author = {I. J. Hayes and R. Colvin and D. Hemer and P. A. Strooper and R. Nickson},
title = {A Refinement Calculus for Logic Programs},
journal = {Theory and Practice of Logic Programming},
volume = {2},
number = {4--5},
month = JUL,
dates = {July--September},
pages = {425--460},
issn = {?},
project = {RefLP},
year = {2002},
abstract = {
Existing refinement calculi provide frameworks for the stepwise
development of imperative programs from specifications.
This paper presents a refinement calculus for deriving logic programs.
The calculus contains a wide-spectrum logic programming language,
including executable constructs such as sequential conjunction,
disjunction, and
existential quantification, as well as specification constructs
such as general predicates, assumptions and universal quantification.
A declarative semantics is defined for this wide-spectrum language
based on {\em executions}.
Executions are partial functions from states to states,
where a state is represented as a set of bindings.
The semantics is used to define the meaning of programs and
specifications, including parameters and recursion.
To complete the calculus, a notion of correctness-preserving refinement
over programs in the wide-spectrum language is defined
and refinement laws for developing programs are introduced.
The refinement calculus is illustrated using example derivations and
prototype tool support is discussed.}
}
@INPROCEEDINGS{TRLPtM,
author = {R. Colvin and I. J. Hayes and D. Hemer and P. A. Strooper},
title = {Translating Refined Logic Programs to {Mercury}},
booktitle = {Proceedings 25th Australasian Computer Science Conference (ACSC 2002)},
editor = {M. Oudshoorn},
publisher = {Australian Computer Society},
series = {Conferences in Research and Practice in Information Technology},
volume = {4},
pages = {33--40},
isbn = {0-909925-82-8},
conference = {Melbourne, Australia},
project = {RefLP},
year = {2002}
}
@INPROCEEDINGS{DCOfLPR,
author = {D. Hemer and R. Colvin and I. Hayes and P. Strooper},
title = {Don't Care Non-Determinism in Logic Program Refinement},
booktitle = {Proceedings of Computing: the Australasian Theory Symposium (CATS 2002)},
editor = {J. Harland},
publisher = {Elsevier Science},
series = {Electronic Notes in Theoretical Computer Science (ENTCS)},
volume = {61},
pages = {1--21},
isbn = {0444510850},
conference = {Melbourne, Australia},
project = {RefLP},
year = {2002},
abstract = {
The refinement calculus for logic programs consists of a wide-spectrum
language, a semantics for the language and a notion of refinement that
can be used to develop programs from specifications.
The wide-spectrum language includes many of the concepts found in logic
programs, including sequential composition, existential quantification,
disjunction, procedures and recursion. A number of non-implementable
constructs, such as universal quantification, parallel conjunction,
assumptions and specifications, are also included.
The semantics are defined in terms of {\em executions}, describing the
effect of the program constructs on the state of the program.
A notion of refinement is defined, where one program refines another if
it terminates more often and returns the same set of answers.
Non-determinism is supported in the language by allowing more than
one answer, but in a refinement the refined program must return the
same set of answers as the original program.
In the traditional refinement calculus for imperative programs, there is
another form of non-determinism, called {\em demonic choice}, which allows
non-determinism to be eliminated during refinement.
Thus, non-deterministic specifications, which give the implementer as
much freedom as possible, can be refined to deterministic implementations.
In this paper, we introduce a notion of demonic non-determinism into the
refinement calculus for logic programs.
We extend the wide-spectrum language to include demonic, non-deterministic
choice.
We describe the changes to the underlying semantics and the notion of
refinement that are required, and give an example that illustrates the
use of demonic choice.}
}
@ARTICLE{RaRTRTaN,
title = {Reasoning about Real-Time Repetitions: Terminating and Nonterminating},
author = {I. J. Hayes},
journal = {Science of Computer Programming},
publisher = {Elsevier},
ocity = {Amsterdam},
volume = {43},
number = {2--3},
pages = {161--192},
pdf = {../Papers/iloop.pdf},
issn = {0167-6423},
keywords = {Real-time refinement; nonterminating repetitions.},
url = {http://www.elsevier.com/locate/scico},
rfcd = {280302 (Software Engineering)},
seo = {700199 (Computer Software and Services n.e.c.)},
project = {HertZ},
year = {2002},
abstract = {
It is common for a real-time system to contain a
nonterminating process monitoring an input and controlling
an output. Hence a real-time program development
method needs to support nonterminating repetitions.
In this paper we develop a general proof rule for
reasoning about possibly nonterminating repetitions.
The rule makes use of a Floyd-Hoare-style loop invariant
that is maintained by each iteration of the repetition,
a Jones-style relation between the pre- and post-states on
each iteration, and a deadline specifying an upper bound
on the starting time of each iteration. The general rule
is proved correct with respect to a predicative semantics.
In the case of a terminating repetition the rule reduces
to the standard rule extended to handle real time.
Other special cases include repetitions whose bodies
are guaranteed to terminate, nonterminating repetitions
with the constant true as a guard, and repetitions
whose termination is guaranteed by the inclusion of a
fixed deadline.}
}
@ARTICLE{AItRTOZ,
author = {G. Smith and I. J. Hayes},
title = {An Introduction to {Real-Time Object-Z}},
journal = {Formal Aspects of Computing},
issn = {0934-5043},
volume = {13},
number = {2},
month = {May},
pages = {128--141},
special = {Selected papers from IFM '99},
publisher = {BCS/Springer-Verlag},
city = {London},
project = {HertZ},
year = {2002},
abstract = {
This paper presents Real-Time Object-Z: an integration of the
object-oriented, state-based specification language Object-Z with the
timed trace notation of the timed refinement calculus. This
integration provides a method of formally specifying and refining
systems involving continuous variables and real-time constraints. The
basis of the integration is a mapping of the existing Object-Z
history semantics to timed traces.},
keywords = {Real-time specification; real-time refinement; Object-Z; timed
refinement calculus}
}
@ARTICLE{SCoDCFP,
author = {I. J. Hayes and C. J. Fidge and K. Lermer},
title = {Semantic Characterisation of Dead Control-Flow Paths},
journal = {IEE Proceedings---Software},
volume = {148},
number = {6},
month = {December},
pages = {175--186},
pdf = {../Papers/dead.pdf},
anote = {Awarded the 2001/2002 \emph{Mather Premium} by the Institution of Electrical Engineers},
project = {TPA},
year = {2001},
abstract = {
Many program verification, testing and performance prediction
techniques rely on analysis of statically-identified control-flow
paths. However, some such paths may be `dead' because they can
never be followed at run time, and should therefore be excluded
from analysis.
It is shown how the formal semantics of those statements comprising
a path provides a sound theoretical foundation for identification
of dead paths.}
}
@INPROCEEDINGS{RCfLPiIH,
author = {D. Hemer and I. Hayes and P. Strooper},
title = {Refinement Calculus for Logic Programming in {Isabelle/HOL}},
booktitle = {Theorem Proving in Higher Order Logics, 14th International Conference, {TPHOLs} 2001},
editor = {R. Boulton and P. Jackson},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {2152},
pages = {249--264},
isbn = {3-540-42525-X},
conference = {Edinburgh, Scotland},
project = {RefLP},
year = {2001},
abstract = {This paper describes a deep embedding of a
refinement calculus for logic programs in Isabelle/HOL. It
extends a previous tool with support for procedures and
recursion. The tool supports refinement in context, and a
number of window-inference tactics that ease the burden on
the user. In this paper, we also discuss the insights
gained into the suitability of different logics for
embedding refinement calculii (applicable to both
declarative and imperative paradigms). In particular, we
discuss the richness of the language, choice between typed
and untyped logics, automated proof support, support for
user-defined tactics, and representation of program
states.},
keywords = {Refinement, logic programming, theorem provers}
}
@INPROCEEDINGS{MLPR,
author = {R. Colvin and I. J. Hayes and P. Strooper},
title = {A Technique for Modular Logic Program Refinement},
booktitle = {Logic-based Program Synthesis and Transformation (LOPSTR 2000) Selected Papers},
editor = {Kung-Kiu Lau},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {2402},
pages = {38--56},
doi = {http://dx.doi.org/10.1007/3-540-45142-0_3},
conference = {10th International Workshop, LOPSTR 2000},
isbn = {3-540-42127-0},
issn = {0302-9743},
project = {RefLP},
year = {2001},
abstract = {A refinement calculus provides a method for transforming
specifications to executable code, maintaining the correctness of
the code with respect to its specification. Modules allow one to
group together data types with sets of procedures that manipulate
the data types. In this paper we develop a technique for refining
a module to one that uses a more efficient representation of the
data type. The technique places restrictions on the way procedures
in the module use the data type, and on the way a program uses the
module. The restrictions allow a more efficient implementation to
be developed.}
}
@ARTICLE{aSRTRC,
author = {I. J. Hayes and M. Utting},
title = {A Sequential Real-Time Refinement Calculus},
journal = {Acta Informatica},
publisher = {Springer},
volume = {37},
number = {6},
pages = {385--448},
pdf = {../Papers/srtr.pdf},
project = {HertZ},
year = {2001},
abstract = {
We present a comprehensive refinement calculus for the
development of sequential, real-time programs from real-time
specifications.
A specification may include not only execution time limits,
but also requirements on the behaviour of outputs over the
duration of the execution of the program.
The approach allows refinement steps that separate timing
constraints and functional requirements.
New rules are provided for handling timing constraints, but
the refinement of components implementing functional
requirements is essentially the same as in the standard
refinement calculus.
The product of the refinement process is a program in the
target programming language extended with timing deadline
directives. The extended language is a machine-independent,
real-time programming language.
To provide valid machine code for a particular model of machine,
the machine code produced by a compiler must be analysed to
guarantee that it meets the specified timing deadlines.},
keywords = {Refinement calculus; machine-independent;
real-time specification; real-time refinement;
real-time programming; deadline command; timing constraint analysis;
time-invariant properties.}
}
@INPROCEEDINGS{UTItMtRiaTP,
author = {J. Shield and I. J. Hayes and D. A. Carrington},
title = {Using Theory Interpretation to Mechanise the Reals in a Theorem Prover},
booktitle = {Computing: The Australian Theory Symposium (CATS)},
editor = {C. J. Fidge},
series = {Electronic Notes in Theoretical Computer Science},
volume = {42},
publisher = {Elsevier Science},
isbn = {none!},
pages = {266--281},
note = {URL: www.elsevier.nl/locate/entcs},
conference = {29 Jan - 2 Feb 2001, Bond University, Gold Coast, Queensland, Australia},
organisation = {Australian Computer Science Association},
city = {Amsterdam},
year = {2001}
}
@TECHREPORT{ADSfLPR-TR,
author = {I. J. Hayes and R. Nickson and P. Strooper and R. Colvin},
title = {A Declarative Semantics for Logic Program Refinement},
number = {00-30},
institution = {Software Verification Research Centre,
The University of Queensland, Brisbane 4072, Australia},
month = NOV,
keywords = {Logic programming, refinement.},
project = {RefLP},
year = {2000},
abstract = {The refinement calculus provides a framework for
the stepwise development of
imperative programs from specifications.
This paper presents a semantics for a refinement calculus for deriving
logic programs.
The calculus contains a wide-spectrum logic programming language,
including
executable constructs such as sequential conjunction, disjunction, and
existential quantification, as well as specifications constructs
(general predicates and assumptions) and universal quantification.
A semantics is defined for this wide-spectrum language based on
{\em executions}, which are partial functions from states to states,
where a state is represented as a set of bindings.
This execution semantics is used to define the meaning of programs and
specifications, including parameters and recursion.
To complete the calculus, a notion of correctness-preserving refinement
over programs in the wide-spectrum language is defined and a refinement
law for introducing recursive procedures is presented.}
}
@INPROCEEDINGS{RaRTPUIIA,
author = {I. J. Hayes},
title = {Reasoning about Real-Time Programs Using Idle-Invariant Assertions},
pages = {16--23},
booktitle = {Proceedings 7th Asia-Pacific Software Engineering Conference (APSEC 2000)},
conference = {5--8 December 2000, Singapore},
isbn = {0-7695-0915-0},
editor = {J. S. Dong and J. He and M. Purvis},
publisher = {IEEE Computer Society},
city = {Washington},
techreport = {Also SVRC-TR-00-38},
project = {HertZ},
year = {2000},
abstract = {We develop a set of laws for reasoning about
real-time programs using assertions (preconditions and
postconditions) in the style of Hoare.
In the real-time context assertions may refer to the current
time and to the value of external inputs,
which are not under the direct control of the program
and hence not guaranteed to be stable with respect to the
passage of time
(even if the program does not modify any of the
variables under its control).
Hence in order to reason about real-time programs,
we make use of idle-invariant assertions:
assertions that are invariant to just the passage of time.}
}
@INPROCEEDINGS{SRTOZS,
author = {G. Smith and I. J. Hayes},
title = {Structuring Real-Time {Object-Z} Specifications},
booktitle = {IFM'00: Proceedings of the 2nd International Conference on Integrated Formal Methods},
editor = {W. Grieskamp and T. Santen and B. Stoddart},
isbn = {3-540-41196-8},
pages = {97-115},
series = {Lecture Notes in Computer Science},
volume = {1945},
publisher = {Springer},
city = {Berlin},
conference = {Schloss Dagstuhl, 1-3, November 2000},
project = {HertZ},
year = {2000}
}
@INPROCEEDINGS{RTPRuAV,
author = {I. J. Hayes},
title = {Real-Time Program Refinement Using Auxiliary Variables},
pages = {170--184},
booktitle = {Proc.\ Formal Techniques in Real-Time and Fault-Tolerant Systems},
series = {LNCS},
publisher = {Springer},
volume = {1926},
isbn = {3-540-41055-4},
editor = {M. Joseph},
project = {TPA},
year = {2000},
abstract = {Real-time program development can be split into a
machine-independent phase,
that derives a machine-independent real-time
program from a specification,
and a machine-dependent phase,
that checks that the compiled program will meet its
deadlines when executed on the target machine.
In this paper we extend a machine-independent real-time
programming language with auxiliary variables.
These are introduced to facilitate both reasoning about the
correctness of real-time programs
and the expression of timing deadlines,
and hence
the calculation of timing constraints on paths through a program.
The auxiliary variable concept is extended to auxiliary
parameters to procedures.}
}
@INPROCEEDINGS{MLPR-EA,
author = {R. Colvin and I. J. Hayes and P. Strooper},
title = {Modular Logic Program Refinement},
booktitle = {Pre-Proceedings of the Tenth International Workshop on
Logic-based Program Synthesis and Transformation (LOPSTR 2000)},
editor = {Kung-Kiu Lau},
publisher = {Department of Computer Science, Manchester University},
series = {Technical Report},
number = {UMCS-00-6-1},
pages = {1--10},
isbn = {??},
conference = {24--28 July 2000, Imperial College, London, UK},
note = {Extended abstract},
year = {2000},
abstract = {A refinement calculus provides a method for transforming
specifications to executable code, maintaining the correctness of
the code with respect to its specification. Modules allow one to
group together data types with sets of procedures that manipulate
the data types. In this paper we develop a technique for refining
a module to one that uses a more efficient representation of the
data type. The technique places restrictions on the way procedures
in the module use the data type, and on the way a program uses the
module. The restrictions allow a more efficient implementation to
be developed.}
}
@INPROCEEDINGS{RaNtLUDC,
author = {I. J. Hayes},
title = {Reasoning about Non-terminating Loops Using Deadline Commands},
pages = {60--79},
booktitle = {Proc.\ Mathematics of Program Construction},
isbn = {3-540-67727-5},
issn = {0302-9743},
editor = {R. Backhouse and J. N. Oliveira},
series = {Lecture Notes in Computer Science},
volume = {1837},
note = {This paper is superceded by \cite{RaRTRTaN}},
publisher = {Springer},
project = {HertZ},
year = {2000},
abstract = {
It is common for a real-time process to consist of a
nonterminating loop monitoring an input
and controlling an output.
Hence a real-time program development method needs to
support nonterminating loops.
Earlier work on real-time program development has produced a
real-time refinement calculus that makes use of a novel
deadline command which allows timing constraints to be
embedded in real-time programs.
The addition of the deadline command to the real-time
programming language gives the significant advantage of
providing a real-time programming language that is machine
independent.
This allows a more abstract approach to the program
development process.
In this paper we add possibly nonterminating loops to the
refinement calculus.
First we examine the semantics of possibly nonterminating loops,
and use them to reason directly about a simple example.
Then we develop simpler refinement rules that make use of a
loop invariant.}
}
@INPROCEEDINGS{RLPuT,
author = {R. Colvin and I. J. Hayes and P. Strooper},
title = {Refining Logic Programs Using Types},
booktitle = {Australasian Computer Science Conference (ACSC~2000)},
editor = {Jenny Edwards},
publisher = {IEEE Computer Society},
pages = {43--50},
isbn = {0-7695-0518-X},
conference = {31 Jan -- 3 Feb 2000, ANU, Canberra, Australia},
year = {2000},
abstract = {The logic programming refinement calculus is a method for
transforming specifications to executable code, maintaining the
correctness of the code with respect to its specification. In this paper
we show how types can be handled in the logic programming refinement
calculus. Types of variables are necessary for a complete specification
of a procedure, and typing information can guide the refinement of a
procedure specification to code. As an application of this framework,
we show how dynamic type-checks can be formally eliminated from a
sample program.}
}
@INPROCEEDINGS{RTSaRUMI,
author = {C. J. Fidge and I. J. Hayes and B. P. Mahony and A. K. Wabenhorst},
title = {Real-Time Specification and Reasoning Using Maximal Intervals},
editor = {W. C. H. Cheng and A. S. M. Sajeev},
booktitle = {PART'99: Proceedings of the 6th Australasian Conference on Parallel and Real-Time Systems},
pages = {344--354},
isbn = {981-4021-59-8},
publisher = {Springer},
year = {1999}
}
@INPROCEEDINGS{TRTOZ,
author = {G. Smith and I. J. Hayes},
title = {Towards Real-Time {Object-Z}},
booktitle = {IFM'99: Proceedings of the 1st International Conference on Integrated Formal Methods},
editor = {Keijiro Araki and Andy Galloway and Kenji Taguchi},
isbn = {1-85233-107-0},
pages = {49--65},
publisher = {Springer},
city = {London},
conference = {York, 28--29 June 1999},
year = {1999}
}
@INCOLLECTION{SaNNE99,
author = {I. J. Hayes and C. B. Jones},
title = {Specifications are not (necessarily) executable},
booktitle = {High-Integrity System Specification and Design},
editor = {J. P. Bowen and M. G. Hinchey},
isbn = {3-540-76226-4},
note = {(Previously published in {\em IEE/BCS Software Engineering Journal},
Vol.\ 4, No.\ 6, 330--338, November, 1989)},
pages = {563--581},
publisher = {Springer},
city = {London},
year = {1999}
}
@ARTICLE{TDC,
author = {C. J. Fidge and I. J. Hayes and G. Watson},
title = {The Deadline Command},
journal = {IEE Proceedings---Software},
volume = {146},
number = {2},
month = APR,
pages = {104--111},
ps = {../Papers/deadline.ps},
project = {TPA},
year = {1999}
}
@INPROCEEDINGS{DDaIiZ,
author = {C. J. Fidge and I. J. Hayes and B. P. Mahony},
title = {Defining Differentiation and Integration in {Z}},
booktitle = {Proceedings Second International Conference on Formal Engineering Methods ({ICFEM'98})},
editor = {J. Staples and M. G. Hinchey and {Shaoying Liu}},
isbn = {0-8186-9198-0},
pages = {64--73},
publisher = {IEEE Computer Society},
svrctr = {UQ-SVRC-98-09},
where = {Brisbane, Australia},
year = {1998}
}
@INPROCEEDINGS{STaCiRTR,
author = {I. J. Hayes},
title = {Separating timing and calculation in real-time refinement},
booktitle = {Int.\ Refinement Workshop and Formal Methods Pacific 1998},
editor = {J. Grundy and M. Schwenke and T. Vickers},
publisher = {Springer},
isbn = {981-4021-16-4},
pages = {1--16},
pdf = {../Papers/rtsep.pdf},
city = {Singapore},
svrctr = {UQ-SVRC-98-14},
year = {1998},
abstract = {
We consider the specification and refinement of sequential
real-time programs.
Our real-time specifications describe the allowable behaviours
of an implementation in terms of the values of variables over time.
Hence within a specification the values of the variables and
the times at which they have those values are intertwined.
However, in a real-time program some commands are concerned
with calculating the right outputs, while other commands,
such as delays and deadlines, are concerned with making sure
the outputs appear at the right time.
During the refinement process we would like to decompose the
overall problem into those aspects dealing with time and
those that are purely calculation.
We need refinement rules that allow us to separate these
concerns.
Further, given a component that is only concerned with
calculation, the complexities of the real-time calculus that
deal with timing behaviour are an unnecessary burden.
Such calculational components can be developed more
straightforwardly in the standard refinement calculus.
We would like to allow the use of the untimed calculus for
the development of such components.
To do that we need to embed the untimed calculus within the
real-time calculus.}
}
@INPROCEEDINGS{SCitSRTRC,
author = {L. P. Wildman and I. J. Hayes},
title = {Supporting Contexts in the Sequential Real-Time Refinement Calculus},
booktitle = {International Refinement Workshop and Formal Methods Pacific 1998},
editor = {J. Grundy and M. Schwenke and T. Vickers},
publisher = {Springer},
isbn = {981-4021-16-4},
pages = {352--369},
svrctr = {UQ-SVRC-98-29},
city = {Singapore},
year = {1998}
}
@INPROCEEDINGS{DRLP,
author = {R. Colvin and I. J. Hayes and P. Strooper},
title = {Data refining logic programs},
booktitle = {International Refinement Workshop and Formal Methods Pacific 1998},
editor = {J. Grundy and M. Schwenke and T. Vickers},
series = {Discrete Mathematics and Theoretical Computer Science},
publisher = {Springer},
isbn = {981-4021-16-4},
pages = {100--116},
city = {Singapore},
svrctr = {UQ-SVRC-98-15},
project = {RefLP},
year = {1998},
abstract = {
A refinement calculus provides a method for transforming
specifications to executable code, maintaining the correctness of the
code with respect to its specification. One aspect of refinement is
transforming the representation of data in a specification. This could
be performed for efficiency reasons, or to change an abstract specification
type into a data type that is in the target implementation language.
This paper looks at data refinement in the refinement calculus for logic
programs. Three cases for data refinement in the logic calculus are
examined, and the process for each is described. The three cases
are illustrated by a running example.}
}
@ARTICLE{aPRT,
author = {D. Carrington and I. Hayes and R. Nickson and
G. Watson and J. Welsh},
title = {A Program Refinement Tool},
journal = {Formal Aspects of Computing},
volume = {10},
number = {2},
pages = {97--124},
ps = {../Papers/prtj.ps},
publisher = {BCS/Springer},
year = {1998}
}
@ARTICLE{EPoSL,
author = {I. J. Hayes},
title = {Expressive power of specification languages},
journal = {Formal Aspects of Computing},
volume = {10},
number = {2},
pages = {187--192},
publisher = {BCS/Springer},
year = {1998}
}
@INPROCEEDINGS{mpc98,
author = {C. J. Fidge and I. J. Hayes and A. P. Martin and A. K. Wabenhorst},
title = {A Set-Theoretic Model for Real-Time Specification and Reasoning},
editor = {J. Jeuring},
booktitle = {Mathematics of Program Construction (MPC'98)},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = 1422,
pages = {188--206},
comment = {Also available as SVRC TR 98-07},
year = 1998
}
@INPROCEEDINGS{DaT,
author = {I. J. Hayes and M. Utting},
title = {Deadlines are Termination},
booktitle = {IFIP TC2/WG2.2, 2.3 International Conference on
Programming Concepts and Methods (PROCOMET'98)},
conference = {8--12 June 1998, Shelter Island, New York, USA},
editor = {D. Gries and W.-P. de Roever},
isbn = {0-412-83760-9},
pages = {186--204},
pdf = {../Papers/procomet.pdf},
publisher = {Chapman and Hall},
city = {London},
year = {1998}
}
@INPROCEEDINGS{TCA98,
author = {S. Grundon and I. J. Hayes and C. J. Fidge},
title = {Timing Constraint Analysis},
booktitle = {Computer Science '98: Proc.\ 21st Australasian Computer Sci.\ Conf.\ ({ACSC'98})},
location = {{\rm Perth, 4--6 Feb.}},
editor = {C. McDonald},
publisher = {Springer},
pages = {575--586},
year = {1998}
}
@INPROCEEDINGS{RefLP-Tool-NFMW,
author = {R. Colvin and I. J. Hayes and R. Nickson and P. A. Strooper},
title = {A Tool for Logic Program Refinement},
booktitle = {Second {BCS-FACS} Northern Formal Methods Workshop (NFMW'97)},
other = {Ilkley, UK, July, 1997},
editor = {D. J. Duke and A. S. Evans},
isbn = {3-540-76215-9},
series = {Electronic Workshops in Computing},
publisher = {Springer},
city = {London},
year = {1997}
}
@INPROCEEDINGS{BancroftHayesTypeExtensionandRefinement,
author = {P. G. Bancroft and I. J. Hayes},
title = {Type extension and refinement},
pages = {23--39},
editor = {L. Groves and S. Reeves},
booktitle = {Formal Methods Pacific (FMP'97)},
publisher = {Springer},
isbn = {981-3083-31-X},
city = {Singapore},
year = {1997},
abstract = {This paper extends the methods of the refinement
calculus to allow the derivation of certain kinds of Oberon-like
programs. The use of records, pointers, opaque types and type
extension distinguishes the work from previous examples.
A case study for a queue abstract data type illustrates a method
for the derivation of a generic, linked implementation.
Firstly, a sequence of integers is refined to a sequence of
integer records with link pointers. The the sequence of records
is refined to a generic linked list that is close to Oberon code.
Pointers are facilitated by declaring an explicit local data
store for each queue variable. The advantage of Oberon over
Modula-2 is the ability to separate the final code into two
modules - a generic queue that maintains the linked data
structure invariant and an integer instantiation of the queue,
using type extension. This separation of concerns (isolation of
the linked data structure properties) is the main benefit of the
approach.}
}
@ARTICLE{SCiPR,
author = {R. Nickson and I. Hayes},
title = {Supporting Contexts in Program Refinement},
key = {program window inference},
journal = {Science of Computer Programming},
issn = {0167-6423},
uqcall = {QA75.5 .S35},
volume = {29},
number = {3},
pages = {279--302},
year = {1997},
abstract = {
A program can be refined either by transforming the whole program
or by refining one of its components.
The refinement of a component is, for the main part,
independent of the remainder of the program.
However, refinement of a component can depend on the
{\em context\/} of the component for information about the
variables that are in scope and what their types are.
The refinement can also take advantage of additional information,
such as any precondition the component can assume.
The aim of this paper is to introduce a technique, which we call
{\em program window inference\/}, to handle such contextual
information during derivations in the refinement calculus.
The idea is borrowed from a technique, called {\em window
inference\/}, for handling context in theorem proving.
Window inference is the primary proof paradigm of the {\em Ergo\/}
proof editor. This tool has been extended to mechanize refinement
using program window inference.}
}
@INPROCEEDINGS{CoercingRTR,
author = {I. J. Hayes and M. Utting},
title = {Coercing real-time refinement: A transmitter},
booktitle = {{BCS-FACS} Northern Formal Methods Workshop (NFMW'96)},
other = {Ilkley, UK, September, 1996},
editor = {D. J. Duke and A. S. Evans},
isbn = {3-540-76117-9},
pdf = {../Papers/trco.pdf},
series = {Electronic Workshops in Computing},
publisher = {Springer},
city = {London},
year = {1997}
}
@INPROCEEDINGS{LOPSTR-LP,
author = {I. Hayes and R. Nickson and P. Strooper},
title = {Refining specifications to logic programs},
editor = {J. Gallagher},
booktitle = {Logic Program Synthesis and Transformation. Proc.\ of the 6th Int.\ Workshop, LOPSTR'96, Stockholm, Sweden, August 1996},
volume = {1207},
pages = {1--19},
series = {Lecture Notes in Computer Science},
isbn = {3-540-62718-9},
uqcall = {QA76 .L4 v.1207},
publisher = {Springer},
year = {1997}
}
@PROCEEDINGS{ARW96,
title = {Proc.\ 5th Australasian Refinement Workshop},
editor = {I. J. Hayes},
organization = {Software Verification Research Centre, The University of Queensland},
note = {Unrefereed.},
url = {http://www.itee.uq.edu.au/~arw},
month = {April},
year = {1996}
}
@INPROCEEDINGS{ARW96-LP,
author = {I. J. Hayes and P. A. Strooper},
title = {Refining specifications to logic programs},
booktitle = {Proc.\ 5th Australasian Refinement Workshop},
editor = {I.J. Hayes},
pages = {1--13},
publisher = {Software Verification Research Centre, The University of Queensland},
note = {Unrefereed.},
url = {http://www.itee.uq.edu.au/MENU/WORKSHOPS-SEMINARS-CONFERENCES/WORKSHOPS/5thaus.html},
month = {April},
year = {1996}
}
@ARTICLE{Hayes:reuse-mod,
author = {I. J. Hayes},
key = {refinement calculus; reuse; module},
title = {Supporting module reuse in refinement},
journal = {Science of Computer Programming},
issn = {0167 6423},
uqcall = {QA75.5 .S35},
volume = {27},
number = {2},
pages = {175--184},
year = {1996}
}
@INPROCEEDINGS{PRT:TOOL-PAPER,
author = {D. A. Carrington and I. J. Hayes and R. Nickson and
G. Watson and J. Welsh},
title = {A Tool for Developing Correct Programs by Refinement},
booktitle = {Proc.\ BCS 7th Refinement Workshop, Bath, UK},
editor = {{He Jifeng}},
series = {Electronic Workshops in Computing},
publisher = {Springer},
pages = {1--17},
year = {1996}
}
@INPROCEEDINGS{FidgeUttingKearneyHayes96,
author = {C. J. Fidge and M. Utting and P. Kearney and I. J. Hayes},
title = {Integrating real-time scheduling theory and program refinement},
editor = {M.-C. Gaudel and J. Woodcock},
booktitle = {FME'96: Industrial Benefit and Advances in Formal Methods},
proctitle = {Proc.\ Formal Methods Europe ({FME'96})},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
pages = {327--346},
volume = {1051},
year = {1996}
}
@INPROCEEDINGS{FidgeUttingHayesKearney96,
author = {C. J. Fidge and M. Utting and I. J. Hayes and P. Kearney},
title = {The {Quartz} refinement method for real-time multi-tasking systems},
booktitle = {Fifth Australasian Refinement Workshop (ARW'96)},
month = APR,
city = {Brisbane},
year = {1996}
}
@INPROCEEDINGS{Presentation-of-proofs96,
author = {D. A. Carrington and I. J. Hayes and R. Nickson and G. Watson and J. Welsh},
title = {Structured Presentation of Refinements and Proofs},
booktitle = {Proc.\ 19th Australasian Computer Science Conference ({ACSC'96})},
editor = {Kotagiri Ramamohanarao},
series = {Australian Computer Science Communications},
volume = {18(1)},
pages = {87--96},
month = {February},
year = {1996}
}
@INPROCEEDINGS{talp-95,
title = {The communicating technologist: An educational challenge},
author = {P. Bakker and D.A. Carrington and A. Goodchild and I.J. Hayes
and H. Purchase and P.A. Strooper},
booktitle = {Frontiers in Education 25th Annual Conference},
editor = {D. Budny and B. Herrick},
pages = {4a4.1--4a4.4},
publisher = {IEEE Press},
address = {Atlanta, Georgia},
year = 1995
}
@INPROCEEDINGS{Hayes-spec-models,
author = {I. J. Hayes},
title = {Specification Models},
booktitle = {Proc.\ 7th International Conference on
Putting into Practice Methods and Tools for Information Systems Design,
10--12 October, 1995, Nantes},
note = {Invited keynote paper.},
pages = {1--10},
month = OCT,
year = {1995}
}
@ARTICLE{HayesSanders:sepio,
author = {I. J. Hayes and J. W. Sanders},
title = {Specification by interface separation},
journal = {Formal Aspects of Computing},
volume = {7},
number = {4},
pages = {430--439},
pdf = {../Papers/sepio-fac.pdf},
year = {1995}
}
@INPROCEEDINGS{BancroftHayes-type-ext,
author = {P. Bancroft and I. J. Hayes},
title = {A Formal Semantics for a Language with Type Extension},
booktitle = {ZUM'95: The Z Formal Specification Notation, Proc.\ 9th International Conference of Z Users, Limerick, Ireland, September 7--9, 1995},
isbn = {3-540-60271-2},
series = {Lecture Notes in Computer Science},
volume = {967},
publisher = {Springer},
pages = {299--314},
year = {1995}
}
@ARTICLE{HayesMahony-units,
author = {I. J. Hayes and B. P. Mahony},
title = {Using units of measurement in formal specifications},
journal = {Formal Aspects of Computing},
publisher = {BCS/Springer},
volume = {7},
number = {3},
pages = {329--347},
pdf = {../Papers/units.pdf},
year = {1995}
}
@INPROCEEDINGS{RfaPRE,
author = {David Carrington and Ian Hayes and Ray Nickson and Geoffrey Watson and Jim Welsh},
title = {Requirements for a Program Refinement Engine},
booktitle = {Proc.\ of the 4th Australasian Refinement Workshop (ARW'95)},
pages = {67--83},
publisher = {School of Computer Science and Engineering, University of New South Wales},
month = APR,
year = {1995}
}
@TECHREPORT{Tutoring,
author = {Report of the Computer Science Action Learning Group},
title = {Improving the Quality of Tutorial Classes in Computer Science},
institution = {Department of Computer Science, University of Queensland},
number = {UQ-CS-322},
year = {1995}
}
@INPROCEEDINGS{WildmanHayes:UQ2comp,
author = {L. P. Wildman and I. J. Hayes},
key = {Z modularity UQ2 grammar composition},
title = {Composing grammar transformations to construct a specification of a parser},
booktitle = {Proc.\ 18th Australasian Computer Science Conference ({ACSC'95}), Glenelg, South Australia, Australian Computer Science Communications},
editor = {Ramamohanarao Kotagiri},
pages = {556--562},
journal = {Australian Computer Science Communications},
volume = {17(1)},
month = {February},
year = {1995},
abstract = {As part of a project with the aim of scaling up formal
methods, we have developed a library construct for the
specification language Z. This paper reports on the result
of using libraries to structure a specification of a
relatively complicated parser for a language-based editor.
The parser is complicated by the need to cope with multiple
languages as well as tolerate errors in the input.
Our goal in producing the specification of the parser has
been to separate each of the major concepts on which the
specification is based (eg, multiple languages and
error-tolerance) into a separate library.
To achieve the separation of concerns we have applied the
novel technique of specifying each of the major concepts of
the parser as grammar transformations. The full parser can
then be specified by composing the separate transformations
to give a grammar incorporating all the desired features.}
}
@INPROCEEDINGS{boiler-overview,
author = {B. P. Mahony and C. Millerchip and I. J. Hayes},
title = {A boiler control system:
Overview of a case study in timed refinement},
booktitle = {Software Safety: Everybody's Business,
Proceedings of the 1993 International Invitational Workshop on
Design and Review of Software-Controlled Safety-Related Systems,
Ottawa},
editor = {Diana Del Bel Belluz and Herbert C. Ratz},
key = {realtime specification refinement boiler},
publisher = {The Institute of Risk Research},
city = {Waterloo, Canada},
pages = {189--208},
year = {1994}
}
@INPROCEEDINGS{boiler-full,
author = {B. P. Mahony and C. Millerchip and I. J. Hayes},
title = {A boiler control system:
A case study in timed refinement},
booktitle = {Technical proceedings International Symposium on Design and Review of Software-Controlled Safety-Related Systems, Ottawa},
editor = {Diana Del Bel Belluz},
ps = {../Papers/boilerdesign.ps},
key = {realtime specification refinement boiler},
opublisher = {???},
note = {50 pages},
month = {June},
year = {1993}
}
@INPROCEEDINGS{PWI-ARW,
author = {Ray Nickson and Ian Hayes},
title = {Program Window Inference},
booktitle = {Proc.\ of the 4th Australasian Refinement Workshop (ARW'95)},
pages = {43--65},
publisher = {School of Computer Science and Engineering, University of New South Wales},
note = {Unrefereed. Also available as Technical Report UQ-SVRC-95-29, Software Verification Research Centre, University of Queensland},
month = APR,
year = {1995}
}
@ARTICLE{Diff-VDM-Z-SS,
author = {I. J. Hayes and C. B. Jones and J. E. Nicholls},
title = {Understanding the differences between {VDM} and {Z}},
journal = {ACM Software Engineering News},
publisher = {ACM},
note = {Unrefereed. Previously published in {\em FACS Europe} \cite{Diff-VDM-Z}},
volume = {19},
number = {3},
pages = {75--81},
month = {July},
year = {1994}
}
@ARTICLE{Diff-VDM-Z,
author = {I. J. Hayes and C. B. Jones and J. E. Nicholls},
title = {Understanding the differences between {VDM} and {Z}},
journal = {FACS Europe},
volume = {1},
number = {1},
pages = {7--30},
note = {Unrefereed. Also published in {\em ACM Software Engineering News}, 19(3):75--81, July 1994},
dates = {Autumn},
year = {1993}
}
@TECHREPORT{Diff-VDM-Z-TR,
author = {I. J. Hayes and C. B. Jones and J. E. Nicholls},
title = {Understanding the differences between {VDM} and {Z}},
institution = {Department of Computer Science, University of Manchester},
type = {Technical report},
number = {UMCS-93-8-1},
ps = {../Papers/UMCS-93-8-1.ps},
month = {August},
year = {1993}
}
@INPROCEEDINGS{DMDfFS:93,
author = {D. A. Carrington and D. Duke and I. J. Hayes and J. Welsh},
title = {Deriving Modular Designs from Formal Specifications},
booktitle = {{Int.\ Symp.\ on the Foundations of Software Engineering (SIGSOFT'93)}},
location = {Los Angeles},
isbn = {0-89791-625-5},
publisher = {ACM},
pages = {89--98},
pdf = {../Papers/tr93-06.pdf},
year = {1993}
}
@BOOK{SCS2,
editor = {I. J. Hayes},
title = {Specification Case Studies},
edition = {second},
publisher = {Prentice Hall},
opublisher = {Prentice Hall International},
isbn = {0-13-832544-8},
acquired = {30 March 1993},
pdf = {../Papers/SCS2.pdf},
oyear = {1987. Second edition 1993},
year = {1993}
}
@INCOLLECTION{SCS2-eg,
author = {I. J. Hayes},
booktitle = {Specification Case Studies},
edition = {second},
editor = {I. J. Hayes},
pages = {2--13},
publisher = {Prentice Hall International},
title = {Examples of specification using mathematics},
year = {1993}
}
@INCOLLECTION{SCS2-bst,
author = {I. J. Hayes},
booktitle = {Specification Case Studies},
edition = {second},
editor = {I. J. Hayes},
pages = {14--30},
publisher = {Prentice Hall International},
title = {Block-structured symbol table},
year = {1993}
}
@INCOLLECTION{SCS2-flexi,
author = {I. J. Hayes},
booktitle = {Specification Case Studies},
edition = {second},
editor = {I. J. Hayes},
pages = {134--138},
publisher = {Prentice Hall International},
title = {Flexitime specification},
year = {1993}
}
@INCOLLECTION{SCS2-cics,
author = {I. J. Hayes},
booktitle = {Specification Case Studies},
edition = {second},
editor = {I. J. Hayes},
note = {(Previously published in IEEE Transactions on Software Engineering \cite{Hayes85a})},
pages = {181--201},
publisher = {Prentice Hall International},
title = {Applying formal specification to software development in industry},
year = {1993}
}
@INCOLLECTION{SCS2-ts,
author = {I. J. Hayes},
booktitle = {Specification Case Studies},
edition = {second},
editor = {I. J. Hayes},
pages = {226--237},
publisher = {Prentice Hall International},
title = {{CICS} temporary storage},
year = {1993}
}
@INCOLLECTION{SCS2-mess,
author = {I. J. Hayes},
booktitle = {Specification Case Studies},
edition = {second},
editor = {I. J. Hayes},
pages = {238--243},
publisher = {Prentice Hall International},
title = {{CICS} message system},
year = {1993}
}
@INPROCEEDINGS{BancroftHayes:RaMwOT,
author = {P. Bancroft and I. J. Hayes},
booktitle = {Proceedings, 16th Australian Computer Science Conference, Brisbane, Australian Computer Science Communications},
editor = { Gopal Gupta and George Mohay and Rodney Topor},
opublisher = {ACSC-16},
title = {Refining a Module with Opaque Types},
journal = {Australian Computer Science Communications},
volume = {15(1)},
pages = {615--624},
month = {February},
year = {1993}
}
@INPROCEEDINGS{HayesWildman:zmod,
author = {I. J. Hayes and L. P. Wildman},
booktitle = {Z User Workshop: Proceedings of the Seventh Annual {Z} User Meeting, London, December 1992},
editor = {J. P. Bowen and J. E. Nicholls},
key = {Z modularity},
publisher = {Springer},
title = {Towards Libraries for {Z}},
series = {Workshops in Computing},
pages = {37--51},
isbn = {3-540-19818-0},
year = {1993}
}
@ARTICLE{MahonyHayes:Mine,
author = {B. P. Mahony and I. J. Hayes},
title = {A case-study in timed refinement: A mine pump},
journal = {IEEE Trans.\ on Software Engineering},
volume = 18,
number = 9,
pages = {817--826},
pdf = {../Papers/mahony92mine.pdf},
year = {1992}
}
@ARTICLE{Hayes90f,
author = {I. J. Hayes},
title = {{VDM} and {Z}: A comparative case study},
journal = {Formal Aspects of Computing},
volume = {4},
number = {1},
pages = {76--99},
pdf = {../Papers/ndb.pdf},
category = {D},
year = 1992
}
@ARTICLE{Hayes89e,
author = {I. J. Hayes},
title = {Multi-Relations in {Z}: A cross between multi-sets and binary relations},
journal = {Acta Informatica},
volume = {29},
number = {1},
pages = {33--62},
pdf = {../Papers/mrelpap.pdf},
month = {February},
category = {D},
year = 1992
}
@INPROCEEDINGS{WardHayes91a,
author = {N. Ward and I. J. Hayes},
booktitle = {Proc.\ 6th Australian Software Engineering Conference (ASWEC91)},
editor = {P. A. Bailes},
pages = {391--404},
publisher = {Australian Computer Society},
title = {Applications of Angelic Nondeterminism},
city = {Sydney},
month = JUL,
category = {M},
year = {1991}
}
@INPROCEEDINGS{MahonyHayes91b,
author = {B. P. Mahony and I. J. Hayes},
booktitle = {Proc.\ 6th Australian Software Engineering Conf.\ (ASWEC91)},
editor = {P. A. Bailes},
pages = {257--270},
publisher = {Australian Comp.\ Soc.},
title = {Using continuous real functions to model timed histories},
pdf = {../Papers/mahony91continuity.pdf},
city = {Sydney},
category = {M},
year = {1991}
}
@INPROCEEDINGS{MahonyHayes91a,
author = {B. P. Mahony and I. J. Hayes},
booktitle = {Proc.\ BCS/FACS Fourth Refinement Workshop},
publisher = {Springer},
title = {A case study in timed refinement: A central heater},
city = {Cambridge},
pages = {138--149},
pdf = {../Papers/mahony91heater.pdf},
series = {Workshops in Computing},
month = JAN,
year = {1991}
}
@INCOLLECTION{Hayes90e,
author = {I. J. Hayes},
booktitle = {System and Software Requirements Engineering},
editor = {Richard H. Thayer and Merlin Dorfman},
note = {(Previously published in IEEE Transactions on Software Engineering \cite{Hayes85a})},
annote = {This paper was selected for inclusion in the tutorial by the editors},
pages = {594--603},
publisher = {IEEE Computer Society Press Tutorial},
title = {Applying Formal Specification to Software Development in Industry},
year = 1990
}
@INPROCEEDINGS{Hayes90d,
author = {I. J. Hayes},
booktitle = {Z User Workshop: Proceedings of the Fifth Annual {Z} User Meeting, Oxford, December 1990},
key = {Z schema operators},
publisher = {Springer},
title = {Interpretations of {Z} schema operators},
series = {Workshops in Computing},
pages = {12--26},
year = {1991}
}
@INPROCEEDINGS{CarringtonHayesWelsh90,
author = {D. A. Carrington and I. J. Hayes and J. Welsh},
booktitle = {Proc.\ of Pacific TOOLS '90},
key = {Z object oriented},
title = {A Syntax-Directed Editor for Object-Oriented Specifications},
pages = {46--57},
city = {Sydney},
month = NOV,
year = {1990}
}
@TECHREPORT{Hayes90b-TR,
author = {I. J. Hayes},
institution = {Department of Computer Science, University of Queensland},
title = {Specifying Physical Limitations: A Case Study of an Oscilloscope},
type = {Technical report},
number = {167},
month = {July},
pages = {17 pages},
ps = {../Papers/TR0167.ps},
year = 1990
}
@INPROCEEDINGS{HayesNeucomWelsh89,
author = {I. J. Hayes and R. Neucom and J. Welsh},
booktitle = {Advance papers CASE'89},
city = {London},
key = {Z language},
title = {An Editor for {Z} Specifications},
pages = {1--13},
year = {1989}
}
@INPROCEEDINGS{Hayes89a,
author = {I. J. Hayes},
booktitle = {Z User Workshop: Proceedings of the Fourth Annual {Z} User Meeting, Oxford, December 1989},
editor = {J. E. Nicholls},
key = {Z language bags},
publisher = {Springer},
city = {London},
title = {A generalisation of bags in {Z}},
series = {Workshops in Computing},
uqcall = {QA76.73.Z2},
pages = {113--127},
year = {1990}
}
@ARTICLE{HayesJones89,
author = {I. J. Hayes and C. B. Jones},
journal = {IEE/BCS Software Engineering Journal},
month = {November},
number = {6},
pages = {330--338},
title = {Specifications are not (necessarily) executable},
volume = {4},
year = {1989}
}
@INPROCEEDINGS{HayesMowbrayRose89,
author = {I. J. Hayes and M. Mowbray and G. A. Rose},
booktitle = {Protocol Specification, Testing and Verification, {IX}},
editor = {E. Brinksma and G. Scollo and C. A. Vissers},
pages = {3--14},
title = {{Signalling System No. 7}: The Network Layer},
publisher = {Elsevier Science Publishers B. V. (North-Holland)},
year = {1990}
}
@TECHREPORT{HayesNeucomWelsh88,
author = {I. J. Hayes and R. Neucom and J. Welsh},
title = {An editor for {Z} specifications},
pages = {13 pages},
institution = {Department of Computer Science, University of Queensland},
year = {1988}
}
@INPROCEEDINGS{DukeHayesKingRose88,
author = {R. Duke and I. J. Hayes and P. King and G. A. Rose},
booktitle = {IFIP Eighth International Workshop on Protocol Specification, Testing and Verification},
pages = {33--46},
title = {Protocol Specification and Verification Using {Z}},
publisher = {North-Holland},
year = {1988}
}
@TECHREPORT{DukeHayesRose88,
author = {R. Duke and I. J. Hayes and G. A. Rose},
title = {Verification of a cyclic retransmission protocol},
number = {UQ-CS-92},
pages = {1--23},
institution = {Department of Computer Science, The University of Queensland},
month = {July},
year = {1988}
}
@INPROCEEDINGS{HoareHayesEtcFull92,
author = {C. A. R. Hoare and I. J. Hayes and {He Jifeng} and C. Morgan and A. W. Roscoe and J. W. Sanders and I. H. S{\o}rensen and J. M. Spivey and B. A. Sufrin},
title = {Laws of Programming},
booktitle = {Programming and Mathematical Method},
editor = {Manfred Broy},
series = {NATO ASI Series F: Computer and Systems Sciences},
volume = {88},
key = {Marktoberdorf 1990},
pages = {95-122},
publisher = {Springer},
isbn = {3-540-55558-7},
year = {1992}
}
@ARTICLE{HoareHayesEtcFull87,
author = {C. A. R. Hoare and I. J. Hayes and {He Jifeng} and C. Morgan and A. W. Roscoe and J. W. Sanders and I. H. S{\o}rensen and J. M. Spivey and B. A. Sufrin},
journal = {Communications of the ACM},
key = {full},
month = {August},
number = {8},
pages = {672--686},
title = {Laws of Programming},
volume = {30},
note = {Corrigenda: CACM 30(9):770},
year = {1987}
}
@BOOK{Hayes87a,
editor = {I. J. Hayes},
key = {book editor cics distributed computing caviar icl data dictionary unix file},
pages = {332 pages},
publisher = {Prentice Hall International},
title = {Specification Case Studies},
year = {1987}
}
@INPROCEEDINGS{Hayes87h,
address = {Canberra},
author = {I. J. Hayes},
booktitle = {Proc.\ 2nd Australian Software Engineering Conference (ASWEC-87)},
key = {Z language},
month = MAY,
dates = {13--15 May},
pages = {75--86},
publisher = {IREE (Australia)},
title = {Correctness of data representations},
year = {1987}
}
@INPROCEEDINGS{RoseDukeHayes87,
address = {Canberra},
author = {G. A. Rose and R. Duke and I. J. Hayes},
booktitle = {Proc 2nd Australian Software Engineering Conference (ASWEC-87)},
key = {Z language},
month = MAY,
dates = {13--15 May},
pages = {161--170},
publisher = {IREE (Australia)},
title = {Specifying communications services and protocols},
year = {1987}
}
@TECHREPORT{HayesRobinson87,
address = {Brisbane, Australia},
author = {I. J. Hayes and K. A. Robinson},
institution = {Department of Computer Science, University of Queensland},
pages = {35 pages},
title = {A {Modula}-2-Based Translator Generator},
type = {Technical report 84},
year = {1987}
}
@INPROCEEDINGS{Hayes86c,
address = {Canberra},
author = {I. J. Hayes},
booktitle = {Proc.\ 1st Australian Software Engineering Conference (ASWEC-86)},
key = {z specification language},
month = MAY,
dates = {14--16 May},
pages = {67--71},
publisher = {Institution of Engineers, Australia},
title = {Using mathematics to specify software},
note = {At the 10th ASWEC Conference in 1997 this paper was given the
award of {\em Most Influential Paper of ASWEC'86}, the
first ASWEC Conference},
pdf = {../Papers/aswec.pdf},
year = {1986}
}
@INPROCEEDINGS{Hayes86b,
address = {Canberra},
author = {I. J. Hayes},
booktitle = {Proc.\ 9th Australian Computer Science Conference},
month = JAN,
conference = {29--31 January},
pages = {299--308},
title = {Weakest pre-specifications: weakest pre-conditions for procedures},
year = {1986}
}
@ARTICLE{Hayes86a,
author = {I. J. Hayes},
howpublished = {PRG-49},
journal = {IEEE Transactions on Software Engineering},
key = {abstract data type invariant retrival function Z},
month = {January},
number = {1},
pages = {124--133},
title = {Specification directed module testing},
pdf = {../Papers/spectest.pdf},
volume = {SE-12},
year = {1986}
}
@ARTICLE{Hayes85a,
annote = {Field Hayes 1985},
author = {I. J. Hayes},
journal = {IEEE Transactions on Software Engineering},
key = {orig Z Language, CICS},
month = {February},
number = {2},
pages = {169--178},
title = {Applying formal specification to software development in industry},
pdf = {../Papers/cics-r.pdf},
volume = {SE-11},
year = {1985}
}
@PHDTHESIS{Hayes83,
address = {Sydney, Australia},
author = {I. J. Hayes},
pages = {261 pages},
school = {Department of Computer Science, University of New South Wales},
title = {Computer Architecture: The hardware/software interface},
type = {{Ph.\ D.} Thesis},
year = {1983}
}
@TECHREPORT{HayesRobinson82,
address = {Sydney, Australia},
author = {I. J. Hayes and K. A. Robinson},
institution = {Department of Computer Science, University of New South Wales},
pages = {27 pages},
title = {A Tutorial on {Llama}: A {Pascal}-Based Translator Generator},
type = {Technical report},
year = {1982}
}
This file has been generated by bibtex2html 1.88.
Last updated: