We make the case that the foundation for Rely-Guarantee reasoning can be fruitfully delivered by a coinductive semantics. Using insight from an Isabelle formalization, via a proof analysis we show that the coinductive semantics tends to simplify the proof development; in particular it enables more direct proofs for the soundness of the Rely-Guarantee rules. The comparison between inductive and coinductive proofs also suggests inductive counterparts of coinductive “up-to” enhancements. On the way, we fill a gap in the literature, by showing that three previously defined inductive semantics for Rely-Guarantee are equivalent. Underlying our transformation of an inductive into a coinductive semantics is the notion of inductively approximating a coinductive predicate—which, deployed in the opposite direction (from coinduction to induction), is a standard technical tool for approximating process algebra bisimilarities. On the spectrum between the abstract fixpoint theorems and concrete instances, we formalize effective format-based criteria that enable sound approximation.

Abstract Meltdown and Spectre are vulnerabilities known as transient execution vulnerabilities, where an attacker exploits speculative execution (a semantic optimization present in most modern processors) to break confidentiality. We introduce relative security , a general notion of information-flow security that models this type of vulnerability by contrasting the leaks that are possible in a “vanilla” semantics with those possible in a different semantics, often obtained from the vanilla semantics via some optimizations. We describe incremental proof methods, in the style of Goguen and Meseguer’s unwinding, both for proving and for disproving relative security, and deploy these to formally establish the relative (in)security of some standard Spectre examples. Both the abstract results and the case studies have been mechanized in the Isabelle/HOL theorem prover. This paper is an extension of an earlier conference paper that provides significantly more detail on the Isabelle formalization and the unwinding proof process.

Non-volatile memory (NVM), also known as persistent memory, is an emerging paradigm for memory that preserves its contents even after power loss. NVM is widely expected to become ubiquitous, and hardware architectures are already providing support for NVM programming. This has stimulated interest in the design of novel concepts ensuring correctness of concurrent programming abstractions in the face of persistency and in the development of associated verification approaches. Software transactional memory (STM) is a key programming abstraction that supports concurrent access to shared state. In a fashion similar to linearizability as the correctness condition for concurrent data structures, there is an established notion of correctness for STMs known as opacity. We have recently proposed durable opacity as the natural extension of opacity to a setting with non-volatile memory. Together with this novel correctness condition, we designed a verification technique based on refinement. In this paper, we extend this work in two directions. First, we develop a durably opaque version of NOrec (no ownership records), an existing STM algorithm proven to be opaque. Second, we modularise our existing verification approach by separating the proof of durability of memory accesses from the proof of opacity. For NOrec, this allows us to re-use an existing opacity proof and complement it with a proof of the durability of accesses to shared state.

Abstract Non-volatile memory (NVM), aka persistent memory, is a new memory paradigm that preserves its contents even after power loss. The expected ubiquity of NVM has stimulated interest in the design of persistent concurrent data structures, together with associated notions of correctness. In this paper, we present a formal proof technique for durable linearizability , which is a correctness criterion that extends linearizability to handle crashes and recovery in the context ofNVM.Our proofs are based on refinement of Input/Output automata (IOA) representations of concurrent data structures. To this end, we develop a generic procedure for transforming any standard sequential data structure into a durable specification and prove that this transformation is both sound and complete. Since the durable specification only exhibits durably linearizable behaviours, it serves as the abstract specification in our refinement proof. We exemplify our technique on a recently proposed persistentmemory queue that builds on Michael and Scott’s lock-free queue. To support the proofs, we describe an automated translation procedure from code to IOA and a thread-local proof technique for verifying correctness of invariants.

This paper develops an operational semantics for a release-acquire fragment of the C11 memory model with relaxed accesses. We show that the semantics is both sound and complete with respect to the axiomatic model of Batty et al. The semantics relies on a per-thread notion of observability, which allows one to reason about a weak memory C11 program in program order. On top of this, we develop a proof calculus for invariant-based reasoning, which we use to verify the release-acquire version of Peterson's mutual exclusion algorithm.

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.

Correctness conditions like linearizability and opacity describe some form of atomicity imposed on concurrent objects. In this paper, we propose a correctness condition (called causal atomicity) for concurrent objects executing in a weak memory model, where the histories of the objects in question are partially ordered. We establish compositionality and abstraction results for causal atomicity and develop an associated refinement-based proof technique.

