Abstract Abstract interpretation has been shown to be a promising technique for the thread-modular verification of concurrent programs. Central to this is the generation of interferences, in the form of rely-guarantee conditions, conforming to a user-chosen structure. In this work, we introduce one such structure called the conditional-writes domain, designed for programs where it suffices to establish only the conditions under which particular variables are written to by each thread. We formalise our analysis within a novel abstract interpretation framework that is highly modular and can be easily extended to capture other structures for rely-guarantee conditions. We formalise two versions of our approach and evaluate their implementations on a simple programming language.

Formal Methods (FMs) radically improve the quality of the code artefacts they help to produce. They are simple, probably accessible to first-year undergraduate students and certainly to second-year students and beyond. Nevertheless, in many cases, they are not part of a general recommendation for course curricula, i.e., they are not taught — and yet they are valuable. One reason for this is that teaching “Formal Methods” is often confused with teaching logic and theory. This article advocates what we call FM thinking : the application of ideas from Formal Methods applied in informal, lightweight, practical and accessible ways. We will argue here that FM thinking should be part of the recommended curriculum for every Computer Science student, for even students who train only in that “thinking” will become much better programmers. However, there will be others who, exposed to those ideas, will be ideally positioned to go further into the more theoretical background: why the techniques work, how they can be automated, and how new ones can be developed. Those students would follow subsequently a specialised, more theoretical stream, including topics such as semantics, logics, verification and proof-automation techniques.

Abstract Speculative execution attacks affect all modern processors and much work has been done to develop techniques for detection of associated vulnerabilities. Modern processors also operate on weak memory models which allow out-of-order execution of code. Despite this, there is little work on looking at the interplay between speculative execution and weak memory models. In this paper, we provide an information flow logic for detecting speculative execution vulnerabilities on weak memory models. The logic is general enough to be used with any modern processor, and designed to be extensible to allow detection of vulnerabilities to specific attacks. The logic has been proven sound with respect to an abstract model of speculative execution in Isabelle/HOL.

Rely/guarantee reasoning provides a compositional approach to reasoning about concurrent programs. However, such reasoning traditionally assumes a sequentially consistent memory model and hence is unsound on modern hardware in the presence of data races. In this article, we present a rely/guarantee-based approach for non-multicopy atomic weak memory models, i.e., where a thread’s stores are not simultaneously propagated to all other threads and hence are not observable by other threads at the same time. Such memory models include those of the earlier versions of the ARM processor as well as the POWER processor. This article builds on our approach to compositional reasoning for multicopy atomic architectures, i.e., where a thread’s stores are simultaneously propagated to all other threads. In that context, an operational semantics can be based on thread-local instruction reordering. We exploit this to provide an efficient compositional proof technique in which weak memory behaviour can be shown to preserve rely/guarantee reasoning on a sequentially consistent memory model. To achieve this, we introduce a side-condition, reordering interference freedom on each thread, reducing the complexity of weak memory to checks over pairs of reorderable instructions. In this article, we extend our approach to non-multicopy atomic weak memory models. We utilise the idea of reordering interference freedom between parallel components. This by itself would break compositionality but serves as a vehicle to derive a refined compatibility check between rely and guarantee conditions, which takes into account the effects of propagations of stores that are only partial, i.e., not covering all threads. All aspects of our approach have been encoded and proved sound in Isabelle/HOL.

