Publications by Ian Hayes

[1] BraeJ. Webb, IanJ. Hayes, and Mark Utting. Verifying term graph optimizations using Isabelle/HOL. In Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2023, pages 320--333, New York, NY, USA, 2023. Association for Computing Machinery. [bib| DOI| http]
Our objective is to formally verify the correctness of the hundreds of expression optimization rules used within the GraalVM compiler. When defining the semantics of a programming language, expressions naturally form abstract syntax trees, or, terms. However, in order to facilitate sharing of common subexpressions, modern compilers represent expressions as term graphs. Defining the semantics of term graphs is more complicated than defining the semantics of their equivalent term representations. More significantly, defining optimizations directly on term graphs and proving semantics preservation is considerably more complicated than on the equivalent term representations. On terms, optimizations can be expressed as conditional term rewriting rules, and proofs that the rewrites are semantics preserving are relatively straightforward. In this paper, we explore an approach to using term rewrites to verify term graph transformations of optimizations within the GraalVM compiler. This approach significantly reduces the overall verification effort and allows for simpler encoding of optimization rules.
Keywords: sea-of-nodes intermediate representation, GraalVM compiler, verified code optimizer, Isabelle/HOL
[2] Nasos Evangelou-Oost, Callum Bannister, and IanJ. Hayes. Contextuality in distributed systems. In Roland Glück, Luigi Santocanale, and Michael Winter, editors, Relational and Algebraic Methods in Computer Science, pages 52--68, Cham, 2023. Springer International Publishing. [bib| DOI]
We present a lattice of distributed program specifications, whose ordering represents implementability/refinement. Specifications are modelled by families of subsets of relative execution traces, which encode the local orderings of state transitions, rather than their absolute timing according to a global clock. This is to overcome fundamental physical difficulties with synchronisation. The lattice of specifications is assembled and analysed with several established mathematical tools. Sets of nondegenerate cells of a simplicial set are used to model relative traces, presheaves model the parametrisation of these traces by a topological space of variables, and information algebras reveal novel constraints on program correctness. The latter aspect brings the enterprise of program specification under the widening umbrella of contextual semantics introduced by Abramsky et al. In this model of program specifications, contextuality manifests as a failure of a consistency criterion comparable to Lamport's definition of sequential consistency. The theory of information algebras also suggests efficient local computation algorithms for the verification of this criterion. The novel constructions in this paper have been verified in the proof assistant Isabelle/HOL.
[3] Mark Utting, BraeJ. Webb, and IanJ. Hayes. Differential testing of a verification framework for compiler optimizations (case study). In FormaliSE 2023. IEEE, 2023. [bib]
We want to verify the correctness of optimization phases in the GraalVM compiler, which consist of many thousands of lines of complex Java code performing sophisticated graph transformations. We have built high-level models of the data structures and operations of the code using the Isabelle/HOL theorem prover, and can formally verify the correctness of those high-level operations. But the remaining challenge is: how can we be sure that those high-level operations accurately reflect what the Java is doing? This paper addresses that issue by applying several different kinds of differential testing to validate that the formal model and the Java code have the same semantics. The lessons learned from applying these validation techniques should be applicable to other projects that are building formal models of real-world code.
Keywords: Logic in Computer Science (cs.LO), Programming Languages (cs.PL), Software Engineering (cs.SE), FOS: Computer and information sciences, FOS: Computer and information sciences
[4] LarissaA. Meinicke and IanJ. Hayes. Using cylindric algebra to support local variables in rely/guarantee concurrency. In 2023 IEEE/ACM 11th International Conference on Formal Methods in Software Engineering (FormaliSE), pages 108--119. IEEE, 2023. [bib| DOI]
Local variable blocks are a simple but effective program structuring technique. In the context of concurrency, local variables have the added advantage of avoiding interference from threads running concurrently with the thread containing the local variable. To provide mechanised support for verifying concurrent programs in Isabelle/HOL, we have found making use of algebraic properties of programs simplifies the development of refinement laws. The algebraic properties of local variable blocks are similar to those of existential quantifiers in predicate calculus, the algebra of which is Tarski's cylindric algebra. Hence to support local variables, we make use of a variant of cylindric algebra that allows quantification of a variable over a command, rather than a predicate. The approach allows a local variable to become a shared variable of parallel threads that are local to the block that introduced the variable.
Keywords: Rely/guarantee concurrency, Concurrent program verification, Program algebra, Cylindric algebra, Local variables
[5] IanJ. Hayes, CliffB. Jones, and LarissaA. Meinicke. Specifying and reasoning about shared-variable concurrency. In JonathanP. Bowen, Qin Li, and Qiwen Xu, editors, Theories of Programming and Formal Methods: Essays Dedicated to Jifeng He on the Occasion of His 80th Birthday, volume 14080 of Lecture Notes in Computer Science, pages 110--135, Cham, 2023. Springer Nature Switzerland AG. [bib| DOI]
Specifications are a necessary reference point for correctness arguments. Top-down descriptions of concurrent programs require a way of recording information about the environment in which the component will be required to function. It was shown in the 1980s that adding rely and guarantee conditions to pre and post conditions could support formal specification and reasoning about a class of concurrent systems. More recent research has both widened the class of specifications to include progress requirements and facilitated mechanisation of proofs. This paper describes the algebraic underpinnings that have made this possible. Particular attention is paid to notions of atomicity.
[6] Naso Evangelou-Oost, Larissa Meinicke, Callum Bannister, and IanJ. Hayes. Trace models of concurrent valuation algebras. In YiLi and Sofiène Tahar, editors, Formal Methods and Software Engineering (ICFEM 2023), volume 14308 of Lecture Notes in Computer Science, pages 118--136, Singapore, 2023. Springer Nature. [bib| DOI]
This paper introduces Concurrent Valuation Algebras (CVAs), a novel extension of ordered valuation algebras (OVAs). CVAs include two combine operators representing parallel and sequential prod- ucts, adhering to a weak exchange law. This development offers theoret- ical and practical benefits for the specification and modelling of concur- rent and distributed systems. As a presheaf on a space of domains, CVAs enable localised specifications, supporting modularity, compositionality, and the ability to represent large and complex systems. Furthermore, CVAs align with lattice-based refinement reasoning and are compatible with established methodologies such as Hoare and Rely-Guarantee logics. The flexibility of CVAs is explored through three trace models, illustrat- ing distinct paradigms of concurrent/distributed computing, interrelated by morphisms. The paper also highlights the potential to incorporate a powerful local computation framework from valuation algebras for model checking in concurrent and distributed systems. The foundational results presented have been verified with the proof assistant Isabelle/HOL.
[7] IanJ. Hayes, Mark Utting, and BraeJ. Webb. Verifying compiler optimisations. In YiLi and Sofiène Tahar, editors, Formal Methods and Software Engineering (ICFEM 2023), volume 14308 of Lecture Notes in Computer Science, pages 3--8, Singapore, 2023. Springer Nature. Invited paper. [bib| DOI]
Compilers are a vital tool but errors in a compiler can lead to errors in the myriad of programs it compiles. Our research focuses on verifying the optimisation phase because it is a common source of errors within compilers. In programming language semantics, expressions (or terms) are represented by abstract syntax trees, and their semantics is expressed over their (recursive) structure. Optimisations can then be represented by conditional term rewriting rules. The correctness of these rules is verified in Isabelle/HOL. In the GraalVM compiler, the intermediate representation is a sea-of-nodes graph structure that combines data flow and control flow in the one graph. The data flow sub-graphs correspond to term graphs, and the term rewriting rules apply equally to this representation.
[8] BraeJ. Webb, Mark Utting, and IanJ. Hayes. A formal semantics of the GraalVM intermediate representation. In Zhe Hou and Vijay Ganesh, editors, Automated Technology for Verification and Analysis, volume 12971 of Lecture Notes in Computer Science, pages 111--126, Cham, October 2021. Springer International Publishing. [bib| DOI]
The optimization phase of a compiler is responsible for transforming an intermediate representation (IR) of a program into a more efficient form. Modern optimizers, such as that used in the GraalVM compiler, use an IR consisting of a sophisticated graph data structure that combines data flow and control flow into the one structure. As part of a wider project on the verification of optimization passes of GraalVM, this paper describes a semantics for its IR within Isabelle/HOL. The semantics consists of a big-step operational semantics for data nodes (which are represented in a graph-based static single assignment (SSA) form) and a small-step operational semantics for handling control flow including heap-based reads and writes, exceptions, and method calls. We have proved a suite of canonicalization optimizations and conditional elimination optimizations with respect to the semantics.
[9] B.Dongol, I.J. Hayes, and G.Struth. Convolution algebras: Relational convolution, generalised modalities and incidence algebras. Logical Methods in Computer Science, 17(1):13:1--13:34, February 2021. [bib| DOI]
Convolution is a ubiquitous operation in mathematics and computing. The Kripke semantics for substructural and interval logics motivates its study for quantale-valued functions relative to ternary relations. The resulting notion of relational convolution leads to generalised binary and unary modal operators for qualitative and quantitative models, and to more conventional variants, when ternary relations arise from identities over partial semigroups. Convolution-based semantics for fragments of categorial, linear and incidence (segment or interval) logics are provided as qualitative applications. Quantitative examples include algebras of durations and mean values in the duration calculus.
Keywords: relational convolution, relational semigroup, partial semigroup, quantale, convolution algebra, modal algebra, substructural logics, interval logics, duration calculus
[10] IanJ. Hayes, LarissaA. Meinicke, and PatrickA. Meiring. Deriving laws for developing concurrent programs in a rely-guarantee style, 2021. Ext. report at arXiv:2103.15292. [bib| arXiv| http]
[11] IanJ. Hayes and Steve King. Software specification. In CliffB. Jones and Jayadev Misra, editors, Theories of Programming: The Life and Works of Tony Hoare, page 251–270, New York, NY, USA, 2021. Association for Computing Machinery. [bib| http]
[12] A.Burns, I.J. Hayes, and C.B. Jones. Deriving specifications of control programs for cyber physical systems. The Computer Journal, 63(5):774--790, May 2020. [bib| DOI| http]
Cyber physical systems (CPS) exist in a physical environment and comprise both physical components and a control program. Physical components are inherently liable to failure and yet an overall CPS is required to operate safely, reliably and cost effectively. This paper proposes a framework for deriving the specification of the software control component of a CPS from an understanding of the behaviour required of the overall system in its physical environment. The two key elements of this framework are (i) an extension to the use of rely/guarantee conditions to allow specifications to be obtained systematically from requirements (as expressed in terms of the required behaviour in the environment) and nested assumptions (about the physical components of the CPS); and (ii) the use of time bands to record the temporal properties required of the CPS at a number of different granularities. The key contribution is in combining these ideas; using time bands overcomes a significant drawback in earlier work. The paper also addresses the means by which the reliability of a CPS can be addressed by challenging each rely condition in the derived specification and, where appropriate, improve robustness and/or define weaker guarantees that can be delivered with respect to the corresponding weaker rely conditions.
Keywords: Cyber-physical systems; real-time systems; time bands; rely-guarantee; concurrency; embedded systems
[13] I.J. Hayes and L.A. Meinicke. Developing an algebra for rely/guarantee concurrency: design decisions and challenges. In Pedro Ribeiro and Augusto Sampaio, editors, Unifying Theories of Programming 2019, volume 11885 of Lecture Notes in Computer Science, pages 176--197, Cham, October 2019. Springer International Publishing. [bib| DOI]
An algebra for rely/guarantee concurrency has beenc onstructed via a hierarchy of algebraic theories starting from basic theories like lattices through to theories of synchronous behaviour of atomic steps and a theory to support localisation. The algebra is supported by a model based on Aczel traces. We examine the role of these theories in developing a mechanised theory for deriving concurrent programs and outline some of the challenges remaining.
[14] IanJ. Hayes, LarissaA. Meinicke, Kirsten Winter, and RobertJ. Colvin. A synchronous program algebra: a basis for reasoning about shared-memory and event-based concurrency. Formal Aspects of Computing, 31(2):133--163, April 2019. [bib| DOI]
In this paper we introduce an abstract algebra for reasoning about concurrent programs, that includes an abstract algebra of atomic steps, with sub-algebras of program and environment steps, and an abstract synchronisation operator. We show how the abstract synchronisation operator can be instantiated as a synchronous parallel operator with interpretations in rely-guarantee concurrency for shared-memory systems, and in process algebras CCS and CSP. It is also instantiated as a weak conjunction operator, an operator that is useful for the specification of rely and guarantee conditions in rely/guarantee concurrency. The main differences between the parallel and weak conjunction instantiations of the synchronisation operator are how they combine individual atomic steps. Lemmas common to these different instantiations are proved once using the axiomatisation of the abstract synchronous operator. Using the sub-algebras of program and environment atomic steps, rely and guarantee conditions, as well as Morgan-style specification commands, are defined at a high-level of abstraction in the program algebra. Lifting these concepts from rely/guarantee concurrency to a higher level of abstraction makes them more widely applicable. We demonstrate the practicality of the algebra by showing how a core law from rely-guarantee theory, the parallel introduction law, can be abstracted and verified easily in the algebra. In addition to proving fundamental properties for reasoning about concurrent shared-variable programs, the algebra is instantiated to prove abstract process synchronisation properties familiar from the process algebras CCS and CSP. The algebra has been encoded in Isabelle/HOL to provide a basis for tool support for concurrent program verification based on the rely/guarantee technique. It facilitates simpler, more general, proofs that allow a higher level of automation than what is possible in low-level, model-specific interpretations.
Keywords: Refinement calculus; synchronous parallel; concurrency; program algebra; rely-guarantee
[15] B.Dongol, I.J. Hayes, L.A. Meinicke, and G.Struth. Cylindric Kleene lattices for program construction. In G.Hutton, editor, Mathematics of Program Construction 2019, volume 11825 of Lecture Notes in Computer Science, pages 197--225, Cham, 2019. Springer International Publishing. [bib| DOI]
Cylindric algebras have been developed as an algebraisation of equational first order logic. We adapt them to cylindric Kleene lattices and their variants and present relational and relational fault models for these. This allows us to encode frames and local variable blocks, and to derive Morgan's refinement calculus as well as an algebraic Hoare logic for while programs with assignment laws. Our approach thus opens the door for algebraic calculations with program and logical variables instead of domain-specific reasoning over concrete models of the program store. Refinement proofs for small programs are presented as examples.
[16] X.Wu, Y.Lu, P.Meiring, I.J. Hayes, and L.A. Meinicke. Type capabilities for object-oriented programming languages. In Jing Sun and Meng Sun, editors, Formal Methods and Software Engineering (ICFEM), volume 11232 of Lecture Notes in Computer Science, pages 215--230, Cham, November 2018. Springer International Publishing. [bib| DOI]
[17] I.J. Hayes. Engineering a theory of concurrent programming. In Jing Sun and Meng Sun, editors, Formal Methods and Software Engineering (ICFEM), volume 11232 of Lecture Notes in Computer Science, pages 3--18, Cham, November 2018. Springer International Publishing. Invited keynote paper. [bib| DOI]
Our original goal was to develop a refinement calculus for shared-memory concurrent programs to support Jones-style rely/guarantee developments. Our semantics was based on Aczel traces, which explicitly include environment steps as well as program steps, and were originally proposed as a basis for showing the rely/guarantee rules are sound. Where we have ended up is with a hierarchy of algebraic theories that provide a foundation for concurrent program refinement, which allows us to prove Jones-style rely/guarantee laws, as well as new laws. Our algebraic theory is based on a lattice of commands that includes a sub-lattice of test commands (similar to Kozen's Kleene Algebra with Tests) and a sub-algebra of atomic step commands (similar to Milner's SCCS) but with a structure that supports Aczel's program and environment steps as atomic step commands. The latter allows us to directly encode rely and guarantee commands to represent rely/guarantee specifications, and to encode fair execution of a command.
[18] IanJ. Hayes. Some challenges of specifying concurrent program components. In John Derrick, Brijesh Dongol, and Steve Reeves, editors, Proceedings 18th Refinement Workshop, Oxford, UK, 18th July 2018, volume 282 of Electronic Proceedings in Theoretical Computer Science, pages 10--22. Open Publishing Association, October 2018. [bib| DOI]
The purpose of this paper is to address some of the challenges of formally specifying components of shared-memory concurrent programs. The focus is to provide an abstract specification of a component that is suitable for use both by clients of the component and as a starting point for refinement to an implementation of the component. We present some approaches to devising specifications, investigating different forms suitable for different contexts. We examine handling atomicity of access to data structures, blocking operations and progress properties, and transactional operations that may fail and need to be retried.
[19] I.J. Hayes and L.A. Meinicke. Encoding fairness in a synchronous concurrent program algebra. In Klaus Havelund, Jan Peleska, Bill Roscoe, and Erik deVink, editors, Formal Methods, Lecture Notes in Computer Science, pages 222--239, Cham, July 2018. Springer International Publishing. [bib| DOI]
Concurrent program refinement algebra provides a suitable basis for supporting mechanised reasoning about shared-memory concurrent programs in a compositional manner, for example, it supports the rely/guarantee approach of Jones. The algebra makes use of a synchronous parallel operator motivated by Aczel?s trace model of concurrency and with similarities to Milner?s SCCS. This paper looks at defining a form of fairness within the program algebra. The encoding allows one to reason about the fair execution of a single process in isolation as well as define fair-parallel in terms of a base parallel operator, of which no fairness properties are assumed. An algebraic theory to support fairness and fair-parallel is developed.
[20] IanJ. Hayes and LarissaA. Meinicke. Encoding fairness in a synchronous concurrent program algebra: extended version with proofs, May 2018. [bib| arXiv| http]
[21] I.J. Hayes and C.B. Jones. A guide to rely/guarantee thinking. In J.P. Bowen, Z.Liu, and Z.Zhang, editors, Engineering Trustworthy Software Systems, volume 11174 of Lecture Notes in Computer Science, pages 1--38, Cham, 2018. Springer International Publishing. [bib| DOI]
Designing concurrent shared-variable programs is difficult. The Rely-Guarantee concept provides a compositional approach to the challenge. This paper reviews some recent developments in the approach, offers worked examples and relates the approach to other research.
[22] Brijesh Dongol, Victor B.F. Gomes, IanJ. Hayes, and Georg Struth. Partial semigroups and convolution algebras. Archive of Formal Proofs, June 2017. https://www.isa-afp.org/entries/PSemigroupsConvolution.shtml, Formal proof development. [bib]
Partial Semigroups are relevant to the foundations of quantum mechanics and combinatorics as well as to interval and separation logics. Convolution algebras can be understood either as algebras of generalised binary modalities over ternary Kripke frames, in particular over partial semigroups, or as algebras of quantale-valued functions which are equipped with a convolution-style operation of multiplication that is parametrised by a ternary relation. Convolution algebras provide algebraic semantics for various substructural logics, including categorial, relevance and linear logics, for separation logic and for interval logics; they cover quantitative and qualitative applications. These mathematical components for partial semigroups and convolution algebras provide uniform foundations from which models of computation based on relations, program traces or pomsets, and verification components for separation or interval temporal logics can be built with little effort.
[23] R.J. Colvin, I.J. Hayes, and L.A. Meinicke. Designing a semantic model for a wide-spectrum language with concurrency. Formal Aspects of Computing, 29:853--875, 2017. Online 27 February 2017. [bib]
A wide-spectrum language integrates specification constructs into a programming language in a manner that treats a specification command just like any other command. The primary contribution of this paper is a semantic model for a wide-spectrum language that supports concurrency and a refinement calculus. A distinguishing feature of the language is that steps of the environment are modelled explicitly, alongside steps of the program. From these two types of steps a rich set of specification commands can be constructed, based on operators for nondeterministic choice, and sequential and parallel composition. We also introduce a novel operator, weak conjunction, which is used extensively to conjoin separate aspects of specifications, allowing us to take a separation-of-concerns approach to subsequent reasoning. We provide a denotational semantics for the language based on traces, which may be terminating, aborting, infeasible, or infinite.