Abstract Software transactional memory (STM) provides programmers with a high-level programming abstraction for synchronization of parallel processes, allowing blocks of codes that execute in an interleaved manner to be treated as atomic blocks. This atomicity property is captured by a correctness criterion called opacity , which relates the behaviour of an STM implementation to those of a sequential atomic specification. In this paper, we prove opacity of a recently proposed STM implementation: the Transactional Mutex Lock (TML) by Dalessandro et al. For this, we employ two different methods: the first method directly shows all histories of TML to be opaque (proof by induction), using a linearizability proof of TML as an assistance; the second method shows TML to be a refinement of an existing intermediate specification called TMS2 which is known to be opaque (proof by simulation). Both proofs are carried out within interactive provers, the first with KIV and the second with both Isabelle and KIV. This allows to compare not only the proof techniques in principle, but also their complexity in mechanization. It turns out that the second method, already leveraging an existing proof of opacity of TMS2, allows the proof to be decomposed into two independent proofs in the way that the linearizability proof does not.

Transactional Memory (TM) is a high-level programming abstraction for concurrency control that provides programmers with the illusion of atomically executing blocks of code, called transactions. TMs come in two categories, optimistic and pessimistic, where in the latter transactions never abort. While this simplifies the programming model, high-performing pessimistic TMs can be complex. In this paper, we present the first formal verification of a pessimistic software TM algorithm, namely, an algorithm proposed by Matveev and Shavit. The correctness criterion used is opacity, formalising the transactional atomicity guarantees. We prove that this pessimistic TM is a refinement of an intermediate opaque I/O-automaton, known as TMS2. To this end, we develop a rely-guarantee approach for reducing the complexity of the proof. Proofs are mechanised in the interactive prover Isabelle.

We report on the analysis of gen_server, a popular Erlang library to build client-server applications. Our analysis uses a tool based on choreographic models. We discuss how, once the library has been modelled in terms of communicating finite state machines, an automated analysis can be used to detect potential communication errors. The results of our analysis suggest how to properly use gen_server in order to guarantee the absence of communication errors.

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.

No abstract available.

Abstract Data refinement in a state-based language such as Z is defined using a relational model in terms of the behaviour of abstract programs. Downward and upward simulation conditions form a sound and jointly complete methodology to verify relational data refinements, which can be checked on an event-by-event basis rather than per trace. In models of concurrency, refinement is often defined in terms of sets of observations, which can include the events a system is prepared to accept or refuse, or depend on explicit properties of states and transitions. By embedding such concurrent semantics into a relational framework, eventwise verification methods for such refinement relations can be derived. In this paper, we continue our program of deriving simulation conditions for process algebraic refinement by defining further embeddings into our relational model: traces, completed traces, failure traces and extension. We then extend our framework to include various notions of automata based refinement.

Efficient implementations of data structures such as queues, stacks or hash-tables allow for concurrent access by many processes at the same time. To increase concurrency, these algorithms often completely dispose with locking, or only lock small parts of the structure. Linearizability is the standard correctness criterion for such a scenario—where a concurrent object is linearizable if all of its operations appear to take effect instantaneously some time between their invocation and return. The potential concurrent access to the shared data structure tremendously increases the complexity of the verification problem, and thus current proof techniques for showing linearizability are all tailored to specific types of data structures. In previous work, we have shown how simulation-based proof conditions for linearizability can be used to verify a number of subtle concurrent algorithms. In this article, we now show that conditions based on backward simulation can be used to show linearizability of every linearizable algorithm, that is, we show that our proof technique is both sound and complete. We exemplify our approach by a linearizability proof of a concurrent queue, introduced in Herlihy and Wing's landmark paper on linearizability. Except for their manual proof, none of the numerous other approaches have successfully treated this queue. Our approach is supported by a full mechanisation: both the linearizability proofs for case studies like the queue, and the proofs of soundness and completeness have been carried out with an interactive prover, which is KIV.