A number of approaches have been developed for analysing information flow in concurrent programs in a compositional manner, i.e., in terms of one thread at a time. Early approaches modelled the behaviour of a given thread's environment using simple read and write permissions on variables, or by associating specific behaviour with whether or not locks are held. Recent approaches allow more general representations of environmental behaviour, increasing applicability. This, however, comes at a cost. These approaches analyse the code in a forwards direction, from the start of the program to the end, constructing the program's entire state after each instruction. This process needs to take into account the environmental influence on all shared variables of the program. When environmental influence is modelled in a general way, this leads to increased complexity, hindering automation of the analysis. In this paper, we present a compositional information flow analysis for concurrent systems which is the first to support a general representation of environmental behaviour and be automated within a theorem prover. Our approach analyses the code in a backwards direction, from the end of the program to the start. Rather than constructing the entire state at each instruction, it generates only the security-related proof obligations. These are, in general, much simpler, referring to only a fraction of the program's shared variables and thus reducing the complexity introduced by environmental behaviour. For increased applicability, our approach analyses value-dependent information flow, where the security classification of a variable may depend on the current state. The resulting logic has been proved sound within the theorem prover Isabelle/HOL.

Noninterference characterizes a security property in which an attacker cannot determine the inputs to a system based on outputs of a lower classification. Value-dependent noninterference enables the analysis of systems in which these classifications may depend on the system's state and evolve throughout execution. Existing approaches to enforcing such a property for concurrent systems are constrained in their capability to express how the concurrent components modify shared variables and, therefore, the value-dependent classifications. Such approaches typically make use of externally verified annotations or coarse locking primitives to express limited constraints on variables, such as read and write permissions. Consequently, these techniques are insufficient for the analysis of programs that feature complex concurrent behaviours or require fine-grained synchronisation, as seen in non-blocking algorithms. This paper presents a compositional logic for enforcing value-dependent noninterference properties for complex concurrent algorithms, including non-blocking algorithms. It uses rely/guarantee reasoning to establish how classifications may be modified by concurrent components. Additionally, the logic allows for the specification of security policies at a component level and ensures their valid composition. These results have been formalised in Isabelle/HOL.

Abstract Linearizability is a widely accepted notion of correctness for concurrent objects. Recent research has investigated redefining linearizability for particular hardware weak memory models, in particular for TSO. In this paper, we provide an overview of this research and show that such redefinitions of linearizability are not required: under an interpretation of specification behaviour which abstracts from weak memory effects, the standard definition of linearizability is sound and complete on all hardware weak memory models.We prove our result with respect to a definition of object refinement which takes a weak memory model as a parameter. The main consequence of our findings is that we can leverage the range of existing techniques and tools for standard linearizability when verifying concurrent objects running on hardware weak memory models.

Weak memory models are used to increase the performance of concurrent programs by allowing program instructions to be executed on the hardware in a different order to that specified by the software. This places a challenge on the verification of concurrent programs running on weak memory models since the variations in the executions need to be considered. Many approaches of modelling weak memory behaviour focus on architectural models to capture aspects of the hardware's architecture. In this paper, we investigate observational models of weak memory model behaviour which abstract from the underlying hardware architecture, and are instead derived from instruction reordering rules. This enables existing proof methods and tool support for linearizability to be reused. Specifically, we show how one existing proof method and associated model checking approach can be used to reason about programs running on the TSO and XC weak memory models.

Abstract An autonomous agent is one that is not only directed by its environment, but is also driven by internal motivation to achieve certain goals based on beliefs about the environmental behaviour. Design paradigms for autonomous agents such as belief-desire-intention take into account the agent’s “mental” features when presenting its patterns of behaviour. In this paper we present an approach to modelling autonomous agents by introducing mental features to conventional transition system specifications. Mental features such as belief and desire are represented by declarative linear temporal logic formulas. Refinement is then proposed to define the correctness of the agent design and development. It turns out, however, that the introduction of these mental features is not monotonic with respect to refinement. We therefore introduce additional refinement proof obligations to enable the use of simulation rules when checking refinement.

Abstract In the late 1980’s, Back extended the notion of stepwise refinement of sequential systems to concurrent systems. By doing so he provided a definition of what it means for a concurrent system to be correct with respect to an abstract (potentially sequential) specification. This notion of refinement, referred to as trace refinement , was also independently proposed by Abadi and Lamport and has found widespread acceptance and application within the refinement community. Around the same time as Back’s work, Herlihy and Wing proposed linearizability as the correctness notion for concurrent objects. Linearizability has also found widespread acceptance being regarded as the standard notion of correctness for concurrent objects in the concurrent-algorithms community. In this paper, we provide a formal link between trace refinement and linearizability. This allows us to compare the two correctness conditions. Our comparisons show that trace refinement implies linearizability, but that linearizability does not imply trace refinement in general. However, linearizability does imply trace refinement under certain conditions. These conditions relate to (i) the fact that trace refinement can be used to prove both safety and liveness properties, whereas linearizability can only be used to prove safety properties, and (ii) the fact that trace refinement depends on the identification of when operations in the implementation are observed to occur. We discuss the consequences of these differences in the context of verifying concurrent objects.

Correctness of concurrent objects is defined in terms of conditions that determine allowable relationships between histories of a concurrent object and those of the corresponding sequential object. Numerous correctness conditions have been proposed over the years, and more have been proposed recently as the algorithms implementing concurrent objects have been adapted to cope with multicore processors with relaxed memory architectures. We present a formal framework for defining correctness conditions for multicore architectures, covering both standard conditions for totally ordered memory and newer conditions for relaxed memory, which allows them to be expressed in uniform manner, simplifying comparison. Our framework distinguishes between order and commitment properties, which in turn enables a hierarchy of correctness conditions to be established. We consider the Total Store Order (TSO) memory model in detail, formalise known conditions for TSO using our framework, and develop sequentially consistent variations of these. We present a work-stealing deque for TSO memory that is not linearizable, but is correct with respect to these new conditions. Using our framework, we identify a new non-blocking compositional condition, fence consistency, which lies between known conditions for TSO, and aims to capture the intention of a programmer-specified fence.

Self-organising systems are distributed systems which achieve an ordered global state without centralised control. They include adaptive sensor networks, swarm robotic systems and mobile ad-hoc networks. Designing such systems is difficult and often based on a trial-and-error approach. In this paper, we provide an approach which is both systematic and formal. Our approach builds on the formalism of Object-Z and the refinement approach of action systems. It follows an intuitive approach to development which breaks a refinement proof into three steps which the designer may iterate through on the way to the final design.

Asynchronous multi-agent systems (AMAS) are multi-agent systems with asynchronous updates and communications. They are often designed from the point of view of local computations and the interactions of autonomous agents. However, often some functionality of the system is proposed from the global point of view. It is not always possible to verify such global functionality under total, random, asynchrony and such asynchrony is unrealistic in most cases. Several non-functional factors such as the variance of local clocks of the agents and the message delays play essential roles in implementing ordered asynchrony in practice and should be taken into account in the specification and verification. In this paper, we present a specification framework for AMAS using Object-Z and bounded fairness constraints. The bounded fairness constraints are used to specify required non-functional factors. We demonstrate that under these constraints the system's functionality can be guaranteed by the local behaviour of the agents.

Self-organising systems have become important relatively recently. It is frequently claimed that their complex nature necessitates new formalisms to express and reason about them. In this paper the opposite view is taken. Following Back's use of action systems to express a distributed system as an initialised possibly nonterminating loop, here two simple but representative case studies of self-organising systems are explored using only conventional techniques. The first deals with the configuration of an ad hoc network and shows how safety and liveness can be accurately expressed with an initialised loop. The second involves, like many self-organising systems, probabilistic behaviour and it is shown that existing techniques suffice to establish the system behaviour. In conclusion, the techniques illustrated can be used to provide a higher level of assurance than is possible with simulation alone.

The complexity of multi-agent systems (MAS) demands a formal and incremental approach to their development. Such an approach needs to take into account issues specific to the development of MAS. In particular, methods are required for incrementally introducing agent decisionmaking procedures, and inter-agent negotiation mechanisms. This paper introduces an approach to modelling MAS and a definition of action refinement in Object-Z aimed at addressing these issues.