To demonstrate the generality and unifying strength of the language, we use it to express a range of concepts from the concurrency literature, including: a refinement theory for rely/guarantee reasoning; an abstract specification of local variables in a concurrent context; specification of an abstract, linearisable data structure; a partial encoding of temporal logic; and defining the relationships between notions of nonblocking programs. The novelty of the paper is that these diverse concepts build on the same theory. In particular, the rely concept from Jones' rely/guarantee framework, and a stronger demand concept that restricts the environment, are reused across the different domains to express assumptions about the environment. The language and model form an instance of an abstract concurrent program algebra, and this facilitates reasoning about properties of the model at a high level of abstraction.

Keywords: Refinement calculus; wide-spectrum language; concurrency; program algebra; rely-guarantee
[24] IanJ. Hayes, XiWu, and LarissaA. Meinicke. Capabilities for Java: Secure access to resources. In Bor-YuhEvan Chang, editor, Programming Languages and Systems: 15th Asian Symposium, APLAS 2017, Suzhou, China, November 27-29, 2017, Proceedings, pages 67--84, Cham, 2017. Springer International Publishing. [bib| DOI| http]
This paper explores adding capabilities to Java with the objective of tightening security management for access to resources both within the Java Class Library and Java applications. Code can only access resources if it is given explicit capabilities, allowing replacement of the use of doPrivileged blocks. Capabilities provide restricted access to their implementing object -- like an interface -- but when a capability is created, it has a more restrictive dynamic type than its implementing object, and hence access to the full facilities of the implementing object (e.g. via down casting) are precluded. We used the Annotation Processing Tool to track the declaration and use of capabilities.
[25] IanJ. Hayes, LarissaA. Meinicke, Kirsten Winter, and RobertJ. Colvin. A synchronous program algebra: a basis for reasoning about shared-memory and event-based concurrency, 2017. https://arxiv.org/abs/1710.03352. [bib| arXiv| http]
[26] J.Fell, I.J. Hayes, and A.Velykis. Concurrent refinement algebra and rely quotients. Archive of Formal Proofs, December 2016. http://isa-afp.org/entries/Concurrent_Ref_Alg.shtml, Formal proof development. [bib]
The concurrent refinement algebra developed here is designed to provide a foundation for rely/guarantee reasoning about concurrent programs. The algebra builds on a complete lattice of commands by providing sequential composition, parallel composition and a novel weak conjunction operator. The weak conjunction operator coincides with the lattice supremum providing its arguments are non-aborting, but aborts if either of its arguments do. Weak conjunction provides an abstract version of a guarantee condition as a guarantee process. We distinguish between models that distribute sequential composition over non-deterministic choice from the left (referred to as being conjunctive in the refinement calculus literature) and those that don't. Least and greatest fixed points of monotone functions are provided to allow recursion and iteration operators to be added to the language. Additional iteration laws are available for conjunctive models. The rely quotient of processes c and i is the process that, if executed in parallel with i implements c. It represents an abstract version of a rely condition generalised to a process.
[27] IanJ. Hayes. Generalised rely-guarantee concurrency: An algebraic foundation. Formal Aspects of Computing, 28(6):1057--1078, November 2016. [bib| DOI| http]
The rely-guarantee technique allows one to reason compositionally about concurrent programs. To handle interference the technique makes use of rely and guarantee conditions, both of which are binary relations on states. A rely condition is an assumption that the environment performs only atomic steps satisfying the rely relation and a guarantee is a commitment that every atomic step the program makes satisfies the guarantee relation. In order to investigate rely-guarantee reasoning more generally, in this paper we allow interference to be represented by a process rather than a relation and hence derive more general rely-guarantee laws. The paper makes use of a weak conjunction operator between processes, which generalises a guarantee relation to a guarantee process, and introduces a rely quotient operator, which generalises a rely relation to a process. The paper focuses on the algebraic properties of the general rely-guarantee theory. The Jones-style rely-guarantee theory can be interpreted as a model of the general algebraic theory and hence the general laws presented here hold for that theory.
Keywords: Concurrent programming; rely-guarantee concurrency; program verification; program algebra.
[28] I.J. Hayes, R.Colvin, L.Meinicke, K.Winter, and A.Velykis. An algebra of synchronous atomic steps, November 2016. http://dx.doi.org/10.1007/978-3-319-48989-6_22. [bib| arXiv| http]
This research started with an algebra for reasoning about rely/guarantee concurrency for a shared memory model. The approach taken led to a more abstract algebra of atomic steps, in which atomic steps synchronise (rather than interleave) when composed in parallel. The algebra of rely/guarantee concurrency then becomes an interpretation of the more abstract algebra. Many of the core properties needed for rely/guarantee reasoning can be shown to hold in the abstract algebra where their proofs are simpler and hence allow a higher degree of automation. Moreover, the realisation that the synchronisation mechanisms of standard process algebras, such as CSP and CCS/SCCS, can be interpreted in our abstract algebra gives evidence of its unifying power. The algebra has been encoded in Isabelle/HOL to provide a basis for tool support.
[29] I.J. Hayes, R.Colvin, L.Meinicke, K.Winter, and A.Velykis. An algebra of synchronous atomic steps. In J.Fitzgerald, C.Heitmeyer, S.Gnesi, and A.Philippou, editors, FM 2016: Formal Methods: 21st International Symposium, Limassol, Cyprus, November 9-11, 2016, Proceedings, volume 9995 of Lecture Notes in Computer Science, pages 352--369, Cham, November 2016. Springer International Publishing. Best paper award. [bib| DOI| http]
This research started with an algebra for reasoning about rely/guarantee concurrency for a shared memory model. The approach taken led to a more abstract algebra of atomic steps, in which atomic steps synchronise (rather than interleave) when composed in parallel. The algebra of rely/guarantee concurrency then becomes an interpretation of the more abstract algebra. Many of the core properties needed for rely/guarantee reasoning can be shown to hold in the abstract algebra where their proofs are simpler and hence allow a higher degree of automation. Moreover, the realisation that the synchronisation mechanisms of standard process algebras, such as CSP and CCS/SCCS, can be interpreted in our abstract algebra gives evidence of its unifying power. The algebra has been encoded in Isabelle/HOL to provide a basis for tool support.
[30] CliffB. Jones and IanJ. Hayes. Possible values: Exploring a concept for concurrency. Journal of Logical and Algebraic Methods in Programming, 85(5, Part 2):972--984, August 2016. [bib| DOI| http]
An important issue in concurrency is interference. This issue manifests itself in both shared-variable and communication-based concurrency -- this paper focusses on the former case where interference is caused by the environment of a process changing the values of shared variables. Rely/guarantee approaches have been shown to be useful in specifying and reasoning compositionally about concurrent programs. This paper explores the use of a “possible values” notation for reasoning about variables whose values can be changed multiple times by interference. Apart from the value of this concept in providing clear specifications, it offers a principled way of avoiding the need for some auxiliary (or ghost) variables whose unwise use can destroy compositionality.
Keywords: Concurrent programming
[31] B.Dongol, I.J. Hayes, and G.Struth. Convolution as a unifying concept: Applications in separation logic, interval calculi, and concurrency. ACM Trans. Comput. Logic, 17(3):15:1--15:25, February 2016. [bib| DOI| http]
A notion of convolution is presented in the context of formal power series together with lifting constructions characterising algebras of such series, which usually are quantales. A number of examples underpin the universality of these constructions, the most prominent ones being separation logics, where convolution is separating conjunction in an assertion quantale; interval logics, where convolution is the chop operation; and stream interval functions, where convolution is proposed for analysing the trajectories of dynamical or real-time systems. A Hoare logic can be constructed in a generic fashion on the power-series quantale, which applies to each of these examples. In many cases, commutative notions of convolution have natural interpretations as concurrency operations.
Keywords: Concurrency, Hoare logics, convolution, formal power series, formal semantics, interval logics, quantales, semigroups, separation logics, systems verification
[32] CliffB. Jones, IanJ. Hayes, and RobertJ. Colvin. Balancing expressiveness in formal approaches to concurrency. Formal Aspects of Computing, 27(3):475--497, May 2015. [bib| DOI| http]
One might think that specifying and reasoning about concurrent programs would be easier with more expressive languages. This paper questions that view. Clearly too weak a notation can mean that useful properties either cannot be expressed or their expression is unnatural. But choosing too powerful a notation also has its drawbacks since reasoning receives little guidance. For example, few would suggest that programming languages themselves provide tractable specifications. Both rely/guarantee methods and separation logic(s) provide useful frameworks in which it is natural to reason about aspects of concurrency. Rather than pursue an approach of extending the notations of either approach, this paper starts with the issues that appear to be inescapable with concurrency and --only as a response thereto-- examines ways in which these fundamental challenges can be met. Abstraction is always a ubiquitous tool and its influence on how the key issues are tackled is examined in each case.
Keywords: Concurrency; Rely/guarantee reasoning; Separation logic
[33] IanJ. Hayes. Separating concerns of rely and guarantee in concurrent program derivation. In DavidA. Naumann, editor, Unifying Theories of Programming, UTP 2014, volume 8963 of LNCS, pages vii--x. Springer, 2015. Invited keynote. [bib]
To reason compositionally about concurrent programs one needs to be able to reason about a process in the context of the interference from its environment. Cliff Jones introduced an elegant approach to handle reasoning about interference in terms of rely and guarantee conditions, each of which is a binary relation between program states.