No abstract available.

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 Despite being widely known and accepted in industry, the Z formal specification language has not so far been well supported by automated verification tools, mostly because of the challenges in handling the abstraction of the language. In this paper we discuss a novel approach to building a model-checker for Z, which involves implementing a translation from Z into SAL, the input language for the Symbolic Analysis Laboratory, a toolset which includes a number of model-checkers and a simulator. The Z2SAL translation deals with a number of important issues, including: mapping unbounded, abstract specifications into bounded, finite models amenable to a BDD-based symbolic checker; converting a non-constructive and piecemeal style of functional specification into a deterministic, automaton-based style of specification; and supporting the rich set-based vocabulary of the Z mathematical toolkit. This paper discusses progress made towards implementing as complete and faithful a translation as possible, while highlighting certain assumptions, respecting certain limitations and making use of available optimisations. The translation is illustrated throughout with examples; and a complete working example is presented, together with performance data.

Concurrent objects are inherently complex to verify. In the late 80s and early 90s, Herlihy and Wing proposed linearizability as a correctness condition for concurrent objects, which, once proven, allows us to reason about concurrent objects using pre- and postconditions only. A concurrent object is linearizable if all of its operations appear to take effect instantaneously some time between their invocation and return. In this article we define simulation-based proof conditions for linearizability and apply them to two concurrent implementations, a lock-free stack and a set with lock-coupling. Similar to other approaches, we employ a theorem prover (here, KIV) to mechanize our proofs. Contrary to other approaches, we also use the prover to mechanically check that our proof obligations actually guarantee linearizability. This check employs the original ideas of Herlihy and Wing of verifying linearizability via possibilities .

No abstract available.

Abstract Two styles of description arise naturally in formal specification: state-based and behavioural. In state-based notations, a system is characterised by a collection of variables, and their values determine which actions may occur throughout a system history. Behavioural specifications describe the chronologies of actions—interactions between a system and its environment. The exact nature of such interactions is captured in a variety of semantic models with corresponding notions of refinement; refinement in state based systems is based on the semantics of sequential programs and is modelled relationally. Acknowledging that these viewpoints are complementary, substantial research has gone into combining the paradigms. The purpose of this paper is to do three things. First, we survey recent results linking the relational model of refinement to the process algebraic models. Specifically, we detail how variations in the relational framework lead to relational data refinement being in correspondence with traces–divergences, singleton failures and failures–divergences refinement in a process semantics. Second, we generalise these results by providing a general flexible scheme for incorporating the two main “erroneous” concurrent behaviours: deadlock and divergence, into relational refinement. This is shown to subsume previous characterisations. In doing this we derive relational refinement rules for specifications containing both internal operations and outputs that corresponds to failures–divergences refinement. Third, the theory has been formally specified and verified using the interactive theorem prover KIV.

Retrenchment is a weakening of model based refinement that enables many development steps not expressible by refinement to be formally described nevertheless. The greater flexibility of retrenchment comes at the price of much feebler guarantees as compared with refinement, and so the interplay between retrenchment and refinement can hope to offer the best of both worlds. The paper explores the strategy of filtering the information in a retrenchment to yield a refinement under a suitable notion of observation. A general construction is given that enables a retrenchment, with its intrinsic notion of observability, to be filtered to produce a refinement with its intrinsic notion of observability. A simple running example illustrates the theory

No abstract available.

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.

This book describes theoretical results about AnsProlog * that have been obtained over the past decade.AnsProlog * or Prolog with Answer Sets 1 is a variation of the Prolog programming language, and extends the language by allowing clauses of the form:in the program.The L i 's are the literals (or atoms) of the Prolog language and may be supplied with a prefix ¬ sign, indicating the negation of a literal, while the prefix of not indicates negation as failure.Hence the semantics of the clause (C) may be read as follows: if all the literals L1, . . ., L m are true and all the literals L m+1 , . . ., L n can be safely assumed false then at least one of the literals L 1 , . . ., L k is true.(The actual semantics of each AnsProlog * program will be defined in terms of the Herbrand Universe of ground terms and the Herbrand Base of ground atoms.)The book takes the approach that the clause (C) is the most general form of a clause in the AnsProlog * language and so various subclasses of AnsProlog * can be defined by restricting this clause.For example: an AnsProlog -not program is when none of the clauses of a program contain the prefix not.In this respect, the book discusses the tractability, the complexity, the expressibility of the various subclasses of AnsProlog * based on the premise that AnsProlog * is both an excellent knowledge representation language and that it has a number of advantages over the Prolog language implementations based on SLDNF.For example, the ordering of goals within a clause and the ordering of clauses within a Prolog program affects whether a solution can or cannot be found (i.e. the program might get into an infinite loop); but not this is not the case within an AnsProlog * program.The reason being is that the semantics of an implementation of the AnsProlog * language can be thought of as allowing all models of the program to exist and then by using the clauses within the program, to impose restrictions on these models.The actual model(s) produced can then be interpreted in either a bi-valent (where a ground atom is either true or false) fashion or a tri-valent (where a ground atom is either true, false or unknown) fashion.The implementation algorithms describing how to restrict the models are described in Chapter 7 and two systems implementing the AnsProlog * language (and various subclasses), viz: (i) lparse+smodels and (ii) dlv are discussed in Chapter 8.The lparse+smodels program produces the stable models (or bi-valent) implementation, while the dlv produces the well-founded models (or tri-valent) implementation.Baral does note that both systems are under development and so implying that Chapter 8 may be out of date within a few years.However this aspect is compensated by Baral having a website www.baral.us/bookonewhere hypertext links to both the two systems and an errata/additional notes for the book are presented.On the application side, the book is peppered with many examples and simple programs illustrating the current point being made in the text.For example: how various forms of the 1 AnsProlog * is sometimes called A-Prolog in the literature.

