Conference Papers 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] 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]
[10] 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.
[11] 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.
[12] 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]
[13] 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.
[14] 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.
[15] 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.
[16] 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.
[17] 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.
[18] 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.
[19] 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:
[20] 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: ?
[21] 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:
[22] 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
[23] 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
[24] 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.
[25] 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
[26] 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.
[27] 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
[28] 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
[29] 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
[30] 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.
[31] 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
[32] 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
[33] 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
[34] 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
[35] 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.
[36] 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.
[37] 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
[38] 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.
[39] 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.
[40] 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.

[41] 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.
[42] 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.
[43] 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.

[44] 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.

[45] 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]
[46] 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.
[47] 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.

[48] 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.
[49] 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.

[50] 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.

[51] 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.

[52] 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]
[53] 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.

[54] 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.

[55] 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.

[56] 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
[57] 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]
[58] 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]
[59] 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.
[60] 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
[61] 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.
[62] 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 [?]. [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.

[63] 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.
[64] 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.

[65] 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]
[66] 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.
[67] 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]
[68] 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]
[69] 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]
[70] 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]
[71] 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]
[72] 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.
[73] 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]
[74] 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.
[75] 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]
[76] 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]
[77] 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]
[78] 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.
[79] 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]
[80] 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]
[81] 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]
[82] 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]
[83] 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]
[84] 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]
[85] 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]
[86] 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]
[87] 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]
[88] 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.
[89] 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]
[90] 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]
[91] 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]
[92] 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]
[93] 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]
[94] 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]
[95] 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]
[96] 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]
[97] 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]
[98] 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]
[99] 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]
[100] 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]
[101] 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]
[102] 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]
[103] 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]
[104] I.J. Hayes, R.Neucom, and J.Welsh. An editor for Z specifications. In Advance papers CASE'89, pages 1--13, 1989. [bib]
[105] 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]
[106] 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]
[107] 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]
[108] 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]
[109] 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]

This file was generated by bibtex2html 1.99.

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