Abstract Formal specification languages such as Z, B and VDM are used in the incremental development of abstract specifications (suitable for establishing required properties) to more concrete specifications (resembling the final implementation). This incremental development process, known as refinement , preserves all observable properties of the original abstract specification. Recent research has looked at applying temporal-logic model checking to such specification languages. While this assists in the establishment of properties of the abstract specification, temporal-logic properties typically refer to state variables which are regarded as non-observable. Hence, such properties are not guaranteed to be preserved by refinement. This paper investigates the classes of temporal-logic properties which are preserved by refinement, and for some of those properties that are not preserved in general, the restrictions on the refinement process under which they are preserved. Results are presented for the temporal logics LTL, CTL and the μ -calculus and the formal specification language Z. They apply equally, however, to related formal specification languages such as B and VDM.

Abstract Emergent behaviour—system behaviour not determined by the behaviours of system components when considered in isolation—is commonplace in multi-agent systems, particularly when agents adapt to environmental change. This article considers the manner in which Formal Methods may be used to authenticate the trustworthiness of such systems. Techniques are considered for capturing emergent behaviour in the system specification and then the incremental refinement method is applied to justify design decisions embodied in an implementation. To demonstrate the approach, one and two-dimensional cellular automata are studied. In particular an incremental refinement of the ‘glider’ in Conway’s Game of Life is given from its specification.

Specification notations such as JML and Spec# which are embedded into program code provide a promising approach to formal object-oriented software development. If the program code is refactored, however, the specifications need also to be changed. This can be facilitated by specification refactoring rules which allows such changes to be made systematically along with the changes to the code. A set of minimal and complete set of refactoring rules have been devised for the Object-Z specification language. This paper reviews these rules as a basis for a similar approach for languages like JML and Spec#. Specifically, it modifies the rules for introducing and removing inheritance and polymorphism from specifications. While these concepts are orthogonal in Object-Z, they are closely intertwined in the other notations.

No abstract available.

Abstract Action systems provide a formal approach to modelling parallel and reactive systems. They have a well established theory of refinement supported by simulation-based proof rules. This paper introduces an automatic approach for verifying action system refinements utilising standard CTL model checking. To do this, we encode each of the simulation conditions as a simulation machine , a Kripke structure on which the proof obligation can be discharged by checking that an associated CTL property holds. This procedure transforms each simulation condition into a model checking problem. Each simulation condition can then be model checked in isolation, or, if desired, together with the other simulation conditions by combining the simulation machines and the CTL properties.

Formal specifications of software systems need to evolve in many ways during system development. Not only are changes required to refine the specification towards an implementation, they are also required in response to changes in requirements, or to incorporate different aspects of the system, e.g., fault tolerance or timing, initially ignored in order to simplify reasoning. This paper presents an approach for evolving Z specifications by the step-wise application of a number of simple rules. These rules not only document the specification's evolution, but also make precise how safety properties of the system evolve with the specification. Hence, reasoning about these properties performed on the original specification need not be repeated on the new specification.

Abstract In this paper, we consider how refinements between state-based specifications (e.g., written in Z) can be checked by use of a model checker. Specifically, we are interested in the verification of downward and upward simulations which are the standard approach to verifying refinements in state-based notations. We show how downward and upward simulations can be checked using existing temporal logic model checkers. In particular, we show how the branching time temporal logic CTL can be used to encode the standard simulation conditions. We do this for both a blocking, or guarded, interpretation of operations (often used when specifying reactive systems) as well as the more common non-blocking interpretation of operations used in many state-based specification languages (for modelling sequential systems). The approach is general enough to use with any state-based specification language, and we illustrate how refinements between Z specifications can be checked using the SAL CTL model checker using a small example.

No abstract available.

We discuss a methodology for animating the Object-Z specification language using a Z animation environment. Central to the process is the introduction of a framework to handle dynamic instantiation of objects and management of object references. Particular focus is placed upon building the animation environment through pre-existing tools, and a case study is presented that implements the proposed framework using a shallow encoding in the Possum Z animator. The animation of Object-Z using Z is both automated and made transparent to the user through the use of a software tool named O-zone.

