Simulating truly concurrent CSP

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. However 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 construction that splits events into start and end events and monitors the result in a manner faithful to the original process. The method is applied to determine pairs of possibly concurrent events and to compute maximal simultaneity in a CSP design. © 2011 Springer-Verlag Berlin Heidelberg.