@COMMENT{{This file has been generated by bib2bib 1.88}}
@COMMENT{{Command line: /usr/bin/bib2bib -ob ARTICLE.bib -oc ARTICLE-cites -c 'not $key : "TRX$"' -c '$type : "^ARTICLE$"' ../pubs-html.bib}}
@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}
}
@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
}
@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}
}
@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}
}
@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.}
}
@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.}
}
@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.}
}
@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.}
}
@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}
}
@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}
}
@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.}
}
@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}
}
@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}
}
@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}
}
@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}
}
@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
}
@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}
}
@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}
}
@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}
}
This file has been generated by bibtex2html 1.88.
Last updated: