Hoare-style inference rules for program constructs permit the copying of expressions and tests from program text into logical contexts. It is known that this requires care even for sequential programs but much more serious issues arise with concurrent programs because of potential interference to the values of variables. The “rely-guarantee” approach tackles the challenge of recording acceptable interference and offers a way to provide safe inference rules for concurrent constructs. This article shows how the algebraic presentation of rely-guarantee ideas can clarify and formalise the conditions for safely re-using expressions and tests from program text in logical contexts for reasoning about concurrent programs; crucially this extends to handling expressions that reference more than one shared variable. A non-trivial example related to the Fischer-Galler forest representation of equivalence relations is treated.

This article presents a general formal framework for describing the relationship between a criticality-aware scheduler, a set of application jobs that are assigned different criticality levels, and an environment that generates both work and faults that the run-time system must control. The proposed formalism extends the rely-guarantee approach, which facilitates formal reasoning about the functional behaviour of concurrent systems, to address real-time properties. The exposition of the general framework is supplemented by a seven step approach that enables it to be instantiated to deliver the formal specification of any proposed mixed-criticality scheduling protocol. The expressive power of the approach is explored via a non-trivial instantiation.

Abstract The reference point for developing any artefact is its specification; to develop software formally, a formal specification is required. For sequential programs, pre and post conditions (together with abstract objects) suffice; rely and guarantee conditions extend the scope of formal development approaches to tackle concurrency. In addition, real-time systems need ways of both requiring progress and relating that progress to some notion of time. This paper extends rely-guarantee ideas to cope with specifications of—and assumptions about—real-time schedulers. Furthermore it shows how the approach helps identify and specify fault-tolerance aspects of such schedulers by systematically challenging the assumptions.

In addition to the major UK contributions to research underpinning formal approaches to the specification and development of computer systems—and perhaps as a consequence of this—some significant attempts to deploy the ideas into practical environments have taken place in the United Kingdom. The authors of this article have been involved in formal methods for many years and both had contact with a significant proportion of this history. This article both lists key ideas and indicates where attempts were made to use the ideas in practice. Not all of these deployment stories have been a complete success and an attempt is made to tease out lessons that influence the probability of successful long-term changes to software engineering.

Abstract Cyber physical systems (CPS) exist in a physical environment and comprise both physical components and a control program. Physical components are inherently liable to failure and yet an overall CPS is required to operate safely, reliably and cost effectively. This paper proposes a framework for deriving the specification of the software control component of a CPS from an understanding of the behaviour required of the overall system in its physical environment. The two key elements of this framework are (i) an extension to the use of rely/guarantee conditions to allow specifications to be obtained systematically from requirements (as expressed in terms of the required behaviour in the environment) and nested assumptions (about the physical components of the CPS); and (ii) the use of time bands to record the temporal properties required of the CPS at a number of different granularities. The key contribution is in combining these ideas; using time bands overcomes a significant drawback in earlier work. The paper also addresses the means by which the reliability of a CPS can be addressed by challenging each rely condition in the derived specification and, where appropriate, improve robustness and/or define weaker guarantees that can be delivered with respect to the corresponding weaker rely conditions.

The collection of papers in this edition signals a new departure for our journal. At a meeting of many of the editors in Oxford in 2018, the idea evolved of having occasional focused special issues. Rather soon after the meeting, two themes crystallized. The current editors suggested having a special issue addressing the history of the development of ideas that form the basis of formal methods. Our aim is to facilitate the collection of source material for later historians.

Abstract Decomposing the design (or documentation) of large systems is a practical necessity but finding compositional development methods for concurrent software is technically challenging. This paper includes the development of a difficult example in order to draw out lessons about such methods. The concurrent garbage collector development is interesting in several ways; in particular, the final step of its development appears to be just beyond what can be expressed by rely/guarantee relations. This prompts an exploration of the limitations of this well-known method. Although the rely/guarantee approach is used, most of the lessons are more general.

No abstract available.

No abstract available.

Abstract One might think that specifying and reasoning about concurrent programs would be easier with more expressive languages. This paper questions that view. Clearly too weak a notation can mean that useful properties either cannot be expressed or their expression is unnatural. But choosing too powerful a notation also has its drawbacks since reasoning receives little guidance. For example, few would suggest that programming languages themselves provide tractable specifications. Both rely/guarantee methods and separation logic(s) provide useful frameworks in which it is natural to reason about aspects of concurrency. Rather than pursue an approach of extending the notations of either approach, this paper starts with the issues that appear to be inescapable with concurrency and—only as a response thereto—examines ways in which these fundamental challenges can be met. Abstraction is always a ubiquitous tool and its influence on how the key issues are tackled is examined in each case.

No abstract available.

No abstract available.

No abstract available.

It might appear that having highly expressive notations is an advantage in writing specifications and subsequently reasoning about programs. Even for sequential programs, this is not always true: simple type systems that are statically decidable or fixed formats of specifications that yield intuitive proof obligations both indicate that constrained expressiveness can increase tractability. The aim here is to examine some of the trade-offs in expressiveness for notations that address concurrency. The Rely/Guarantee approach to top-down development of concurrent programs offers a way of recording assumptions and commitments about interference. In the same way that pre conditions invite the designer of a component to ignore the possibility that the artifact they are to create will start in states that fail to satisfy the predicate, rely conditions record assumptions the developer is invited to make about any interfering state transitions from the environment in which the artifact will be deployed. In other words, the developer cannot be held liable for the behaviour of the artifact in environments that do not satisfy either assumption. In contrast, just as the post condition expresses a relation that must hold between the initial and final, a guarantee condition records the relation that must exist over any state transition of the artifact. (There are obvious robustness arguments for making components as general as possible; this is not the subject here; it is inevitable that any non-trivial component will need some assumptions.) The decision to use simple relations on pairs of states for (post and) rely and guarantee conditions is a restriction on expressiveness. The restriction, however, means that a reasonably tractable set of proof rules can be given for compositional development of concurrent programs (see [1]; a more recent soundness proof is [2]). In contrast, the initial goal of Concurrent Separation Logic [3] was the bottom-up analysis of intricate code that manipulates heap variables. Here again, there is a deliberate decision to focus on expressing a set of issues: those concerned with separation or ownership. Separation logic has spawned many variants (cf. [4]) but each has a set of operators with neat algebraic properties.

Expression evaluation in programming languages is normally assumed to be deterministic; however, if an expression involves variables that are being modified by the environment of the process during its evaluation, the result of the evaluation can be non-deterministic. Two common scenarios in which this occurs are concurrent programs within which processes share variables and real-time programs that interact to monitor and/or control their environment. In these contexts, although any particular evaluation of an expression gives a single result, there is a range of possible values that could be returned depending on the relative timing between modification of a variable by the environment and its access within the expression evaluation. To compare the semantics of non-deterministic expression evaluation, one can use the set of possible values the expression evaluation could return. This paper formalizes three approaches to non-deterministic expression evaluation, highlights their commonalities and differences, shows the relationships between the approaches and explores conditions under which they coincide. Modal operators representing that a predicate holds for all possible evaluations and for some possible evaluation are associated with each of the evaluation approaches, and the properties and relationships between these operators are investigated. Furthermore, a link is made to a new notation used in reasoning about interference.

No abstract available.

Abstract Arguing that intricate concurrent programs satisfy their specifications can be difficult; recording understandable explanations is important for subsequent readers. Abstraction is a key tool even for sequential programs. The purpose here is to explore some abstractions that help readers (and writers) understand the design of concurrent programs. As an illustration, the paper presents a formal development of a non-trivial parallel program: Simpson’s implementation of asynchronous communication mechanisms. Although the correctness of this “4-slot algorithm” has been shown elsewhere, earlier proofs fail to offer much insight into the design. From an understandable (yet formal) design history of this one algorithm, the techniques employed in the explanation are teased out for wider application. Among these techniques is using a “fiction of atomicity” as an aid to understanding the initial steps of development. The rely-guarantee approach is, here, combined with notions of read/write frames and “phased” specifications; furthermore, the atomicity assumptions implied by the rely/guarantee conditions are achieved by clever choice of data representations.

My first attempt to build a "formal development support system" was in IBM in the 1970s; more public is the mural system we built in Manchester; the Rodin (EU) project developed a set of open source tools that are now being used in the (EU) DEPLOY project. These attempts give me some perspective from which to predict what sort of tool will finally make the difference to software developers that CAD systems have made in hardware design.

No abstract available.

This issue of Formal Aspects is devoted to an experiment conducted as part of the world-wide Grand Challenge in Verified Software.The challenge is to achieve a significant body of verified programs that have precise external specifications, complete internal specifications, and machine-checked proofs of correctness with respect to a sound theory of programming.The first pilot project in the challenge was to mechanise the proof of correctness of the Mondex smart-card for electronic finance.Eight international research groups tackled the problem, and the following papers record the experiences of six of these groups.The pilot project remains open for other groups to contribute. The certification of the Mondex electronic purse to ITSEC Level E6Woodcock, Stepney, Cooper, Clark, and Jacob were all involved in the original work on Mondex; the first three were specifiers and the last two evaluators.They recall the work that led to the successful certification of the Mondex electronic purse, and the research that this inspired.The paper contains an introduction to the Mondex specification and refinement, and an overview of the proof. Mondex, an electronic purse: specification and refinement checks with the Alloy model-finding methodRamananandro started from the existing specification on Mondex in Z, and constructed a specification in the Alloy specification language, which is based on relational first-order logic with transitive closures.The experiment shows that, if the concerns about finiteness are dropped, then the Mondex specification can be expressed in first-order logic without transitive closures.Ramananandro checked the specification with the Alloy Analyser, a tool for finding models.The Analyser translates the specification into a boolean formula, which it then tries to satisfy.If an assignment of variables is found, then the program translates it back to get a counterexample.This can be accomplished only for bounded numbers of objects: their scope.The specification has been checked for a scope of at most eight objects of each kind.The analysis found several bugs in Mondex: (i) purses can hold unauthentic transaction details; (ii) a wrong case analysis in a proof; (iii) a mistake in a framing schema.

This paper looks at the wider system surrounding a "Mondex" electronic purse. It does this from a process-oriented perspective using the pi-calculus. Our model includes the issuing of purses by an authorised bank and the decisions of cardholders to participate in transactions.

No abstract available.

Various forms of rely/guarantee conditions have been used to record and reason about interference in ways that provide compositional development methods for concurrent programs. This article illustrates such a set of rules and proves their soundness. The underlying concurrent language allows fine-grained interleaving and nested concurrency; it is defined by an operational semantics; the proof that the rely/guarantee rules are consistent with that semantics (including termination) is by a structural induction. A key lemma which relates the states which can arise from the extra interference that results from taking a portion of the program out of context makes it possible to do the proofs without having to perform induction over the computation history. This lemma also offers a way to think about expressibility issues around auxiliary variables in rely/guarantee conditions.

This roadmap describes ways that researchers in four areas---specification languages, program generation, correctness by construction, and programming languages---might help further the goal of verified software. It also describes what advances the "verified software" grand challenge might anticipate or demand from work in these areas. That is, the roadmap is intended to help foster collaboration between the grand challenge and these research areas.A common goal for research in these areas is to establish language designs and tool architectures that would allow multiple annotations and tools to be used on a single program. In the long term, researchers could try to unify these annotations and integrate such tools.

Dynamic coalitions are temporary alliances formed between agents in order to achieve specific business goals. Such coalitions can vary widely in architecture, scale, complexity and lifetime. Few techniques have so far emerged to assist in the analysis and design of coalitions. We apply formal model- oriented techniques to help structure the space of dynamic coalitions, with an emphasis on modelling information flow. A series of models is developed in VDM, each emphasising a different "dimension" of the space. These are used to characterise a new dynamic coalition architecture under development for the chemical engineering industry. Tool-supported analysis of this formal model has identified potential improvements in the coalition architecture.

No abstract available.

No abstract available.

No abstract available.

The integration of complex systems out of existing systems is an active area of research and development. There are many practical situations in which the interfaces of the component systems, for example belonging to separate organisations, are changed dynamically and without notification. In this paper we propose an approach to handling such upgrades in a structured and disciplined fashion. All interface changes are viewed as abnormal events and general fault tolerance mechanisms (exception handling, in particular) are applied to dealing with them. The paper outlines general ways of detecting such interface upgrades and recovering after them. An Internet Travel Agency is used as a case study.

Abstract. Professor Edsger W. Dijkstra has had a profound effect on many aspects of Computer Science. His death will leave a huge gap in our scientific world. The personal loss to those who had the privilege of knowing Edsger is even larger. Edsger was not always the easiest of colleagues: he held strong opinions and rarely hid them. His exacting scientific standards have had an enormous impact on computing science. Edsger's writings have shaped and will continue to influence our subject. Those who worked closely with him and have taken up his methods and ideas will continue to be heard. This edition of Formal Aspects contains a wonderfully insightful memorial written by Krzysztof Apt. In his balanced obituary, Apt refers to the famous “EWD” reports whose contribution we reflect by printing one that has not previously been published: we are grateful to Ria Dijkstra for permission to so do and for help from Ham Richards (Ham was also behind the lens for the evocative photograph of Edsger). Many EWDs were circulated as copies of Edsger's clear handwriting and although EWD1300 is printed here in typescript, a complete library in Edsger's hand is available at http://www.cs.utexas.edu/users/EWD/