In order to provide a unifying theory of rely-guarantee reasoning, here guarantees and relies are treated as separate forms of specifications in a wide-spectrum language with a single refinement relation. The separate forms of specification allow guarantees and relies to be examined separately, leading to simpler expression of their algebraic properties, as well as in combination, as needed to handle the introduction of a parallel composition.

Keywords:
[34] IanJ. Hayes. Generalised rely-guarantee concurrency: An algebraic foundation, 2015. http://dx.doi.org/10.1007/s00165-012-??-1. [bib| arXiv| http]
The rely-guarantee technique allows one to reason compositionally about concurrent programs. To handle interference the technique makes use of rely and guarantee conditions, both of which are binary relations on states. A rely condition is an assumption that the environment performs only atomic steps satisfying the rely relation and a guarantee is a commitment that every atomic step the program makes satisfies the guarantee relation. In order to investigate rely-guarantee reasoning more generally, in this paper we allow interference to be represented by a process rather than a relation and hence derive more general rely-guarantee laws. The paper makes use of a weak conjunction operator between processes, which generalises a guarantee relation to a guarantee process, and introduces a rely quotient operator, which generalises a rely relation to a process. The paper focuses on the algebraic properties of the general rely-guarantee theory. The Jones-style rely-guarantee theory can be interpreted as a model of the general algebraic theory and hence the general laws presented here hold for that theory.
Keywords: Concurrent programming; rely-guarantee concurrency; program verification; program algebra.
[35] IanJ. Hayes, CliffB. Jones, and RobertJ. Colvin. Laws and semantics for rely-guarantee refinement. Technical Report CS-TR-1425, School of Computing Science, Newcastle University, July 2014. Superseded by [25] and other papers. 66 pages. [bib]
Interference is the essence of concurrency and it is what makes reasoning about concurrent programs difficult. The fundamental insight of rely-guarantee thinking is that stepwise design of concurrent programs can only be compositional in development methods that offer ways to record and reason about interference. In this way of thinking, a rely relation records assumptions about the behaviour of the environment, and a guarantee relation records commitments about the behaviour of the process. The standard application of these ideas is in the extension of Hoare-like inference rules to quintuples that accommodate rely and guarantee conditions. In contrast, in this paper, we embed rely-guarantee thinking into a refinement calculus for concurrent programs, in which programs are developed in (small) steps from an abstract specification. As is usual, we extend the implementation language with specification constructs (the extended language is sometimes called a wide-spectrum language), in this case adding two new commands: a guarantee command (guar g ·c) whose valid behaviours are in accord with the command c but all of whose atomic steps also satisfy the relation g, and a rely command (rely r ·c) whose behaviours are like c provided any interference steps from the environment satisfy the relation r. The theory of concurrent program refinement is based on a theory of atomic program steps and more powerful refinement laws, most notably, a law for decomposing a specification into a parallel composition, are developed from a small set of more primitive lemmas, which are proved sound with respect to an operational semantics.
Keywords: rely-guarantee, concurrency
[36] Brijesh Dongol, IanJ. Hayes, and PeterJ. Robinson. Reasoning about goal-directed real-time teleo-reactive programs. Formal Aspects of Computing, 26(3):563--589, May 2014. [bib| DOI| http]
The teleo-reactive programming model is a high-level approach to developing real-time systems that supports hierarchical composition and durative actions. The model is different from frameworks such as action systems, timed automata and TLA+, and allows programs to be more compact and descriptive of their intended behaviour. Teleo-reactive programs are particularly useful for implementing controllers for autonomous agents that must react robustly to their dynamically changing environments. In this paper, we develop a real-time logic that is based on Duration Calculus and use this logic to formalise the semantics of teleo-reactive programs. We develop rely/guarantee rules that facilitate reasoning about a program and its environment in a compositional manner. We present several theorems for simplifying proofs of teleo-reactive programs and present a partially mechanised method for proving progress properties of goal-directed agents.
Keywords: Teleo-reactive programming; Goal-directed agents; Rely/guarantee reasoning; Real-time programs; Reactive systems; Interval-based logics
[37] Brijesh Dongol, IanJ. Hayes, and John Derrick. Deriving real-time action systems with multiple time bands using algebraic reasoning. Science of Computer Programming, 85 Part B:137--165, 2014. [bib| DOI]
The verify-while-develop paradigm allows one to incrementally develop programs from their specifications using a series of calculations against the remaining proof obligations. This paper presents a derivation method for real-time systems with realistic constraints on their behaviour. We develop a high-level interval-based logic that provides flexibility in an implementation, yet allows algebraic reasoning over multiple granularities and sampling multiple sensors with delay. The semantics of an action system is given in terms of interval predicates and algebraic operators to unify the logics for an action system and its properties, which in turn simplifies the calculations and derivations.
Keywords: Action systems
[38] IanJ. Hayes. Towards structuring system specifications with time bands using layers of rely-guarantee conditions. In C.Artho and P.C. Ölveczky, editors, Formal Techniques for Safety-Critical Systems, volume 419 of Communications in Computer and Information Science, pages 1--2. Springer, 2014. [bib| DOI]
The overall specification of a cyber-physical system can be given in terms of the desired behaviour of its physical components operating within the real world. The specification of its control software can then be derived from the overall specification and the properties of the real-world phenomena, including their relationship to the computer system's sensors and actuators. The control software specification then becomes a combination of the guarantee it makes about the system behaviour and the real-world assumptions it relies upon.

Such specifications can easily become complicated because the complete system description deals with properties of phenomena at widely different time granularities, as well as handling faults. To help manage this complexity, we consider layering the specification within multiple time bands, with the specification of each time band consisting of both the rely and guarantee conditions for that band, both given in terms of the phenomena of that band. The overall specification is then the combination of the multiple rely-guarantee pairs. Multiple rely-guarantee pairs can also be used to handle faults.

