INTRODUCTION

One can speak of Computer Integrated Manufacturing (CIM) if the computer is used in all phases of the production of some industrial product. In this paper we will focus on the design of the product-flow and the information-flow, which occurs when products are actually produced. Topics like product-development, marketing and management are beyond the scope of this paper. The technique used in this paper is based on a theory for concurrency, called process algebra (see or). It can be used to describe the total phase of manufacturing, from the ordering of raw materials up to the shipping of the products which are made from this materials. During this process many machines are used, which can operate independently, but often depend on the correct operation of each other. Providing a correct functioning of the total of all machines, computers and transport-services is not a trivial exercise. Before actually building such a system (a CIM-architecture) there must be some design. Such a specification, when validated, describes a properly functioning system.

INTRODUCTION

At this moment there are a lot of programming languages which offer facilities for concurrent programming. The basic notions of some of these languages, for example CSP, occam and LOTOS, are rather close to the basic notions in ACP, and it is not very difficult to give semantics of these languages in the framework of ACP. Milner showed how a simple high level concurrent language can be translated into CCS. However, it is not obvious at first sight how to give process algebra semantics of more complex concurrent programming languages like Ada, Pascal-Plus or POOL. This is an important problem because of the simple fact that a lot of concurrent systems are specified in terms of these languages. In this article we will tackle the problem, and give process algebra semantics of the language POOL.

INTRODUCTION

Extension of process algebra

In this paper we extend process algebra with a new operator that will be helpful to describe process creation. From a methodological point of view the extension of process algebra with new operators is just the right way to incorporate new features. Only in a very rich calculus with many operators one may hope to be able to perform significant algebraic calculations on systems. In many cases a new feature requires new (additional) syntax and more equations, only in very rare circumstances the addition of equations alone suffices to obtain an appropriate model of some new system aspect. The core system ACP, see, describes asynchronous cooperation with synchronous communication.

On top of ACP various features can be added, for instance: asynchronous communication, cooperation in the presence of shared data, broadcasting, interrupts. This note adds process creation to the features that are compatible with process algebra.

For historical remarks and relations with previous literature we refer to.

Process creation

We start on basis of the axiom system ACP which is supposed to be known to the reader. We assume the presence of a finite set of data D and introduce for each d∈D an action cr(d). The action cr(d) stands for: create a process on basis of initial information d. Let cr(D) denote the set {cr(d)|d∈D}.

INTRODUCTION

Many authors have studied the concurrency aspects of sorting, and indeed the n-time bubblesort algorithm (using n processors) is rather thoroughly analyzed already (e.g. see: Hennessy, Kossen and Weijland). However, bubblesort is not the most efficient sorting algorithm in sequential programming, since it is n2-time and for instance heapsort and mergesort are n log n-time sorting algorithms. So, the natural question arises whether it would be possible to design an algorithm using even less than n-time.

In this paper we discuss a concurrent algorithm, capable of sorting n numbers in O(log n) time. This algorithm is based on the idea of square comparison: putting all numbers to be sorted in a square matrix, all comparisons can be made in O(1) time, using n2 processors (one for each cell of the matrix). Then, the algorithm only needs to evaluate the result of this operation.

The algorithm presented here, which is called ranksort, is not the only concurrent time-efficient sorting algorithm. Several sub n-time algorithms have been developed by others (see: Thompson).

One of the basic problems in protocol verification is the following: data are to be transmitted from A to B via some unreliable medium M. A protocol has been proposed for doing so correctly and perhaps efficiently. A rigorous mathematical proof of the correctness claim is desired.

Now protocol verification aims at providing the techniques for giving such a proof. Several formalisms have been advocated, but as yet none has been widely accepted.

The framework we adhere to is process algebra. The first protocol correctness proof by means of process algebra is in Bergstra and Klop, where a simple version of the Alternating Bit Protocol is verified.

We have tried our hands at a more complicated version, called the Concurrent Alternating Bit Protocol (CABP) and found that the number of possible state transitions was prohibitively large. In this article we propose a divide-and-conquer strategy. We group processes into modules, describe and verify their behaviour and finally combine them. For different approaches, see.

In Section 1 we deal with the Concurrent Alternating Bit Protocol (CABP). In Section 2 we present the modular approach. Modules are introduced in Section 3, whereas the verification of the CABP is given in Section 4.

It has been observed that formal verification methods for mathematical proofs, computer programs, communication protocols and the like are usually illustrated by ‘toy’ examples and that such proofs tend to be discouragingly long. In order to demonstrate that it is feasible to verify a ‘real-life’ communication protocol by means of process algebra, we picked one from the literature.

In his Ph.D. thesis, Mullender investigates issues he considered while developing the Amoeba distributed operating system. In Section 3.2.4 of a transaction protocol is described to which we will refer as the Amoeba protocol. In the preceding sections of the design goals are described that this protocol is supposed to satisfy. He does not give a formal verification that his protocol meets this criteria. In fact, it turns out that one of them is not met. Note that this only applies to the simplified version of the protocol that appears in, the actual implementation uses a much more complicated version in which this mistake is not found.

Section 1 of this article gives the minimum background information necessary for understanding the rest of the article.

In Section 2 the design goals are formulated in English and in terms of process algebra.

INTRODUCTION

In this article we will present simple descriptions of so-called systolic systems. Such systems can be looked at as a large integration of identical cells in such a way that the behaviour of the total system strongly resembles the behaviour of the individual cells. In fact the total system behaves like one of its individual cells ‘on a larger scale’.

