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