Keywords: ?
[39] IanJ. Hayes and Larissa Meinicke. Invariants, well-founded statements and real-time program algebra. In Cliff.B. Jones, P.Pihlajasaari, and Jun Sun, editors, Formal Methods (FM 2014), volume 8442 of LNCS, pages 318--334. Springer, 2014. [bib]
Program algebras based on Kleene algebra abstract the essential properties of programming languages in the form of algebraic laws. The proof of a refinement law may be expressed in terms of the algebraic properties of programs required for the law to hold, rather than directly in terms of the semantics of a language. This has the advantage that the law is then valid for any programming language that satisfies the axioms of the algebra. In this paper we explore the notion of well-founded statements and their relationship to well-founded relations and iterations. The laws about well-founded statements and relations are combined with invariants to derive a simpler proof of a while-loop introduction law. The algebra is then applied to a real-time programming language. The main difference is that tests within conditions and loops take time to evaluate and during that time the values of program inputs may change. This requires new definitions for conditionals and while loops but the proofs of the introduction laws for these constructs can still make use of the more basic algebraic properties of iterations.
Keywords:
[40] IanJ. Hayes, CliffB. Jones, and RobertJ. Colvin. Reasoning about concurrent programs: Refining rely-guarantee thinking. Technical Report CS-TR-1395, School of Computing Science, Newcastle University, September 2013. Superseded by CS-TR-1425. 66 pages. [bib]
Interference is the essence of concurrency and it is what makes reasoning about concurrent programs difficult. The fundamental insight of rely-guarantee thinking is that stepwise design of concurrent programs can only be compositional in development methods that offer ways to record and reason about interference. In this way of thinking, a rely relation records assumptions about the behaviour of the environment, and a guarantee relation records commitments about the behaviour of the process. The standard application of these ideas is in the extension of Hoare-like inference rules to quintuples that accommodate rely and guarantee conditions. In contrast, in this paper, we embed rely-guarantee thinking into a refinement calculus for concurrent programs, in which programs are developed in (small) steps from an abstract specification. As is usual, we extend the implementation language with specification constructs (the extended language is sometimes called a wide-spectrum language), in this case adding (in addition to pre and postconditions) two new commands: a guarantee command (guar g · c) whose valid behaviours are in accord with the command c but all of whose atomic steps also satisfy the relation g, and a rely command (rely r · c) whose behaviours are like c provided any interference steps from the environment satisfy the relation r. The theory of concurrent program refinement is based on a theory of atomic program steps and more powerful refinement laws, most notably, a law for decomposing a specification into a parallel composition, are developed from a small set of more primitive lemmas, which are proved sound with respect to an operational semantics.
Keywords: rely-guarantee, concurrency
[41] I.J. Hayes, S.E. Dunne, and L.A. Meinicke. Linking unifying theories of program refinement. Science of Computer Programming, 78(11):2086--2107, 2013. [bib| DOI| http]
In this paper we consider three theories of programs and specifications at different levels of abstraction. The theories we focus on are: the basic Unifying Theories of Programming (UTP) model, which corresponds to the theories of VDM, B, and the refinement calculus; an extended theory that distinguishes abort from nontermination; and a further extension that introduces (abstract) time. We define UTP-style designs (or specifications) in each theory and show how program constructors, such as nondeterministic choice and sequential composition, can be expressed as single designs in each theory. To examine the relationships between the theories, we construct mappings in both directions between pairs of theories and show that the pairs of mappings form Galois connections. This shows that the simpler (more abstract) models are sub-theories of the more complex extensions. The mappings preserve the program structure and hence are homomorphisms. An important property of a Galois connection is that both mappings preserve refinement. The Galois connections between the models can be exploited to translate properties, including refinement laws, between theories. In addition, we show how to define an iteration in the extended model in terms of an iteration in the timed model.
Keywords: Unifying theories of programming (UTP), Real-time refinement, Program termination
[42] Brijesh Dongol and IanJ. Hayes. Deriving real-time action systems in a sampling logic. Science of Computer Programming, 78(11):2047--2063, 2013. [bib| DOI| http]
Action systems have been shown to be applicable for modelling and constructing systems in both discrete and hybrid domains. We present a novel semantics for action systems using a sampling logic that facilitates reasoning about the truly concurrent behaviour between an action system and its environment. By reasoning over the apparent states, the sampling logic allows one to determine whether a state predicate is definitely or possibly true over an interval. We present a semantics for action systems that allows the time taken to sample inputs and evaluate expressions (and hence guards) into account. We develop a temporal logic based on the sampling logic that facilitates formalisation of safety, progress, timing and transient properties. Then, we incorporate this logic to the method of enforced properties, which facilitates stepwise refinement of action systems.
Keywords: Sampling logic
[43] I.J. Hayes, A.Burns, B.Dongol, and C.B. Jones. Comparing degrees of non-deterministic in expression evaluation. The Computer Journal, 56(6):741--755, 2013. [bib]
Expression evaluation in programming languages is normally assumed to be deterministic; however, if an expression involves variables that are being modified by the environment of the process during its evaluation, the result of the evaluation can be non-deterministic. Two common scenarios in which this occurs are concurrent programs within which processes share variables and real-time programs that interact to monitor and/or control their environment. In these contexts, although any particular evaluation of an expression gives a single result, there is a range of possible values that could be returned depending on the relative timing between modification of a variable by the environment and its access within the expression evaluation. To compare the semantics of non-deterministic expression evaluation, one can use the set of possible values the expression evaluation could return. This paper formalizes three approaches to non-deterministic expression evaluation, highlights their commonalities and differences, shows the relationships between the approaches and explores conditions under which they coincide. Modal operators representing that a predicate holds for all possible evaluations and for some possible evaluation are associated with each of the evaluation approaches, and the properties and relationships between these operators are investigated. Furthermore, a link is made to a new notation used in reasoning about interference.
Keywords: non-deterministic expression evaluation; sampling logic; rely-guarantee; concurrency; real-time programming
[44] DanielR. Bradley and IanJ. Hayes. Visuocode: A software development environment that supports spatial navigation and composition. In Alexandru Telea, Andreas Kerren, and Andrian Marcus, editors, First IEEE Working Conference on Software Visualization (VISSOFT), pages 1--4. IEEE, 2013. [bib| DOI| http]
Navigating through software is an integral part of software development. Studies have identified that during navigation programmers often become disoriented and lose task awareness. To mitigate this, the method-flow visualisation technique displays traversed methods in adjacent editor columns. This paper presents the Visuocode software development environment, which is an implementation of method-flow that, in addition to navigation, supports program composition.
Keywords: program visualisation
[45] Kirsten Winter, Chenyi Zhang, IanJ. Hayes, Nathan Keynes, Cristina Cifuentes, and Lian Li. Path-sensitive data flow analysis simplified. In Lindsay Groves and Jing Sun, editors, Formal Methods and Software Engineering: Proceedings 15th International Conference on Formal Engineering Methods (ICFEM), volume 8144 of LNCS, pages 415--430. Springer, 2013. [bib| DOI| http]
Path-sensitive data flow analysis pairs classical data flow analysis with an analysis of feasibility of paths to improve precision. In this paper we propose a framework for path-sensitive backward data flow analysis that is enhanced with an abstraction of the predicate domain. The abstraction is based on a three-valued logic. It follows the strategy that path predicates are simplified if possible (without calling an external predicate solver) and every predicate that could not be reduced to a simple predicate is abstracted to the unknown value, for which the feasibility is undecided. The implementation of the framework scales well and delivers promising results.
Keywords: static program analysis
[46] B.Dongol and I.J. Hayes. Approximating idealised real-time specifications using time bands. In A.Romanovsky, C.B. Jones, J.Bendiposto, and M.Leuschel, editors, Automated Verification of Critical Systems 2011, volume46 of Electronic Communications of the EASST, pages 1--16. EASST, 2012. [bib| DOI]
Timed specifications are often formalised at an absolute level of precision, which does not reflect the real world that the specifications model, i.e., in the real world, inputs cannot be sampled with absolute precision and physical hardware cannot react instantaneously. As a result the developed specifications can often become unimplementable. In this paper, we consider the time bands model which allows time to be structured into several layers of abstraction and relationships between bands to be formalised. This allows the timed specifications developed under idealised assumptions to be approximated using the time band in which the variables are sampled. We implement the approximated specifications using teleo-reactive programs embedded with time bands.
[47] Eban Escott, Paul Strooper, Paul King, and Ian Hayes. Model-driven web form validation with UML and OCL. In Andreas Harth and Nora Koch, editors, Current Trends in Web Engineering, volume 7059 of Lecture Notes in Computer Science, pages 223--235. Springer Berlin / Heidelberg, 2012. [bib| http]
Form validation is an integral part of a web application. Web developers must ensure that data input by the user is validated for correctness. Given the importance of form validation it must be considered as part of a model-driven solution to web development. Existing model-driven approaches typically have not addressed form validation as part of the model. In this paper, we present an approach that allows validation constraints to be captured within a model using UML and OCL. Our approach covers three common types of validation: single element, multiple element, and entity association. We provide an example to illustrate an architecture-centric approach.
[48] Brijesh Dongol and IanJ. Hayes. Rely/guarantee reasoning for teleo-reactive programs over multiple time bands. In John Derrick, Stefania Gnesi, Diego Latella, and Helen Treharne, editors, Integrated Formal Methods, volume 7321 of LNCS, pages 39--53. Springer, 2012. [bib| DOI| http]
A complex real-time system consists of components at multiple time abstractions with varying notions of granularity and precision. Existing hybrid frameworks only allow reasoning at a single granularity and at an absolute level of precision, which can be problematic because the models that are developed can become unimplementable. In this paper, we develop a framework that incorporates time bands so that the behaviour of each component may be specified at a time granularity that is appropriate for the component and its properties. We implement our controllers using teleo-reactive programs, which are high-level programs that are well-suited to controlling reactive systems in dynamic environments. We develop rely/guarantee-style reasoning rules and as an example, prove properties of a well-known mine-pump system.
Keywords: Teleo reactive
[49] IanJ. Hayes and RobertJ. Colvin. Integrated operational semantics: Small-step, big-step and multi-step. In John Derrick, John Fitzgerald, Stefania Gnesi, Sarfraz Khurshid, Michael Leuschel, Steve Reeves, and Elvinia Riccobene, editors, Abstract State Machines, Alloy, B, VDM, and Z - Third International Conference, ABZ 2012, Pisa, Italy, June 18-21, 2012. Proceedings, volume 7316 of LNCS, pages 21--35. Springer, 2012. [bib| DOI]
Plotkin's structural operational semantics provides a tried and tested method for defining the semantics of a programming language via sets of rules that define valid transitions between program configurations. Mosses' modular structural operational semantics (MSOS) recasts the approach by making use of rules consisting of labelled transitions, allowing a more modular approach to defining language semantics. MSOS can be adapted by using “syntactic” labels that allow local variables and aliasing to be defined without augmenting the semantics with environments and locations. The syntactic labels allow both state-based constructs of imperative languages and event-based constructs of process algebras to the specified in an integrated manner. To illustrate the integrated approach we compare its rules with Plotkin's original rules for both small-step and big-step operational semantics. One issue that arises is that defining concurrency requires the use of a small-step approach to handle interleaving, while defining a specification command requires a big-step approach. The integrated approach can be generalised to use a sequence of (small) steps as a label; we call this a multi-step operational semantics. This approach allows both concurrency and non-atomic specification commands to be defined.
[50] Brijesh Dongol and IanJ. Hayes. Deriving real-time action systems controllers from multiscale system specifications. In J.Gibbons and P.Nogueira, editors, Mathematics of Program Construction, volume 7342 of LNCS, pages 102--131. Springer, 2012. [bib| DOI| http]
This paper develops a method for deriving controllers for real-time systems in which the components of the system operate at different time granularities. To this end, we incorporate the theory of time bands into action systems, which allows one to structure a system into multiple abstractions of time. The framework includes a logic that facilitates reasoning about different types of sampling errors and transient properties (i.e., properties that only hold for a brief amount of time), and we develop theorems for simplifying proofs of hardware/software interaction. We formalise true concurrency and define refinement for the parallel composition of action systems. Our method of derivation builds on the verify-while-develop paradigm, where the action system code is developed side-by-side with its proof.
Keywords: Action systems
[51] Brijesh Dongol, IanJ. Hayes, Larissa Meinicke, and Kim Solin. Towards an algebra for real-time programs. In W.Kahl and T.G. Griffin, editors, 13th International Conference on Relational and Algebraic Methods in Computer Science (RAMiCS), volume 7560 of LNCS, pages 50--65. Springer, 2012. [bib| DOI| http]
We develop an algebra for an interval-based model that has been shown to be useful for reasoning about real-time programs. In that model, a system's behaviour over all time is given by a stream (mapping each time to a state) and the behaviour over an interval is determined using an interval predicate, which maps an interval and a stream to a Boolean. Intervals are allowed to be open/closed at either end and adjoining (i.e., immediately adjacent) intervals do not share any common points but are contiguous over their boundary. Values of variables at the ends of open intervals are determined using limits, which allows the possible piecewise continuity of a variable at the boundaries of an interval to be handled in a natural manner. What sort of an algebra does this model give rise to? In this paper, we take a step towards answering that question by investigating an algebra of interval predicates.
Keywords: Real-time, program algebra
[52] Brijesh Dongol, John Derrick, and IanJ. Hayes. Fractional permissions and non-deterministic evaluators in interval temporal logic. In Gerald Lüttgen and Stephan Merz, editors, Proc. 12th International Workshop on Automated Verification of Critical Systems (AVoCS 2012), volume53 of Electronic Communications of the EASST, pages 1--15, 2012. [bib| DOI]
We propose Interval Temporal Logic as a basis for reasoning about concurrent programs with fine-grained atomicity due to the generality it provides over reasoning with standard pre/post-state relations. To simplify the semantics of parallel composition over intervals, we use fractional permissions, which allows one to ensure that conflicting reads and writes to a variable do not occur simultaneously. Using non-deterministic evaluators over intervals, we enable reasoning about the apparent states over an interval, which may differ from the actual states in the interval. The combination of Interval Temporal Logic, non-deterministic evaluators and fractional permissions results in a generic framework for reasoning about concurrent programs with fine-grained atomicity. We use our logic to develop rely/guarantee-style rules for decomposing a proof of a large system into proofs of its subcomponents, where fractional permissions are used to ensure that the behaviours of a program and its environment do not conflict.
Keywords: Interval Temporal Logic, Fractional Permissions, Non-deterministic Expression Evaluation, Parallel Composition, Compositional Reasoning
[53] I.J. Hayes, A.Burns, B.Dongol, and C.B. Jones. Comparing models of nondeterministic expression evaluation. Technical Report CS-TR-1273, School of Computing Science, Newcastle University, September 2011. [bib]
Expression evaluation in programming languages is normally deterministic; however, if expressions involve variables that are being modified by the environment of the process during their evaluation, the result of the evaluation can be nondeterministic. Two common cases where this occurs are in concurrent programs where processes share variables and real-time programs that interact to monitor and/or control their environment. In these contexts, while any particular evaluation of an expression gives a single result, there is a range of possible results that could be returned depending on the relative timing of modification of variables by the environment and their access within expression evaluation. Hence to model the semantics of expression evaluation one can use the set of possible values the expression evaluation could return. This paper considers three views of interpreting expressions nondeterministically. The paper formalises the three approaches, highlights different properties satisfied by the approaches, relates the approaches and explores conditions under which they coincide. Furthermore, a link is made to a new notation used in reasoning about interference.
Keywords: sampling logic
[54] R.J. Colvin and I.J. Hayes. A semantics for Behavior Trees using CSP with specification commands. Science of Computer Programming, 76(10):891--914, 2011. [bib| DOI| http]
In this paper we give a formal definition of the requirements translation language Behavior Trees. This language has been used with success in industry to systematically translate large, complex, and often erroneous requirements documents into a structured model of the system. It contains a mixture of state-based manipulations, synchronisation, message passing, and parallel, conditional, and iterative control structures. The formal semantics of a Behavior Tree is given via a translation to a version of Hoare's process algebra CSP, extended with state-based constructs such as guards and updates, and a message passing facility similar to that used in publish/subscribe protocols. We first provide the extension of CSP and its operational semantics, which preserves the meaning of the original CSP operators, and then the Behavior Tree notation and its translation into the extended version of CSP.
Keywords: Structural operational semantics
[55] R.J. Colvin and I.J. Hayes. Structural operational semantics through context-dependent behaviour. Journal of Logic and Algebraic Programming, 80(7):392--426, 2011. [bib| DOI]
We present a new approach to providing a structural operational semantics for imperative programming languages with concurrency and procedures. The approach is novel because we expose the building block operations—--variable assignment and condition checking—--in the labels on the transitions; these form the context-dependent behaviour of a program. Using this style results in two main advantages over standard formalisms for imperative programming language semantics: firstly, our individual transition rules are more concise, and secondly, we are able to more abstractly and intuitively describe the semantics of procedures, including by-value and by-reference parameters. Standard techniques in the literature tend to result in complex and hard-to-read rules for even simple language constructs when procedures and parameters are dealt with. Our semantics for procedures utilises the context-dependent behaviour in the transition label to handle variable name scoping, and defines the semantics of recursion without requiring additional rules. In contrast with Plotkin’s seminal structural operational semantics paper, we do not use locations to describe some of the more complex language constructs. Novel aspects of the abstract syntax include local states (in contrast to a single global store), which simplifies the reasoning about local variables, and a command for dynamically renaming variables (in contrast to mapping variables to locations), which simplifies the reasoning about the effect of procedures on by-reference parameters.
[56] Alan Burns, Kun Wei, Jim Woodcock, IanJ. Hayes, and CliffB. Jones. Timebands framework -- 2011. Technical Report YCS-2011-467, Department of Computer Science, University of York, 2011. 36 pages. [bib]
Complex real-time systems must integrate physical processes with digital control, human operation and organisational structures. New scientific foundations are required for specifying, designing and implementing these systems. One key challenge is to cope with the wide range of time scales and dynamics inherent in such systems. To exploit the unique properties of time, with the aim of producing more dependable computer-based systems, a timeband framework has been developed. In this paper we review this framework and report on modifications, extensions and applications that have been undertaken in funded research that completed in 2011.
[57] Alan Burns and IanJ. Hayes. A timeband framework for modelling real-time systems. Real-Time Systems, 45(1--2):106--142, June 2010. [bib| DOI| http]
Complex real-time systems must integrate physical processes with digital control, human operation and organisational structures. New scientific foundations are required for specifying, designing and implementing these systems. One key challenge is to cope with the wide range of time scales and dynamics inherent in such systems. To exploit the unique properties of time, with the aim of producing more dependable computer-based systems, it is desirable to explicitly identify distinct time bands in which the system is situated. Such a framework enables the temporal properties and associated dynamic behaviour of existing systems to be described and the requirements for new or modified systems to be specified. A system model based on a finite set of distinct time bands is motivated and developed in this paper.
Keywords: Real-time systems, time bands
[58] SteveE. Dunne, IanJ. Hayes, and AndyJ. Galloway. Reasoning about loops in total and general correctness. In A.Butterfield, editor, Unifying Theories of Programming: Second International Symposium, UTP 2008, Dublin, Ireland, September 8-10, 2008, Revised Selected, volume 5713 of Lecture Notes in Computer Science, pages 62--81. Springer, 2010. [bib| DOI]
We introduce a calculus for reasoning about programs in total correctness which blends UTP designs with von Wright's notion of a demonic refinement algebra. We demonstrate its utility in verifying the familiar loop-invariant rule for refining a total-correctness specification by a while loop. Total correctness equates non-termination with completely chaotic behaviour, with the consequence that any situation which admits non-termination must also admit arbitrary terminating behaviour. General correctness is more discriminating in allowing non-termination to be specified together with more particular terminating behaviour. We therefore introduce an analogous calculus for reasoning about programs in general correctness which blends UTP prescriptions with a demonic refinement algebra. We formulate a loop-invariant rule for refining a general-correctness specification by a while loop, and we use our general-correctness calculus to verify the new rule.
[59] Brijesh Dongol and IanJ. Hayes. Compositional action system derivation using enforced properties. In C.Bolduc, J.Desharnais, and B.Ktari, editors, Mathematics of Program Construction (MPC), volume 6120 of LNCS, pages 119--139. Springer Verlag, 2010. [bib]
Action systems have been shown to be applicable for modelling and constructing both sequential and concurrent systems. This paper presents an approach to program construction where the concrete implementation is derived from its specification---via a series of small refinements---using incomplete proofs to motivate changes to the program. Formalisation of our approach is provided by enforced properties, which restrict the traces of a program to those that satisfy the enforced properties. The goal of the derivation is to refine a program with enforced properties to a program (with no enforced properties) whose code satisfies the enforced properties. An advantage of this approach is that the code in the earlier versions of the program need not be complete; incorrect execution of the program is avoided by including enforced properties in the specification. Enforced properties may be any temporal formula or relation, and hence we may reason about both safety and progress in a compositional setting.
Keywords: Action systems
[60] I.J. Hayes, S.E. Dunne, and L.A. Meinicke. Unifying theories of programming that distinguish nontermination and abort. In C.Bolduc, J.Desharnais, and B.Ktari, editors, Mathematics of Program Construction, volume 6120 of LNCS, pages 178--194. Springer, 2010. [bib]
In this paper we focus on the relationship between a number of specification models. The models are formulated in the Unifying Theories of Programming of Hoare and He, but correspond to widely used specification models. We cover issues such as partial correctness, total correctness, and general correctness. The properties we use to distinguish the models are these: whether they allow the specification of assumptions about the initial state outside of which no guarantees are given about the behaviour of the program, i.e., the program may "abort"; whether a specification may allow or even require nontermination as a valid (non-aborting) outcome; and whether they allow the expression of tests or enabling conditions, outside of which the program has no possible behaviour. When considering termination, we consider both an abstract model, which only distinguishes whether a program terminates or not, as well as models that include a notion of time: either abstract time representing a notion of progress or real-time.
Keywords: Unifying theories of programming
[61] I.J. Hayes. Invariants and well-foundedness in program algebra. In A.Cavalcanti, D.Déharbe, M.-C. Gaudel, and J.Woodcock, editors, International Colloquium on Theoretical Aspects of Computing (ICTAC), volume 6255 of LNCS, pages 1--14. Springer, 2010. [bib| DOI]
Program algebras abstract the essential properties of programming languages in the form of algebraic laws. The proof of a refinement law may be expressed in terms of the algebraic properties of programs required for the law to hold, rather than directly in terms of the semantics of a language. This has the advantage that the law is then valid for any programming language that satisfies the required algebraic properties. By characterised the important properties of programming languages algebraically we can devise simple proofs of common refinement laws. In this paper we consider standard refinement laws for sequential programs. We give simple characterisations of program invariants and well foundedness of statements.
Keywords: Program algebra
[62] K.Winter, I.J. Hayes, and R.J. Colvin. Integrating requirements: The Behavior Tree philosophy. In J.L. Fiadeiro and S.Gnesi, editors, Proc. of Int. Conf. on Software Engineering and Formal Methods (SEFM 2010), pages 41--50. IEEE Computer Society Press, 2010. [bib| DOI]
Behavior Trees were invented by Geoff Dromey as a graphical modelling notation. Their design was driven by the desire to ease the task of capturing functional system requirements and to bridge the gap between an informal language description and a formal model. Vital to Dromey’s intention is the idea of incrementally building the model out of its building blocks, the functional requirements. This is done by graphically representing each requirement as its own Behavior Tree and incrementally merging the trees to form a more complete model of the system. In this paper we investigate the essence of this constructive approach to creating a model in general notation-independent terms and discuss its advantages and disadvantages. The result can be seen as a framework of rules and provides us with a semantic underpinning of requirements integration. Integration points are identified by examining the (implicit or explicit) preconditions of each requirement. We use Behavior Trees as an example of how this framework can be put into practise.
Keywords: Requirements, modelling, analysis, integration, Behavior Tree
[63] IanJ. Hayes. Dynamically detecting faults via integrity constraints. In Michael Butler, Cliff Jones, Alexander Romanovsky, and Elena Troubitsyna, editors, Methods, Models, and Tools for Fault Tolerance, volume 5454 of Lecture Notes in Computer Science, pages 85--103. Springer Verlag, 2009. [bib]
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 integrity constraints, which are invariants on the state of a system's variables, including its inputs and outputs. Under normal operation integrity constraints 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.
[64] R.J. Colvin and I.J. Hayes. CSP with hierarchical state. In M.Leuschel and H.Wehrheim, editors, Integrated Formal Methods (IFM 2009), volume 5423 of LNCS, pages 118--135. Springer, 2009. [bib]
The process algebra CSP is designed for specifying interactions between concurrent systems. In CSP, and related languages, concurrent processes synchronise on common events, while the internal operations of the individual processes are treated abstractly. In some contexts, however, such as when modelling systems of systems, it is desirable to model both interprocess communications as well as the internal operations of individual processes. At the implementation level, shared state is often the method of communication between processes, and tests and updates of local state are used to implement internal operations. In this paper we propose an extension of the CSP language which maintains CSP's core elegance in specifying process synchronisation, while also allowing state-based behaviour. State is treated hierarchically, allowing (nested) declarations of local and shared variables. The state can be accessed and modified using a refinement calculus-style specification command, which may be optionally paired with event synchronisation. The semantics of the extended language, preserves the original CSP rules. The approach we present is novel in that state is part of the process, rather than a meta-level construct appearing only in the rules.
[65] Brijesh Dongol and IanJ. Hayes. Enforcing safety and progress properties: An approach to concurrent program derivation. In Colin Fidge, editor, Australian Software Engineering Conference, pages 3--12. IEEE Computer Society, 2009. [bib]
In this paper we develop an approach for deriving concurrent programs. At any stage in its derivation, a program consists of a combination of the code for its processes together with a set of enforced properties. The behaviour of such a combination consists of those behaviours of the code that satisfy the enforced properties. Because enforced properties are temporal formulae, they may be used to enforce both safety and progress properties of the program. While the code by itself is executable, when combined with enforced properties, the program is not yet in an executable form. A derivation starts from a program in which the desired properties of the code are expressed via enforced properties, and the goal is to derive a program with additional code but no enforced properties. We outline a trace-based theory which formalises the meaning of programs with enforced properties, and transformation rules that ensure each modified program is a refinement of the original.
[66] R.Colvin, I.J. Hayes, and P.A. Strooper. Calculating modules in contextual logic program refinement. Theory and Practice of Logic Programming, 8(01):1--31, 2008. [bib| DOI| arXiv| http]
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 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 module refinement. A module is a collection of procedures that operate 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 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
[67] Larissa Meinicke and IanJ. Hayes. Algebraic reasoning for probabilistic action systems and while-loops. Acta Informatica, 45(5):321--382, 2008. [bib| DOI]
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
[68] Larissa Meinicke and IanJ. Hayes. Probabilistic choice in refinement algebra. In Philippe Audebaud and Christine Paulin-Mohring, editors, Mathematics of Program Construction (MPC), volume 5133 of Lecture Notes in Computer Science, pages 243--267. Springer Verlag, 2008. [bib| DOI]
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.
Keywords: Kleene algebra, probability, refinement algebra, total-correctness
[69] IanJ. Hayes. Towards reasoning about teleo-reactive programs for robust real-time systems. In Nicolas Guelfi, Henry Muccini, Patrizio Pelliccione, and Alexander Romanovsky, editors, Proceedings of the 2008 RISE/EFTS Joint International Workshop on Software Engineering for Resilient Systems, pages 87--94, New York, NY, USA, 2008. ACM. [bib| DOI]
The teleo-reactive programming approach was developed by Nilsson for application in domains like robotics. It has a high-level programming model that allows real-time control programs to be written in a manner that allows them to react robustly to changes in the environment. In this paper we give a formalisation of the semantics of teleo-reactive programs and provide rely/guarantee rules for reasoning about them. The semantics are given in a form that partitions the behaviour of the system into its behaviour over a sequence of time intervals.
[70] R.Colvin and I.J. Hayes. A semantics for behavior trees. ACCS Technical Report ACCS-TR-07-01, ARC Centre for Complex Systems (ACCS), April 2007. [bib| http]
[71] I.J. Hayes. Procedures and parameters in the real-time program refinement calculus. Science of Computer Programming, 64(3):286--311, February 2007. [bib| DOI]
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
[72] C.B. Jones, I.J. Hayes, and M.A. Jackson. Deriving specifications for systems that are connected to the physical world. In C.B. Jones, Z.Liu, and J.Woodcock, editors, Formal Methods and Hybrid Real-Time Systems, volume 4700 of Lecture Notes in Computer Science, pages 364--390. Springer Verlag, 2007. [bib| DOI]
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 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.
[73] Brijesh Dongol and IanJ. Hayes. Trace semantics for the Owicki-Gries theory integrated with the progress logic from unity. Technical Report SSE-2007-02, Division of Systems and Software Engineering Research, School of Information Technology and Electrical Engineering, The University of Queensland, 2007. [bib]
[74] I.J. Hayes. Termination of real-time programs: definitely, definitely not or maybe. In S.E. Dunne and W.J. Stoddart, editors, UTP 2006: First Int. Symp. on Unifying Theories of Programming, volume 4010 of LNCS, pages 141--154. Springer, 2006. [bib]
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.

