Simulating Truly Concurrent CSP - Formal Methods: Foundations and Applications - page 128

Simulating Truly Concurrent CSP

Moritz Kleine 1 and J.W. Sanders 2

1 Software Engineering Group
Technische Universitat Berlin, Germany
2 International Institute for Software Technology
United Nations University, Macao SAR China

Abstract. Process algebras like CSP provide a convenient intermediate-
level formalism for the design of concurrent systems by allowing
processes to be combined in parallel in such a way that the designer
abstracts synchronization mechanisms and simultaneity of events. How-
ever some purposes require potential simultaneity to be made explicit.
One approach is to produce new semantics models encapsulating that
information. The approach taken here is to use the standard models
and the CSP tool, FDR, to simulate a process in such a way to reveal
potentially-simultaneous events. The simulation is achieved by a con-
struction that splits events into start and end events and monitors the
result in a manner faithful to the original process. The method is ap-
plied to determine pairs of possibly concurrent events and to compute
maximal simultaneity in a CSP design.

1 Introduction

Process algebras, like CSP [4,9], allow synchronizing processes to be combined
in parallel with the result that the system designer need not be concerned about
exploiting simultaneity, which may arise naturally in an implementation con-
forming to the design. But sometimes, for example for purposes of simulation, it
is useful to know what potential simultaneity a design embodies, and then the
abstraction carefully built in to the process algebra must be revoked.
The purpose of this paper is to study one way to make explicit the simul-
taneity of events implicit in a CSP process. Events were designed in CSP to
be instantaneous, on the understanding that duration can then be modelled by
splitting an event into start and end events. Our approach starts by unravelling
that assumption, and proceeds by constructing a faithful, controlled simulation
of the process. The construction is shown to be faithful in the sense that the
simulated version equals the original process in the traces semantics. The ap-
proach is shown at work on three small but typical examples. It is defined for a
subset of CSP M [10] for subsequent analysis with FDR [9] or ProB [8]. Although
our approach is not limited to finite-state processes, applications here are to
finite-state processes analyzed using FDR or ProB.
Several applications of the approach are discussed. For purposes of motivation,
observe that CSP events, being instantaneous, abstract the actions or whole proce-
dures of a lower-level programming language. Of course the advantage is simplicity