Conference Papers by Ian Hayes

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.

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

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

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

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

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.

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.

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.

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.

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

Well understood methods exist for developing programs from formal project = "DCCS", 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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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

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.

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.

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.

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.

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

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.