[75] Larissa Meinicke and IanJ. Hayes. Continuous action system refinement. In T.Uustalu, editor, Mathematics of Program Construction: Proceedings 8th International Conference (MPC 2006), volume 4014 of LNCS, pages 316--337. Springer Verlag, 2006. [bib| DOI| http]
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.
[76] L.Meinicke and I.J. Hayes. Reasoning algebraically about probabilistic loops. In Zhiming Liu and Jifeng He, editors, ICFEM, volume 4260 of LNCS, pages 380--399. Springer Verlag, 2006. [bib| DOI| http]
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.
[77] I.J. Hayes, C.B. Jones, and J.E. Nicholls. Understanding the differences between VDM and Z. FACS FACTS, 2006-2:56--78, 2006. [bib]
[78] K.Lermer, C.J. Fidge, and I.J. Hayes. A theory for execution-time derivation in real-time programs. Theoretical Computer Science, 346(1):3--27, November 2005. [bib]
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
[79] J.Fitzgerald, I.J. Hayes, and A.Tarlecki, editors. FM 2005: Formal Methods -- Proceedings 13th International Symposium of Formal Methods Europe, Newcastle, UK, July 2005, volume 3582 of Lecture Notes in Computer Science. Springer Verlag, July 2005. [bib]
[80] Phil Cook, Jim Welsh, and IanJ. Hayes. Incremental semantic evaluation for interactive systems: Inertia, pre-emption, and relations. Technical Report SSE-2005-01, Division of Systems and Software Engineering Research, School of Information Technology and Electrical Engineering, The University of Queensland, 2005. [bib]
[81] Phil Cook, Jim Welsh, and IanJ. Hayes. Building a flexible incremental compiler back-end. Technical Report SSE-2005-02, Division of Systems and Software Engineering Research, School of Information Technology and Electrical Engineering, The University of Queensland, 2005. [bib]
[82] Erica Glynn, I.J. Hayes, and Anthony MacDonald. Integration of generic program analysis tools into a software development environment. In V.Estivill-Castro, editor, Computer Science 2005: Proceedings 28th Australasian Computer Science Conference (ACSC2005), volume38 of Conferences in Research and Practice in Information Technology, pages 249--257. Australian Computer Society, 2005. [bib]
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.

