INTRODUCTION

In this chapter we will focus on the specification language used throughout this book: PSF (Process Specification Formalism). We will discuss the mathematical origins of PSF as well as its syntax and semantics. The language itself will be clarified by using a running example, which gets more complicated as new language features are introduced. Apart from giving specifications in PSF we will also describe the implementations that make up the so-called PSF-Toolkit, such as the term rewriting system and the simulator.

The PSF-Toolkit also embodies a collection of frequently used specifications in the form of the PSF standard library. In this chapter we will explain which modules are part of the library and how they can be used. A full listing of the relevant modules from the PSF standard library can be found in Appendix A.

ACP

Before we turn our attention to PSF, we will give some information on ACP (Algebra of Communicating Processes). ACP is the theoretical foundation for the process part of PSF, and deserves some explanation as such.

The development of ACP was started in 1982 by J.A. Bergstra and J.W. Klop, at the Centre for Mathematics and Computer Science in Amsterdam. Compared with other concurrency theories like CCS, CSP and Petri Nets, ACP is most closely allied to CCS. The main difference between ACP and the other approaches is the way in which the semantics is treated.

Most formalisms, like CCS, CSP and Petri Nets are based on one specific model of concurrency. ACP, however, is a theory based on algebraic methods. The theory is defined by a set of axioms.

INTRODUCTION

In this chapter specifications of three simple protocols are given in the formalism of PSF. The main goal is to make the reader familiar with the way the formal description technique PSF can be used for the specification of communication protocols. For this reason we specify protocols which are, in technical terms, not hard to understand.

The communication protocols specified in this chapter are the Alternating Bit Protocol (ABP), the Positive Acknowledgement with Retransmission Protocol (PAR-Protocol), and the Concurrent Alternating Bit Protocol (CABP), which is a more complicated version of the ABP.

The three protocols have in common that they follow a simplex scheme, which means that there is only one sender and one receiver and that the data flows in one direction. Moreover, the protocols handle just one data element at a time. These two restrictions make the protocols behave externally as one-element buffers.

The simple protocols considered have an interesting history in the theories of concurrency. Many different specifications and verifications can be found in the literature. Our specifications of the simple protocols are based on existing specifications in ACP that were made for mathematical analysis.

The ABP as specified in this chapter has been verified algebraically in the formalism of ACP. The PAR-Protocol has also been specified and verified by means of ACP but a special operator was needed to specify some restrictions on the communication between the timer process and the sender process: the priority operator. We present a version without priorities which is very similar to this specification. This is because priorities cannot be specified in PSF.

SIGNALS

When describing the behaviour of a real-time process, we may wish to include instantaneous observable events that are not synchronisations. These signals may make it easier to describe and analyse certain aspects of behaviour, providing useful reference points in a history of the system. For example, an audible bell might form part of the user interface to a telephone network, even though the bell may ring without the cooperation of the user. This is incompatible with our existing view of communication.

In some cases, suitable environmental assumptions will allow us to describe such behaviour within the existing timed failures model. However, if we intend that these signals should be used to trigger other events or behaviours, then we must extend our semantic model to include an element of broadcast communication: some output events may occur without the cooperation of the environment.

In our model, signal events will occur as soon as they become available, and will propagate through parallel combination. A process may ignore any signal â performed by another process, unless it is waiting to perform the corresponding synchronisation a. If this is the case, then both â and a will occur. Of these, only the signal will be observed outside the parallel combination; it makes no sense to propagate a synchronisation.

REAL-TIME SYSTEMS

As computing devices become faster and more powerful, we find ourselves increasingly dependent upon systems which are difficult to understand and prone to failure. The failure of a commercial banking system or a company database may be expensive and inconvenient. The failure of an aircraft control system or a railway signalling network may result in injury or death. As the consequences of system failure become ever more severe, we must find ways to make these applications of computing technology safer and more reliable.

Over the past twenty-five years, mathematical techniques have been developed for the specification and implementation of computing systems. Formal methods have been used in the design and analysis of transformational systems—in which results are computed from a given set of inputs—and have been shown to reduce design costs and improve reliability. However, many of the systems in which safety is a primary concern are real-time systems, and cannot easily be viewed in a transformational setting.

