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

6Examp s

In this section the approach is applied to three examples: (a) the example used to
motivate [7]; (b) a one-place buffer from [3]; and (c) a modification of the dining
philosophers from [3]. Due to technical limitations of ProB and FDR, the typing
and naming scheme used in the example scripts (see [6]) differ slightly from the
models presented here. For example, the controller maintains a list instead of a
bag because CSP M has no support for bags built-in.

6.1 Choice versus Concurrency

Consider the processes

P = a → b → STOP b → a → STOP

Q = a → STOP | ∅ | b → STOP .

Evidently P = Q , although the latter offers concurrency of a and b not allowed
by the former. That is revealed using our technique as follows.
By the definition of T ,

T ( P )= s . a → e . a → s . b → e . b → STOP s . b → e . b → s . a → e . a → STOP

T ( Q )= s . a → e . a → STOP | ∅ | s . b → e . b → STOP .

To use FDR we define

SPEC = x : { [[ ]] , [[ a ]] , [[ b ]] }• co . x → SPEC .

Now Ext ( P )= P and Ext ( Q )= Q but using Ext 1 (see the explanation of
definition 2)

SPEC T Ext 1 ( P ) \{ a , b }

while

.
The trace generated by FDR leading to the violation of the second refinement
relation, namely

T \{

a , b

}

SPEC Ext 1 ( Q )

,
reveals that the events a and b might occur simultaneously in Q but not in P .
The same result can be obtained using the LTL model checking capabilities
of ProB. We introduce the fresh event conc a b and define

co . [[ ]] , co . [[ b ]] , co . [[ a , b ]]

F ( P )= P [ co . [[ a , b ]] ← conc a b ]

to check if

φ = G not [conc a b]
holds on F ( Ext 1 ( P )) or F ( Ext 1 ( Q )). Expectedly ProB shows

F ( Ext 1 ( P )) | = φ

F ( Ext 1 ( Q )) | = φ.