[83] A.Burns, I.J. Hayes, G.Baxter, and C.J. Fidge. Modelling temporal behaviour in complex socio-technical systems. Technical Report YCS390, University of York, 2005. [bib| .html| .pdf]
[84] I.J. Hayes. Towards platform-independent real-time systems. In P.A. Strooper, editor, ASWEC, pages 192--200. IEEE Computer Society, 2004. [bib]
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.

[85] R.Colvin, L.Groves, I.J. Hayes, D.Hemer, R.Nickson, and P.A. Strooper. Developing logic programs from specifications using stepwise refinement. In Maurice Bruynooghe and Kung-Kiu Lau, editors, Program Development in Computational Logic: A Decade of Research Advances in Logic-Based Program Development, volume 3049 of Lecture Notes in Computer Science, pages 66--89. Springer Verlag, 2004. [bib]
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.
[86] C.Smith, K.Winter, I.J. Hayes, R.G. Dromey, P.A. Lindsay, and D.A. Carrington. An environment for building a system out of its requirements. In Proc. 19th IEEE Int. Conf. on Automated Software Engineering, pages 398--399. IEEE, 2004. [bib]
[87] K.Lermer, C.J. Fidge, and I.J. Hayes. Linear approximation of execution-time constraints. Formal Aspects of Computing, 15(4):319--348, December 2003. [bib]
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.
[88] K.Lermer, C.J. Fidge, and I.J. Hayes. Formal semantics for program paths. In J.Harland, editor, Computing: The Australian Theory Symposium (CATS) 2003, volume78 of Electronic Notes in Theoretical Computer Science (ENTCS), pages 1--24. Elsevier, February 2003. [bib| .html]
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.
[89] I.J. Hayes. A predicative semantics for real-time refinement. In A.McIver and C.C. Morgan, editors, Programming Methodology, pages 109--133. Springer, 2003. [bib]
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.
[90] Sibylle Peuker and Ian Hayes. Reasoning about deadlines in concurrent real-time programs. In Michel Charpentier and Beverly Sanders, editors, Workshop on Formal Methods for Parallel Programming (FMPP 2003) in Proc. 17th International Parallel and Distributed Processing Symposium, pages 1--8. IEEE CS Press, 2003. [bib| http]
We propose a method for the timing analysis of concurrent real-time programs with hard deadlines. We divide the analysis 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-independent phase.

[91] R.Colvin, I.J. Hayes, D.Hemer, and P.A. Strooper. Refinement of higher-order logic programs. In M.Leuschel, editor, Proceedings of the International Workshop on Logic-based Program Synthesis and Transformation (LOPSTR 2002), volume 2664 of Lecture Notes in Computer Science, pages 126--143. Springer, 2003. [bib]
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.
[92] I.J. Hayes, M.A. Jackson, and C.B. Jones. Determining the specification of a control system from that of its environment. In K.Araki, S.Gnesi, and D.Mandrioli, editors, FME 2003: Formal Methods, volume 2805 of LNCS, pages 154--169. Springer Verlag, 2003. [bib| .pdf]
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.

[93] I.J. Hayes. Programs as paths: An approach to timing constraint analysis. In JinSong Dong and Jim Woodcock, editors, ICFEM, volume 2885 of LNCS, pages 1--15. Springer Verlag, 2003. [bib]
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.

[94] IanJ. Hayes. Block-structured (attribute) grammars. Technical Report 02-47, Software Verification Research Centre, The University of Queensland, December 2002. [bib]
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.
[95] I.J. Hayes, R.Colvin, D.Hemer, P.A. Strooper, and R.Nickson. A refinement calculus for logic programs. Theory and Practice of Logic Programming, 2(4--5):425--460, July 2002. [bib]
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 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.
[96] G.Smith and I.J. Hayes. An introduction to Real-Time Object-Z. Formal Aspects of Computing, 13(2):128--141, May 2002. [bib]
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
[97] I.J. Hayes. Reasoning about real-time repetitions: Terminating and nonterminating. Science of Computer Programming, 43(2--3):161--192, 2002. [bib| http| .pdf]
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.

Keywords: Real-time refinement; nonterminating repetitions.
[98] D.Hemer, R.Colvin, I.Hayes, and P.Strooper. Don't care non-determinism in logic program refinement. In J.Harland, editor, Proceedings of Computing: the Australasian Theory Symposium (CATS 2002), volume61 of Electronic Notes in Theoretical Computer Science (ENTCS), pages 1--21. Elsevier Science, 2002. [bib]
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 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 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.

[99] R.Colvin, I.J. Hayes, D.Hemer, and P.A. Strooper. Translating refined logic programs to Mercury. In M.Oudshoorn, editor, Proceedings 25th Australasian Computer Science Conference (ACSC 2002), volume4 of Conferences in Research and Practice in Information Technology, pages 33--40. Australian Computer Society, 2002. [bib]
[100] I.J. Hayes. Reasoning about timeouts. In EerkeA. Boiten and Bernhard Möller, editors, Proc. Mathematics of Program Construction, volume 2386 of Lecture Notes in Computer Science, pages 94--116. Springer, 2002. [bib| DOI]
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.

[101] I.J. Hayes. The real-time refinement calculus: A foundation for machine-independent real-time programming. In J.Esparza and C.Lakos, editors, Proceedings 23rd International Conference on the Application and Theory of Petri Nets, volume 2360 of Lecture Notes in Computer Science, pages 44--58. Springer, 2002. Invited keynote paper. [bib]
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.

[102] S.Peuker and I.J. Hayes. Towards a refinement calculus for concurrent real-time programs. In C.George and Huaikou Miao, editors, Formal Methods and Software Engineering (ICFEM), volume 2495 of LNCS, pages 335--347. Springer-Verlag, 2002. [bib]
We define a language and a predicative semantics to model concurrent real-time programs. We consider different communication paradigms 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-independent concurrent real-time programs from specifications. We give some examples of refinement laws that deal with concurrency.