Describes the haptic rendering of a virtual environment by drawing upon concepts developed in the area of teleoperation. A four-channel teleoperation architecture is shown to be an effective means of coordinating the control of a 3-DOF haptic interface with the simulation of a virtual dynamic environment.

Formal Aspects of Computing marks the end of the first year of our re-launched format. It has not been an easy year either for the editors or for the ever-patient staff at Springer-Verlag; but it has certainly been successful with first class papers being published soon after acceptance. As with most computing journals, refereeing poses a (potential) bottleneck to getting an author's ideas into print but even here our colleagues at Springer-Verlag have come up with an incentive scheme from which our future referees will benefit and hopefully speed the refereeing process to everyone's advantage. Recently, most editions of the journal have been standard issues with a number of submitted papers. It has been our stated intention since the journal began to have special editions with whole editions on a single topic. We are currently planning such a special edition to mark Rod Burstall's retirement (in fact we have so many excellent papers that there will probably have to be a double edition). This special issue collects a number of papers on X-machines edited by Mike Holcombe and myself. Mike has written a brief introduction and there follow five papers which have all been refereed by experts in the area (I took personal charge of having Mike's paper refereed). The generalisation of the testing theory to non-deterministic stream X-machines is the focus of two articles. Non-determinism can be generalised in several ways. R. Hierons and M. Harman look at quasi-non-deterministic machines and describe an approach to dealing with the generation of test sets for such machines. F. Ipate and M. Holcombe look at another way to view non-determinism and also focus on test set generation, the issue of fairness becomes important if the strong claims about fault detection by the test sets are to be achieved. M. Gheorghe has investigated how a collection of formal grammars can be controlled by a type of generalised stream X-machine so that the languages generated by such a system of grammars can be determined. He has shown that relatively simple grammars can generate very complex languages using this approach. T. Balanescu explores further generalisations of Stream X-machines and discusses how the design for test conditions can be adapted for a specific type of machine. A. Cowling et al. look at communicating X-machine systems and consider how this approach can be used to model message passing using a simple communicating matrix metaphor. Models built this way can be used to generate, automatically, concurrent programs. In a paper to appear in Volume 13, F. Ipate and M. Holcombe look at how the test theory can be adapted to apply to the communicating X-machines systems case. Indeed, Volume 13 already looks to be an exciting mix of scientific contributions – we also expect to back on a more regular publication schedule by the end of 2001.

Multiple-precision arithmetic overcomes the round-off error incurred in conventional floating-point arithmetic, at the cost of increased processing overhead.Significance arithmetic takes into account the Inexactness of the operands of a calculation, but can lead to loss of significant digits after a long series of operations.A new technique is described whmh alleviates the overhead of multiple-precision arithmetic by allowing nonsignificant digits to be discarded, while limiting the significance loss per operation to a controllable and acceptable rate.The technique is based on storing an inexact number as an interval, using a criterion of slgmficance to determine the precision with which the limits of the interval should be stored.A procedure referred to as a slgmficance rule uses this criterion to remove some of the nonsignificant digits from the limits of an interval prior to storage.A certain number of nonslgmficant digits are retained as guard digits.Calculations are performed using exact interval anthmetm and the significance-rule procedure is invoked after each operation to remove superfluous &glts.Round-off in the procedure causes a slight increase in the interval width on each operation.This results in a cumulative loss of significance at a rate related to the number of guard digits.

Development methods for (sequential) programs that run in isolation have been studied elsewhere.Programs that run in parallel can interfere with each other, either via shared storage or by sending messages.Extensions to earlier development methods are proposed for the rigorous development of interfering programs.In particular, extensions to the specification method based on postconditions that are predicates of two states and the development methods of operation decomposition and data refinement are proposed.

The Elias source coding scheme is modified to permit a source sequence of practically unlimited length to be coded as a single codeword using arithmetic of only limited precision. The result is shown to be a nonblock arithmetic code of the first in, first out (FIFO) type-- source symbols are decoded in the same order as they were encoded. Codeword lengths which are near optimum for the specified statistical properties of the source can be achieved. Explicit encoding and decoding algorithms are Provided which effectively implement the coding scheme. Applications to data compression and cryptography are suggested.

This paper presents an approach to hidden line removal which relies on three-dimensional objects being described in terms of a series of inter-connected spatial cells. Avenues of sight through the openings between cells are explored in the process of generating display information for a perspective picture from a given viewpoint. An implementation on a small computer with a graphics display is described, and the performance of the program is illustrated by photographs of some views which were generated in a few seconds. Data preparation for the examples involved the definition of the space surrounding the objects by means of a special purpose data structure.

This paper describes how a particular computer application was tackled using a “Compiler” approach, and how the work is to be extended.