Abstract. This paper is concerned with methods for refinement of specifications written using a combination of Object-Z and CSP. Such a combination has proved to be a suitable vehicle for specifying complex systems which involve state and behaviour, and several proposals exist for integrating these two languages. The basis of the integration in this paper is a semantics of Object-Z classes identical to CSP processes. This allows classes specified in Object-Z to be combined using CSP operators. It has been shown that this semantic model allows state-based refinement relations to be used on the Object-Z components in an integrated Object-Z/CSP specification. However, the current refinement methodology does not allow the structure of a specification to be changed in a refinement, whereas a full methodology would, for example, allow concurrency to be introduced during the development life-cycle. In this paper, we tackle these concerns and discuss refinements of specifications written using Object-Z and CSP where we change the structure of the specification when performing the refinement. In particular, we develop a set of structural simulation rules which allow single components to be refined to more complex specifications involving CSP operators. The soundness of these rules is verified against the common semantic model and they are illustrated via a number of examples.

Abstract. This paper presents Real-Time Object-Z: an integration of the object-oriented, state-based specification language Object-Z with the timed trace notation of the timed refinement calculus. This integration provides a method of formally specifying and refining systems involving continuous variables and real-time constraints. The basis of the integration is a mapping of the existing Object-Z history semantics to timed traces.

This paper investigates model checking Object-Z classes via their translation to the input notation of the CSP model checker FDR. Such a translation must not only be concerned with preserving the semantics of the original specification, but also with how efficiently the resulting specification can be model checked. Hence, the paper investigates alternative translation schemes and compares how efficiently the resulting specifications can be checked.

The formal development of large or complex systems can often be facilitated by the use of more than one formal specification language. Such a combination of languages is particularly suited to the specification of concurrent or distributed systems, where both the modelling of processes and state is necessary. This paper presents an approach to refinement and verification of specifications written using a combination of Object-Z and CSP (communicating sequential processes). A common semantic basis for the two languages enables a unified method of refinement to be used, based upon CSP refinement. To enable state-based techniques to be used for the Object-Z components of a specification, we develop state-based refinement relations which are sound and complete with respect to CSP refinement. In addition, a verification method for static and dynamic properties is presented. The method allows us to verify properties of the CSP system specification in terms of its component Object-Z classes by using the laws of the CSP operators together with the logic for Object-Z.

Abstract Objects can be viewed as entities reacting concurrently with their environment through the sending and receiving of messages. In this paper a model for such reactive objects is constructed where messages may be blocked either by the object or by the environment. This model differentiates between output messages controlled by the object, and input messages controlled by the environment. The model is applied to define an object compatibility lattice structure enabling the construction of objects satisfying best possible compatibility requirements.

This paper presents a method of reasoning about Object-Z specifications. The approach utilises the modularity inherent in Object-Z specifications to simplify proofs. Properties proved for a class in isolation can be used when that class is either inherited by another class or instantiated as part of a system of interacting objects. Proofs using structural induction and the notion of object integrity are discussed.

Abstract This paper presents a fully abstract semantics of classes for the object oriented formal specification language Object-Z. Such a semantics includes no unnecessary syntactic details and, hence, describes a class in terms of the external behaviour of its objects only. The semantics, based on an extension of existing process models, defines a notion of behavioural equivalence which is stronger than that of CSP and weaker than that of CCS.

The modular refinement of object-oriented specifications requires a sound theory of behavioural compatibility of classes. Such a theory will depend on the way in which objects of a class interact with their environment. This paper defines two notions of behavioural compatibility. Observational compatibility is relevant when an active object is placed within a passive environment and operational compatibility when a passive object is placed in an active environment. Rules for maintaining each type of behavioural compatibility through inheritance are also presented.>