Real-time systems maintain a continuous interaction with their environment and are often subject to complex timing constraints. They may also be required to perform several tasks concurrently. To reason about such systems we require a mathematical formalism that supports a treatment of timed concurrency. In this thesis we explore and extend one such formalism, the theory of Communicating Sequential Processes, first introduced by Hoare (1985).

OTHER APPROACHES

A wide variety of formal methods have been proposed for the specification and development of real-time systems, based upon process algebras, temporal logics, and timed programming languages. Although much research has been carried out, a consensus has yet to emerge concerning the applicability of the various formalisms to different types of system. A successful development method is likely to involve some combination of the features mentioned above. A notation that is well-suited to requirements capture is unlikely to be an efficient programming language, and vice versa.

Quantitative Temporal Logics

Hooman and Widom (1989) present a compositional proof system relating an occam-like language to a quantitative temporal logic, similar to the one developed by Koymans and de Roever (1983). Although the system description language is somewhat limited, it is clear that quantitative temporal logics are useful assertion languages; Jackson (1990) shows how such a logic may be employed as a specification language for timed CSP. It would be interesting to see the proof system applied in the development of a large, complex system.

Shasha et al. (1983) use a quantitative temporal logic to prove the correctness of a carrier-sense broadcast protocol, similar to the one described in chapter seven. By assuming a simplified version of the service provided by the physical layer, and an internal specification of the data link layer, the authors are able to establish that certain desirable properties hold of the network.

ABSTRACTION

If we wish to produce a readable specification of a large system, then we must take care to present our description in a clear, structured fashion. At each level of abstraction, we identify the interfaces between system components and conceal any events which are not of interest. We express our specification as a series of service specifications, each describing the service provided by a particular component of the system. In this way, we may refine a description of the service provided by a system towards a satisfactory implementation.

The hiding operator provides the mechanism for abstraction in timed CSP; the expression P\ A denotes a process that behaves as P, except that

• events from A occur as soon as they become available

• only events from outside A are observed

In section 5.2.8 we gave an inference rule for this operator that was easy to derive, but difficult to apply. We can achieve a significant reduction in complexity if we separate the concerns of concealment and scheduling. To this end, we define a predicate actA which holds of any A-active behaviour:

Definition 6.1 actA(s, X) ≙ [0, end(s, X)) × A ⊆ X

A behaviour (s, X) is A-active if all events from set A occur as soon as they become available. If we wish to establish that P\A satisfies a specification S(s, X), it is sufficient to show that

• S(s, X) holds for all of the A-active behaviours of P

• S(s, X) is unaffected by the concealment of events from A

The second condition is satisfied if the truth of the specification is unaffected by the removal of A's events from the trace and refusal.

A LOCAL AREA NETWORK PROTOCOL

To illustrate the application of timed CSP to the specification of real-time systems, we will show how the functions presented in chapter 6 may used to describe the behaviour of a communications protocol at two different levels of abstraction. The protocol chosen for this purpose is based upon the Ethernet communication protocol, a standard protocol for local area networks.

The Ethernet protocol is a broadcast protocol: signals sent by one station may reach all of the stations upon the network. It is a carrier-sense protocol: stations listen for a carrier signal on the broadcast medium and act accordingly. Another important feature is collision detection. Each station must monitor the broadcast medium during transmission, and cease immediately if it becomes apparent that another station is also transmitting.

The protocol specification is divided into two parts, corresponding to the data link and physical layers of the ISO reference model described by Tanenbaum (1981). This model consists of seven layers, each representing a different level of abstraction, from the hardware of the physical layer to the user software of the application layer. Each layer provides a service to the layer above, facilitating virtual communication between peer processes on different machines. In this chapter, we will concern ourselves with the bottom three layers of the model: the communication subnet of figure 7.1.

The physical layer is the lowest layer in the model hierarchy, and transmits data as bits between the stations, or nodes of the network.