Distributed system design is a highly complicated and non-trivial task. The problem is the characterised by the need to design multi-threaded, multi-processor, and multimedia systems. Design frameworks such as open distributed processing (ODP), the ITU/ISO standard, define a number of viewpoints from which the design of a distributed system should be approached. To use the framework, a design language for each of these viewpoints must be defined. This paper defines a computational viewpoint language based on the Unified Modelling Language (UML) and Component Quality Modelling Language (CQML). The use of this approach to provide the ODP viewpoint languages enables standard UML tools to be used as part of an ODP compliant design process; and in addition, it will potentially enable the use of Meta Object Facility (MOF) based generation tools for constructing tool support for our language.

Abstract Refinement in a concurrent context, as typified by a process algebra, takes a number of different forms depending on what is considered observable. Observations record, for example, which events a system is prepared to accept or refuse. Concurrent refinement relations include trace refinement, failures–divergences refinement, readiness refinement and bisimulation. Refinement in a state-based language such as Z, on the other hand, is defined using a relational model in terms of the input–output behaviour of abstract programs. These refinements are normally verified by using two simulation rules which help make the verification tractable. This paper unifies these two standpoints by generalising the standard relational model to include additional observable aspects. These are chosen in such a way that they represent exactly the notions of observation embedded in the various concurrent refinement relations. As a consequence, simulation rules for the tractable verification of concurrent refinement can be derived. We develop such simulation rules for failures–divergences refinement and readiness refinement in particular, using an alternative relational model in the latter case.

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.

Modern distributed systems include a class of applications in which non-functional requirements are important. In particular, these applications include multimedia facilities where real time constraints are crucial to their correct functioning. In order to specify such systems it is necessary to describe that events occur at times given by probability distributions; stochastic automata have emerged as a useful technique by which such systems can be specified and verified.However, stochastic descriptions are very general, in particular they allow the use of general probability distribution functions, and therefore their verification can be complex. In the last few years, model checking has emerged as a useful verification tool for large systems. In this article we describe two model checking algorithms for stochastic automata. These algorithms consider how properties written in a simple probabilistic real-time logic can be checked against a given stochastic automaton.

Abstract. This paper discusses the separation of components from the contexts in which they are used, and how this separation can be supported whilst using different specification languages. There are a number of ways in which this might be possible and here we show how the technique of promotion in Object-Z can be used to combine components which are specified using process algebras. We outline two approaches. The first is to separate out a single specification into a number of distinct viewpoints (i.e., partial specifications), each possibly written in a different notation. These viewpoints can be developed separately, but combined if necessary by a process of translation and unification. The alternative approach we discuss is to use a single hybrid language which is composed of a combination of notations, which we illustrate here by combining CSP and Object-Z. We illustrate both approaches with a simple example, and also consider how such component-based descriptions can be refined, which involves addressing the question of compositionality.

