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

the first e after each non-empty sequence of s events are exactly the steps in
their semantics. The present approach, like the step-failures semantics, can be
used to optimize applications at runtime by predicting maximal parallelism. It
also takes into account duration of user-defined functions related to events.
The language considered here overlooks several useful derived operators, like
chaining , interleaving , interrupt ,and linked parallel (a generalization of chain-
ing), which are subject to future work. Of those, interrupt is especially interest-
ing, because the interpretation of an event heavily influences its transformation
by T . The issue is whether or not a single event x that is split into two events
s . x , e . x may be aborted. If a single event can be aborted, the event can no
longer be interpreted as an action or function that transforms some state into a
well-defined successor state. Furthermore, it would violate the e -non-refusability
property (2). If a single event cannot be aborted, the transformed interrupt
must take care of unfinished events, which renders the transformation reasonably
complicated.
It is planned to realize interleaving according to the deparallelize operator
proposed by Taubner and Vogler in [12]: P

||| Q corresponds to P A Q where

A conc ( P A Q ).

Another interesting issue is the extraction of concurrency in different ways.
The method described here uses FDR to perform this by modifying the con-
troller and checking whether or not the modified version violates the equality or
querying fresh non-conflicting events. Unfortunately, FDR does not perform very
well on such assertions because the bags grow rapidly and the functional part
of CSP M does not provide the most ecient way to model a process for analysis
with FDR. One possible solution is to implement a specialized procedure that
works on the original process P , to compute conc ( P ). This procedure could be
an extension of FDR's procedure to compute the traces of P that performs the
transformation as well as synchronization with the controller internally before
computing the traces.
It might be worthwhile to try the approach with the CSP prover [5], in view
of the performance penalty caused by the controller process (see 6.3).

⊆ Σ and A is an operator ensuring ∀ x , y : A · ( x , y ) / ∈

8Con lu on

In this paper a construction has been given to replace each process with an equiv-
alent version explicitly realising the possibility of concurrency. The controller C
synchronizes with the transformed process. It maintains a bag X whose contents
represent the events of the original process that are possibly concurrent after the
trace that has lead to the current state. Thus it can be used in various ways to
query concurrency information of a process.
In Example 6.1 the controller process C 1 of Definition 2 was used to emit the
recorded concurrency information using a fresh event. That example has also
demonstrated application of our approach with ProB.
The concurrency information can also be exploited using guards. A very simple
application has been shown in the one-place-buffer example 6.2. Limiting the bag