[103] Jamie Shield and IanJ. Hayes. Refining object-oriented invariants and dynamic constraints. In P.A. Strooper and P.Muenchaisri, editors, Asian-Pacific Software Engineering Conference (APSEC), pages 52--61. IEEE Computer Society, 2002. [bib| DOI| http]
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
[104] R.Colvin, I.J. Hayes, D.Hemer, and P.Strooper. Extended abstract: Refinement of higher-order logic programs. In M.Leuschel and F.Bueno, editors, Pre-Proceedings of the International Workshop on Logic-based Program Synthesis and Transformation (LOPSTR 2002), pages 136--141. School of Computer Science, Technical University of Madrid, 2002. Extended abstract. [bib]
[105] Phil Cook, Jim Welsh, and IanJ. Hayes. Incremental context-sensitive evaluation in context. Technical Report 02-11, Software Verification Research Centre, The University of Queensland, 2002. [bib]
[106] I.J. Hayes, C.J. Fidge, and K.Lermer. Semantic characterisation of dead control-flow paths. IEE Proceedings---Software, 148(6):175--186, December 2001. Awarded the 2001/2002 Mather Premium by the Institution of Electrical Engineers. [bib| .pdf]
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.
[107] J.Shield, I.J. Hayes, and D.A. Carrington. Using theory interpretation to mechanise the reals in a theorem prover. In C.J. Fidge, editor, Computing: The Australian Theory Symposium (CATS), volume42 of Electronic Notes in Theoretical Computer Science, pages 266--281. Elsevier Science, 2001. URL: www.elsevier.nl/locate/entcs. [bib]
[108] I.J. Hayes and M.Utting. A sequential real-time refinement calculus. Acta Informatica, 37(6):385--448, 2001. [bib| .pdf]
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.
[109] R.Colvin, I.J. Hayes, and P.Strooper. A technique for modular logic program refinement. In Kung-Kiu Lau, editor, Logic-based Program Synthesis and Transformation (LOPSTR 2000) Selected Papers, volume 2402 of Lecture Notes in Computer Science, pages 38--56. Springer, 2001. [bib| DOI]
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.
[110] D.Hemer, I.Hayes, and P.Strooper. Refinement calculus for logic programming in Isabelle/HOL. In R.Boulton and P.Jackson, editors, Theorem Proving in Higher Order Logics, 14th International Conference, TPHOLs 2001, volume 2152 of Lecture Notes in Computer Science, pages 249--264. Springer, 2001. [bib]
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
[111] I.J. Hayes, R.Nickson, P.Strooper, and R.Colvin. A declarative semantics for logic program refinement. Technical Report 00-30, Software Verification Research Centre, The University of Queensland, Brisbane 4072, Australia, November 2000. [bib]
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 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.
Keywords: Logic programming, refinement.
[112] R.Colvin, I.J. Hayes, and P.Strooper. Refining logic programs using types. In Jenny Edwards, editor, Australasian Computer Science Conference (ACSC2000), pages 43--50. IEEE Computer Society, 2000. [bib| DOI]
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.
[113] I.J. Hayes. Reasoning about non-terminating loops using deadline commands. In R.Backhouse and J.N. Oliveira, editors, Proc. Mathematics of Program Construction, volume 1837 of Lecture Notes in Computer Science, pages 60--79. Springer, 2000. This paper is superseded by [97]. [bib]
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.

[114] R.Colvin, I.J. Hayes, and P.Strooper. Modular logic program refinement. In Kung-Kiu Lau, editor, Pre-Proceedings of the Tenth International Workshop on Logic-based Program Synthesis and Transformation (LOPSTR 2000), number UMCS-00-6-1 in Technical Report, pages 1--10. Department of Computer Science, Manchester University, 2000. Extended abstract. [bib]
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.
[115] I.J. Hayes. Real-time program refinement using auxiliary variables. In M.Joseph, editor, Proc. Formal Techniques in Real-Time and Fault-Tolerant Systems, volume 1926 of LNCS, pages 170--184. Springer, 2000. [bib]
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.