It is now well recognized that the next generation of distributed systems will be distributed multimedia systems. Central to multimedia systems is quality of service, which defines the non-functional requirements on the system. In this paper we investigate how stochastic process algebra can be used in order to determine the quality of service properties of distributed multimedia systems. We use a simple multimedia stream as our basic example. We describe it in the stochastic process algebra PEPA and then we analyse whether the stream satisfies a set of quality of service parameters: throughput, end-to-end latency, jitter and error rates.

The 'viewpoint' approach, in which a system is described by several partial specifications, has been proposed as a way of making complex computing systems more understandable. The ISO's Open Distributing Processing (ODP) framework is an architecture for open distributed systems, involving five named viewpoints. This paper compares two partial specifications of a lending library-from the ODP's Enterprise and Information Viewpoints-and discusses the relation between them. Both specifications are written in Object-Z, an object-oriented variant of Z. Examining how such partial specifications might be unified raises broader issues of refinement and mutual consistency of partial specifications in Object-Z.

Data refinements is a well established technique for transforming specifications of abstract data types into ones which are closer to an eventual implementation. The conditions under which a transformation is a correct refinement can be encapsulated into two simulation rules: downward and upward simulations. These simulations are known to be sound and jointly complete for boundedly-nondeterministic specifications. In this note we derive a single complete refinement method and show how it may be formulated in Z, this is achieved by using possibility mappings. The use of possibility mappings themselves is not new, our aim here is to reformulate them for use within the Z specification language.

Object-based distributed computing is now a well established technique for constructing large, heterogeneous computing and telecommunications systems. Indeed, standards bodies and consortia such as, ITU, ISO, OMG, TINA-C, etc., have all defined distributed object-based frameworks as a foundation for open distributed computing.

The open distributed processing (ODP) standardisation initiative has led to a framework by which distributed systems can be modelled using a number of viewpoints. These include an enterprise viewpoint, which focuses on the objectives and policies of the enterprise that the system is meant to support. Although the ODP reference model provides abstract languages of relevant concepts, it does not prescribe particular techniques that are to be used in the individual viewpoints. In particular, there is a need to develop appropriate notations for ODP enterprise specification, in order to increase the applicability of the ODP framework. In this paper, we tackle this concern and develop a specification language to support the enterprise viewpoint. In doing so, we focus on the expression of enterprise policies that govern the behaviour of enterprise objects. The language we develop is a combination of structured English and simple predicate logic, and is built on top of the formal object-oriented specification language Object-Z. We illustrate its use with a case study that presents an enterprise specification of a library support system.

A specification provides a concise description of a system, and can be used as both the benchmark against which any implementation is tested, and also as a means to generate tests. Formal specifications have potential advantages over informal descriptions because they offer the possibility of reducing the costs of testing by automating part of the testing process. This observation has led to considerable interest in developing test generation techniques from formal specifications, and a number of different methods have been derived for state-based formalisms such as Z, B and VDM. However, after tests have been derived from a formal specification, the specification might be refined further before it is implemented, and therefore a mechanism is needed to relate the abstract tests to the refined implementation. The purpose of this paper is to provide such a method by exploring the relationship between testing and refinement. In this paper a model for test generation is used which constructs a finite state machine (FSM) from a Z specification by using a Disjunctive Normal Form (DNF) partition analysis of the state and operations. The finite state machine is then used to derive suitable test suites. The paper decribes a way of calculating an FSM for a refinement from an abstract FSM together with the information about the refinement embodied in the retrieve relation. This means that it is possible to test an implementation by generating a new concrete finite state machine from a set of abstract tests. Copyright © 1999 John Wiley & Sons, Ltd.

Abstract. An important aspect in the specification of distributed systems is the role of the internal (or unobservable) operation. Such operations are not part of the interface to the environment (i.e. the user cannot invoke them), however, they are essential to our understanding and correct modelling of the system. In this paper we are interested in the use of the formal specification notation Z for the description of distributed systems. Various conventions have been employed to model internal operations when specifying such systems in Z. If internal operations are distinguished in the specification notation, then refinement needs to deal with internal operations in appropriate ways. Using an example of a telecommunications protocol we show that standard Z refinement is inappropriate for refining a system when internal operations are specified explicitly. We present a generalisation of Z refinement, called weak refinement, which treats internal operations differently from observable operations when refining a system. We discuss the role of internal operations in a Z specification, and in particular whether an equivalent specification not containing internal operations can be found. The nature of divergence through livelock is also discussed.

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.

No abstract available.

No abstract available.