For example one can think of a machine sorting arrays of numbers with a certain maximum length. Suppose we need a machine handling arrays that are much longer. A typical ‘systolic approach’ to this problem would be to try to interconnect the smaller machines such that the total circuit sorts arrays of a greater length. As a matter of fact this specific example will be worked out in the following sections. In designing VLSI-circuits (short for very large scale integrated circuits) it is very useful, if not necessary, to construct the specific circuit by placing simple components in regular configurations. Otherwise one looses all intuition about the behaviour of the circuit that is eventually constructed.

INTRODUCTION

We are interested in the verification of distributed systems by means of algebraic manipulations. In process algebra, verifications often consist of a proof that the behaviour of an implementation IMPL equals the behaviour of a specification SPEC, after abstraction from internal activity: τI(IMPL) = SPEC.

The simplest strategy to prove such a statement is to derive first the transition system (process graph) for the process IMPL with the expansion theorem, apply an abstraction operator to this transition system, and then simplify the resulting system to the system for SPEC using the laws of (for instance) bisimulation semantics. This ‘global’ strategy however, is often not very practical due to combinatorial state explosion: the number of states of IMPL can be of the same order as the product of the number of states of its components. Another serious problem with this strategy is that it provides almost no ‘insight’ in the structure of the system being verified.

This article serves as an introduction to the basis of the theory, that will be used in the rest of this book. To be more precise, we will discuss the axiomatic theory ACPT (Algebra of Communicating Processes with abstraction), with additional features added, which is suitable for both specification and verification of communicating processes. As such, it can be used as background material for the other articles in the book, where all basic axioms are gathered. But we address ourselves not exclusively to readers with previous exposure to algebraic approaches to concurrency (or, as we will call it, process algebra). Also newcomers to this type of theory could find enough here, to get started. For a more thorough treatment of the theory, we refer to, which will be revised, translated and published in this CWI Monograph series. There, most proofs can also be found; we refer also to the original papers where the theory was developed. This article is an abbreviated version of reference.

Our presentation will concentrate on process algebra as it has been developed since 1982 at the Centre for Mathematics and Computer Science, Amsterdam (see), since 1985 in cooperation with the University of Amsterdam and the University of Utrecht. This means that we make no attempt to give a survey of related approaches though there will be references to some of the main ones.

This paper is not intended to give a survey of the whole area of activities in process algebra.

We acknowledge the help of Jos Baeten in the preparation of this paper.

In this book, we give applications of the theory of process algebra, known by the acronym ACP (Algebra of Communicating Processes), as it has been developed since 1982 at the Centre for Mathematics and Computer Science, Amsterdam (see), since 1985 in cooperation with the University of Amsterdam and the University of Utrecht. An important stimulus for this book was given by the ESPRIT contract no. 432, An Integrated Formal Approach to Industrial Software Development (Meteor). The theory itself is treated in, which will be revised, translated and published in this series. The theory is briefly reviewed in the first article in this book, An introduction to process algebra, by J.A. Bergstra and J.W. Klop.

This book gives applications of the theory of process algebra. By the term process algebra we mean the study of concurrent or communicating processes in an algebraic framework. We endeavour to treat communicating processes in an axiomatic way, just as for instance the study of mathematical objects as groups or fields starts with an axiomatization of the intended objects. The axiomatic method which will concern us, is algebraic in the sense that we consider structures which are models of some set of (mostly) equational axioms; these structures are equipped with several operators. Thus we use the term ‘algebra’ in the sense of model theory.

Introduction

In this chapter we present and discuss examples of the syntactic and translation rules of the QE-III fragment whose definition was given in Chapter 6. As we pointed out in that presentation, the PTQ fragment stands essentially intact as the core of QE-III. There are, however, certain changes to this core. One major change is our use of the logic ILs as the intermediate translation language; this logic is a modification to Montague's IL, and makes explicit the hidden abstraction over indices that is a part of the evaluation process in Montague's PTQ analysis. In defining ILs we have already shown that we evaluate any expression α with respect to a state s by forming the expression: [λiα](s).

Moreover, in presenting the pragmatics of QE-III, we showed how the pragmatic interpretation of any sentential expression was essentially given by the denotation of the expression formed by λ-abstracting over all of the free individual variables and also evaluating with respect to now.

In addition to this change in the underlying logic and method of evaluation, the following additional modifications have been made to the rules of the PTQ fragment:

1. Rule S4 has been modified to perform the single function of combining a Term with an IV to form a sort of proto-sentence. It no longer performs the verb inflection for third person singular present tense. The entire treatment of tense and time adverbials is now performed more systematically by rules S101 through S106. (The tensing functions of S17 have therefore been totally eliminated.)

2. […]

Introduction

In the previous chapters of this book we have presented the historical relational database model HRDM as a means of formally incorporating a temporal semantics into the relational database model. We now turn our attention to the problem of providing a semantics for querying an hrdb using natural language, specifically English. Our method will be to define the semantics of queries expressed in English in terms of the semantics of the HRDM model already presented by defining a small query fragment as a Montague Grammar (as in [Mon73], henceforth PTQ.) The correlation between the database semantics we have already defined and this query language will be made explicit by providing the semantics of the query fragment via an indirect translation into the intensional logic ILs. The translations will provide for a completely extensional treatment of verbs, (i.e., there will be no verbs like “seek” which can be nonextensional in object position in the PTQ treatment). This treatment is dictated by the application of the Montague Semantics approach to a database environment, in which existence is tantamount to existence in the database. Through these translations, then, the model for ILs that we defined as induced by the database will also serve as the model for a formal definition of the semantics of the English queries. In addition to providing a semantic interpretation, which in model-theoretic terms is called its denotation, we also provide for each expression a pragmatic interpretation in a manner to be explained.