[116] G.Smith and I.J. Hayes. Structuring real-time Object-Z specifications. In W.Grieskamp, T.Santen, and W.J. Stoddart, editors, IFM'00: Proceedings of the 2nd International Conference on Integrated Formal Methods, volume 1945 of Lecture Notes in Computer Science, pages 97--115. Springer, 2000. [bib]
[117] I.J. Hayes. Reasoning about real-time programs using idle-invariant assertions. In J.S. Dong, J.He, and M.Purvis, editors, Proceedings 7th Asia-Pacific Software Engineering Conference (APSEC 2000), pages 16--23. IEEE Computer Society, 2000. [bib]
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.
[118] C.J. Fidge, I.J. Hayes, and G.Watson. The deadline command. IEE Proceedings---Software, 146(2):104--111, April 1999. [bib| .ps]
[119] I.J. Hayes and C.B. Jones. Specifications are not (necessarily) executable. In J.P. Bowen and M.G. Hinchey, editors, High-Integrity System Specification and Design, pages 563--581. Springer, 1999. (Previously published in IEE/BCS Software Engineering Journal, Vol. 4, No. 6, 330--338, November, 1989). [bib]
[120] G.Smith and I.J. Hayes. Towards real-time Object-Z. In Keijiro Araki, Andy Galloway, and Kenji Taguchi, editors, IFM'99: Proceedings of the 1st International Conference on Integrated Formal Methods, pages 49--65. Springer, 1999. [bib]
[121] C.J. Fidge, I.J. Hayes, B.P. Mahony, and A.K. Wabenhorst. Real-time specification and reasoning using maximal intervals. In W.C.H. Cheng and A.S.M. Sajeev, editors, PART'99: Proceedings of the 6th Australasian Conference on Parallel and Real-Time Systems, pages 344--354. Springer, 1999. [bib]
[122] S.Grundon, I.J. Hayes, and C.J. Fidge. Timing constraint analysis. In C.McDonald, editor, Computer Science '98: Proc. 21st Australasian Computer Sci. Conf. (ACSC'98), pages 575--586. Springer, 1998. [bib]
[123] I.J. Hayes and M.Utting. Deadlines are termination. In D.Gries and W.-P. deRoever, editors, IFIP TC2/WG2.2, 2.3 International Conference on Programming Concepts and Methods (PROCOMET'98), pages 186--204. Chapman and Hall, 1998. [bib| .pdf]
[124] C.J. Fidge, I.J. Hayes, A.P. Martin, and A.K. Wabenhorst. A set-theoretic model for real-time specification and reasoning. In J.Jeuring, editor, Mathematics of Program Construction (MPC'98), volume 1422 of Lecture Notes in Computer Science, pages 188--206. Springer, 1998. [bib]
[125] I.J. Hayes. Expressive power of specification languages. Formal Aspects of Computing, 10(2):187--192, 1998. [bib]
[126] D.Carrington, I.Hayes, R.Nickson, G.Watson, and J.Welsh. A program refinement tool. Formal Aspects of Computing, 10(2):97--124, 1998. [bib| .ps]
[127] R.Colvin, I.J. Hayes, and P.Strooper. Data refining logic programs. In J.Grundy, M.Schwenke, and T.Vickers, editors, International Refinement Workshop and Formal Methods Pacific 1998, Discrete Mathematics and Theoretical Computer Science, pages 100--116. Springer, 1998. [bib]
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.
[128] L.P. Wildman and I.J. Hayes. Supporting contexts in the sequential real-time refinement calculus. In J.Grundy, M.Schwenke, and T.Vickers, editors, International Refinement Workshop and Formal Methods Pacific 1998, pages 352--369. Springer, 1998. [bib]
[129] I.J. Hayes. Separating timing and calculation in real-time refinement. In J.Grundy, M.Schwenke, and T.Vickers, editors, Int. Refinement Workshop and Formal Methods Pacific 1998, pages 1--16. Springer, 1998. [bib| .pdf]
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.
[130] C.J. Fidge, I.J. Hayes, and B.P. Mahony. Defining differentiation and integration in Z. In J.Staples, M.G. Hinchey, and Shaoying Liu, editors, Proceedings Second International Conference on Formal Engineering Methods (ICFEM'98), pages 64--73. IEEE Computer Society, 1998. [bib]
[131] I.Hayes, R.Nickson, and P.Strooper. Refining specifications to logic programs. In J.Gallagher, editor, Logic Program Synthesis and Transformation. Proc. of the 6th Int. Workshop, LOPSTR'96, Stockholm, Sweden, August 1996, volume 1207 of Lecture Notes in Computer Science, pages 1--19. Springer, 1997. [bib]
[132] I.J. Hayes and M.Utting. Coercing real-time refinement: A transmitter. In D.J. Duke and A.S. Evans, editors, BCS-FACS Northern Formal Methods Workshop (NFMW'96), Electronic Workshops in Computing. Springer, 1997. [bib| .pdf]
[133] R.Nickson and I.J. Hayes. Supporting contexts in program refinement. Science of Computer Programming, 29(3):279--302, 1997. [bib]
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 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 program window inference, to handle such contextual information during derivations in the refinement calculus. The idea is borrowed from a technique, called window inference, for handling context in theorem proving. Window inference is the primary proof paradigm of the Ergo proof editor. This tool has been extended to mechanize refinement using program window inference.
[134] P.G. Bancroft and I.J. Hayes. Type extension and refinement. In L.Groves and S.Reeves, editors, Formal Methods Pacific (FMP'97), pages 23--39. Springer, 1997. [bib]
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.
[135] R.Colvin, I.J. Hayes, R.Nickson, and P.A. Strooper. A tool for logic program refinement. In D.J. Duke and A.S. Evans, editors, Second BCS-FACS Northern Formal Methods Workshop (NFMW'97), Electronic Workshops in Computing. Springer, 1997. [bib]
[136] C.J. Fidge, M.Utting, I.J. Hayes, and P.Kearney. The Quartz refinement method for real-time multi-tasking systems. In Fifth Australasian Refinement Workshop (ARW'96), April 1996. [bib]
[137] I.J. Hayes and P.A. Strooper. Refining specifications to logic programs. In I.J. Hayes, editor, Proc. 5th Australasian Refinement Workshop, pages 1--13. Software Verification Research Centre, The University of Queensland, April 1996. Unrefereed. [bib| .html]
[138] I.J. Hayes, editor. Proc. 5th Australasian Refinement Workshop. Software Verification Research Centre, The University of Queensland, April 1996. Unrefereed. [bib| http]
[139] D.A. Carrington, I.J. Hayes, R.Nickson, G.Watson, and J.Welsh. Structured presentation of refinements and proofs. In Kotagiri Ramamohanarao, editor, Proc. 19th Australasian Computer Science Conference (ACSC'96), volume 18(1) of Australian Computer Science Communications, pages 87--96, February 1996. [bib]
[140] C.J. Fidge, M.Utting, P.Kearney, and I.J. Hayes. Integrating real-time scheduling theory and program refinement. In M.-C. Gaudel and J.Woodcock, editors, FME'96: Industrial Benefit and Advances in Formal Methods, volume 1051 of Lecture Notes in Computer Science, pages 327--346. Springer, 1996. [bib]
[141] D.A. Carrington, I.J. Hayes, R.Nickson, G.Watson, and J.Welsh. A tool for developing correct programs by refinement. In He Jifeng, editor, Proc. BCS 7th Refinement Workshop, Bath, UK, Electronic Workshops in Computing, pages 1--17. Springer, 1996. [bib]
[142] I.J. Hayes. Supporting module reuse in refinement. Science of Computer Programming, 27(2):175--184, 1996. [bib]
[143] I.J. Hayes. Specification models. In Proc. 7th International Conference on Putting into Practice Methods and Tools for Information Systems Design, 10--12 October, 1995, Nantes, pages 1--10, October 1995. Invited keynote paper. [bib]
[144] Ray Nickson and Ian Hayes. Program window inference. In Proc. of the 4th Australasian Refinement Workshop (ARW'95), pages 43--65. School of Computer Science and Engineering, University of New South Wales, April 1995. Unrefereed. Also available as Technical Report UQ-SVRC-95-29, Software Verification Research Centre, University of Queensland. [bib]
[145] David Carrington, Ian Hayes, Ray Nickson, Geoffrey Watson, and Jim Welsh. Requirements for a program refinement engine. In Proc. of the 4th Australasian Refinement Workshop (ARW'95), pages 67--83. School of Computer Science and Engineering, University of New South Wales, April 1995. [bib]
[146] L.P. Wildman and I.J. Hayes. Composing grammar transformations to construct a specification of a parser. In Ramamohanarao Kotagiri, editor, Proc. 18th Australasian Computer Science Conference (ACSC'95), Glenelg, South Australia, Australian Computer Science Communications, volume 17(1), pages 556--562, February 1995. [bib| .pdf]
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.
[147] Report ofthe Computer Science Action LearningGroup. Improving the quality of tutorial classes in computer science. Technical Report UQ-CS-322, Department of Computer Science, University of Queensland, 1995. [bib]
[148] I.J. Hayes and B.P. Mahony. Using units of measurement in formal specifications. Formal Aspects of Computing, 7(3):329--347, 1995. [bib| .pdf]
[149] P.Bancroft and I.J. Hayes. A formal semantics for a language with type extension. In ZUM'95: The Z Formal Specification Notation, Proc. 9th International Conference of Z Users, Limerick, Ireland, September 7--9, 1995, volume 967 of Lecture Notes in Computer Science, pages 299--314. Springer, 1995. [bib]
[150] I.J. Hayes and J.W. Sanders. Specification by interface separation. Formal Aspects of Computing, 7(4):430--439, 1995. [bib| .pdf]
[151] P.Bakker, D.A. Carrington, A.Goodchild, I.J. Hayes, H.Purchase, and P.A. Strooper. The communicating technologist: An educational challenge. In D.Budny and B.Herrick, editors, Frontiers in Education 25th Annual Conference, pages 4a4.1--4a4.4, Atlanta, Georgia, 1995. IEEE Press. [bib]
[152] I.J. Hayes, C.B. Jones, and J.E. Nicholls. Understanding the differences between VDM and Z. ACM Software Engineering News, 19(3):75--81, July 1994. Unrefereed. Previously published in FACS Europe [166]. [bib]
[153] B.P. Mahony, C.Millerchip, and I.J. Hayes. A boiler control system: Overview of a case study in timed refinement. In Diana DelBel Belluz and HerbertC. Ratz, editors, Software Safety: Everybody's Business, Proceedings of the 1993 International Invitational Workshop on Design and Review of Software-Controlled Safety-Related Systems, Ottawa, pages 189--208. The Institute of Risk Research, 1994. [bib]
[154] I.J. Hayes, C.B. Jones, and J.E. Nicholls. Understanding the differences between VDM and Z. Technical report UMCS-93-8-1, Department of Computer Science, University of Manchester, August 1993. [bib| .ps]
[155] B.P. Mahony, C.Millerchip, and I.J. Hayes. A boiler control system: A case study in timed refinement. In Diana DelBel Belluz, editor, Technical proceedings International Symposium on Design and Review of Software-Controlled Safety-Related Systems, Ottawa, June 1993. 50 pages. [bib| .ps]
[156] P.Bancroft and I.J. Hayes. Refining a module with opaque types. In Gopal Gupta, George Mohay, and Rodney Topor, editors, Proceedings, 16th Australian Computer Science Conference, Brisbane, Australian Computer Science Communications, volume 15(1), pages 615--624, February 1993. [bib]
[157] I.J. Hayes and L.P. Wildman. Towards libraries for Z. In J.P. Bowen and J.E. Nicholls, editors, Z User Workshop: Proceedings of the Seventh Annual Z User Meeting, London, December 1992, Workshops in Computing, pages 37--51. Springer, 1993. [bib| .pdf]
[158] I.J. Hayes. CICS message system. In I.J. Hayes, editor, Specification Case Studies, pages 238--243. Prentice Hall International, second edition, 1993. [bib]
[159] I.J. Hayes. CICS temporary storage. In I.J. Hayes, editor, Specification Case Studies, pages 226--237. Prentice Hall International, second edition, 1993. [bib]
[160] I.J. Hayes. Applying formal specification to software development in industry. In I.J. Hayes, editor, Specification Case Studies, pages 181--201. Prentice Hall International, second edition, 1993. (Previously published in IEEE Transactions on Software Engineering [193]). [bib]
[161] I.J. Hayes. Flexitime specification. In I.J. Hayes, editor, Specification Case Studies, pages 134--138. Prentice Hall International, second edition, 1993. [bib]
[162] I.J. Hayes. Block-structured symbol table. In I.J. Hayes, editor, Specification Case Studies, pages 14--30. Prentice Hall International, second edition, 1993. [bib]
[163] I.J. Hayes. Examples of specification using mathematics. In I.J. Hayes, editor, Specification Case Studies, pages 2--13. Prentice Hall International, second edition, 1993. [bib]
[164] I.J. Hayes, editor. Specification Case Studies. Prentice Hall, second edition, 1993. [bib| .pdf]
[165] D.A. Carrington, D.Duke, I.J. Hayes, and J.Welsh. Deriving modular designs from formal specifications. In Int. Symp. on the Foundations of Software Engineering (SIGSOFT'93), pages 89--98. ACM, 1993. [bib| .pdf]
[166] I.J. Hayes, C.B. Jones, and J.E. Nicholls. Understanding the differences between VDM and Z. FACS Europe, 1(1):7--30, 1993. Unrefereed. Also published in ACM Software Engineering News, 19(3):75--81, July 1994. [bib]
[167] I.J. Hayes. Multi-relations in Z: A cross between multi-sets and binary relations. Acta Informatica, 29(1):33--62, February 1992. [bib| .pdf]
[168] C.A.R. Hoare, I.J. Hayes, He Jifeng, C.Morgan, A.W. Roscoe, J.W. Sanders, I.H. Sørensen, J.M. Spivey, and B.A. Sufrin. Laws of programming. In Manfred Broy, editor, Programming and Mathematical Method, volume88 of NATO ASI Series F: Computer and Systems Sciences, pages 95--122. Springer, 1992. [bib]
[169] I.J. Hayes. VDM and Z: A comparative case study. Formal Aspects of Computing, 4(1):76--99, 1992. [bib| .pdf]
[170] B.P. Mahony and I.J. Hayes. A case-study in timed refinement: A mine pump. IEEE Trans. on Software Engineering, 18(9):817--826, 1992. [bib| .pdf]
[171] N.Ward and I.J. Hayes. Applications of angelic nondeterminism. In P.A. Bailes, editor, Proc. 6th Australian Software Engineering Conference (ASWEC91), pages 391--404. Australian Computer Society, July 1991. [bib| .pdf]
[172] I.J. Hayes. Interpretations of Z schema operators. In Z User Workshop: Proceedings of the Fifth Annual Z User Meeting, Oxford, December 1990, Workshops in Computing, pages 12--26. Springer, 1991. [bib]
[173] B.P. Mahony and I.J. Hayes. A case study in timed refinement: A central heater. In Proc. BCS/FACS Fourth Refinement Workshop, Workshops in Computing, pages 138--149. Springer, January 1991. [bib| .pdf]
[174] B.P. Mahony and I.J. Hayes. Using continuous real functions to model timed histories. In P.A. Bailes, editor, Proc. 6th Australian Software Engineering Conf. (ASWEC91), pages 257--270. Australian Comp. Soc., 1991. [bib| .pdf]
[175] D.A. Carrington, I.J. Hayes, and J.Welsh. A syntax-directed editor for object-oriented specifications. In Proc. of Pacific TOOLS '90, pages 46--57, November 1990. [bib]
[176] I.J. Hayes. Specifying physical limitations: A case study of an oscilloscope. Technical report 167, Department of Computer Science, University of Queensland, July 1990. [bib| .ps]
[177] I.J. Hayes, M.Mowbray, and G.A. Rose. Signalling System No. 7: The network layer. In E.Brinksma, G.Scollo, and C.A. Vissers, editors, Protocol Specification, Testing and Verification, IX, pages 3--14. Elsevier Science Publishers B. V. (North-Holland), 1990. [bib]
[178] I.J. Hayes. A generalisation of bags in Z. In J.E. Nicholls, editor, Z User Workshop: Proceedings of the Fourth Annual Z User Meeting, Oxford, December 1989, Workshops in Computing, pages 113--127. Springer, 1990. [bib]
[179] I.J. Hayes. Applying formal specification to software development in industry. In RichardH. Thayer and Merlin Dorfman, editors, System and Software Requirements Engineering, pages 594--603. IEEE Computer Society Press Tutorial, 1990. (Previously published in IEEE Transactions on Software Engineering [193]). [bib]
[180] I.J. Hayes and C.B. Jones. Specifications are not (necessarily) executable. IEE/BCS Software Engineering Journal, 4(6):330--338, November 1989. [bib| DOI]
[181] I.J. Hayes, R.Neucom, and J.Welsh. An editor for Z specifications. In Advance papers CASE'89, pages 1--13, 1989. [bib]
[182] R.Duke, I.J. Hayes, and G.A. Rose. Verification of a cyclic retransmission protocol. Technical Report UQ-CS-92, Department of Computer Science, The University of Queensland, July 1988. [bib]
[183] R.Duke, I.J. Hayes, P.King, and G.A. Rose. Protocol specification and verification using Z. In IFIP Eighth International Workshop on Protocol Specification, Testing and Verification, pages 33--46. North-Holland, 1988. [bib]
[184] I.J. Hayes, R.Neucom, and J.Welsh. An editor for Z specifications. Technical report, Department of Computer Science, University of Queensland, 1988. [bib]
[185] C.A.R. Hoare, I.J. Hayes, He Jifeng, C.Morgan, A.W. Roscoe, J.W. Sanders, I.H. Sørensen, J.M. Spivey, and B.A. Sufrin. Laws of programming. Communications of the ACM, 30(8):672--686, August 1987. Corrigenda: CACM 30(9):770. [bib]
[186] G.A. Rose, R.Duke, and I.J. Hayes. Specifying communications services and protocols. In Proc 2nd Australian Software Engineering Conference (ASWEC-87), pages 161--170, Canberra, May 1987. IREE (Australia). [bib]
[187] I.J. Hayes. Correctness of data representations. In Proc. 2nd Australian Software Engineering Conference (ASWEC-87), pages 75--86, Canberra, May 1987. IREE (Australia). [bib]
[188] I.J. Hayes and K.A. Robinson. A Modula-2-based translator generator. Technical report 84, Department of Computer Science, University of Queensland, Brisbane, Australia, 1987. [bib]
[189] I.J. Hayes, editor. Specification Case Studies. Prentice Hall International, 1987. [bib]
[190] I.J. Hayes. Using mathematics to specify software. In Proc. 1st Australian Software Engineering Conference (ASWEC-86), pages 67--71, Canberra, May 1986. Institution of Engineers, Australia. At the 10th ASWEC Conference in 1997 this paper was given the award of Most Influential Paper of ASWEC'86, the first ASWEC Conference. [bib| .pdf]
[191] I.J. Hayes. Specification directed module testing. IEEE Transactions on Software Engineering, SE-12(1):124--133, January 1986. [bib| .pdf]
[192] I.J. Hayes. Weakest pre-specifications: weakest pre-conditions for procedures. In Proc. 9th Australian Computer Science Conference, pages 299--308, Canberra, January 1986. [bib]
[193] I.J. Hayes. Applying formal specification to software development in industry. IEEE Transactions on Software Engineering, SE-11(2):169--178, February 1985. [bib| .pdf]
[194] I.J. Hayes. Computer Architecture: The hardware/software interface. Ph. D. thesis, Department of Computer Science, University of New South Wales, Sydney, Australia, 1983. [bib]
[195] I.J. Hayes and K.A. Robinson. A tutorial on Llama: A Pascal-based translator generator. Technical report, Department of Computer Science, University of New South Wales, Sydney, Australia, 1982. [bib]

This file was generated by bibtex2html 1.99.

Last updated: Wed 3 Jan 2024 17:12:52 AEDT