=Paper=
{{Paper
|id=Vol-1269/paper1
|storemode=property
|title=XCCS Diagram to CCS Script Conversion Algorithm
|pdfUrl=https://ceur-ws.org/Vol-1269/paper1.pdf
|volume=Vol-1269
|dblpUrl=https://dblp.org/rec/conf/csp/Balicki14
}}
==XCCS Diagram to CCS Script Conversion Algorithm ==
https://ceur-ws.org/Vol-1269/paper1.pdf
1
XCCS diagram to CCS script Conversion Algorithm
Krzysztof Balicki
Interdisciplinary Centre for Computational Modelling
University of Rzeszów
Pigonia 1, 35 - 310 Rzeszów, Poland
kbalicki@ur.edu.pl
Abstract. The XCCS modelling language can be viewed as a tool supporting fast
and faultless development of CCS scripts or as an independent process calculus
based on CCS process algebra. Having in mind the first of possible applications,
we present an algorithm that converts XCCS diagrams into CCS scripts. This
algorithm takes into consideration the priority of actions in the XCCS diagram
and aims to retain the maximum number of original action’s names for the sake
of readability.
1 Introduction
The XCCS (eXtended Calculus of Communicating Systems) modelling language was
formally defined in the paper [1] as a graphical extension of the Milner CCS ([2], [3],
[4], [5]) process calculus. It has has been developed to replace the algebraic coding of
concurrent systems with graphical modelling.
XCCS models consist of two layers, a graphical and an algebraic one. In the latter
we use the subset of CCS process algebra called CSS (Calculus of Sequential Systems)
to describe behaviour of individual agents. CSS scripts may only contain the prefix op-
erator ".", the choice operator "+" and parentheses "( )". Moreover, in the timed version
of the calculus, the strong choice operator "++" and the delay operator "$" are allowed.
The composition, restriction and relabel operators have graphical representations and
provide simple description of the modelled system structure [1], [6], [7].
In the paper [1] we introduced simple Basic Conversion Algorithm which is proper
for plain XCCS modelling language. The new Universal Conversion Algorithm pre-
sented here can be applied to both plain and full XCCS diagrams. Furthermore, it con-
siders the priority of actions and aims to retain the maximum number of original action’s
names for the sake of readability. First, we show Trivial Conversion Algorithm that does
not perform any relabelling of actions yet works correctly for limited class of models.
Then, we thoroughly examine and define the properties of those diagrams that cannot
be translated by Trivial Conversion Algorithm. We take into account these properties
while applying proper relabeling of actions in the new algorithm.
2 Preliminaries
We recall XCCS modelling language by way of example. Let us consider a simple
XCCS diagram.
1
2
B1 B2
A a c B
b b
A = a.'b.A; B = b.'c.B;
Fig. 1. Example XCCS diagram
The formal definition of the XCCS diagram in Fig. 1 is as follows:
XCCS = (B, CA, CSS , CR, in, out, v, ρ), where:
· B = {B1 , B2 } - agent blocks
· CA = {a, b, c} - communication actions, labels
· CSS = {A = a.b.A, B = b.c.B} - the set of CSS scripts
CA
· in : B → 2 - input ports assigment
in(B1 ) = {a}, in(B2 ) = {b} - labels of input ports
· out : B → 2CA - output ports assigment
out(B1 ) = {b}, out(B2 ) = {c} - labels of output ports
OutP = {(B1 , b), (B2 , c)} = {B1 .b, B2 .c} - output ports
InP = {(B1 , a), (B2 , b)} = {B1 .a, B2 .b} - input ports
· CR ⊆ OutP × InP - communication relation
CR = {((B1 , b), (B2 , b))} = {B1 .b → B2 .b} - connected ports
· ϑ : OutP ∪ InP = P → {v, i} - visibility function
ϑ(B1 .a) = ϑ(B2 .c) = v - visible ports
ϑ(B1 .b) = ϑ(B2 .b) = i - invisible ports
· ρ : B → CSS , ρ(B1 ) = A, ρ(B2 ) = B - assigment of CSS scripts
The above XCCS diagram can be converted to the following CCS script by the
Trivial Conversion Algorithm that does not perform any relabelling of actions.
E = (B1 |B2 )\{b}
B1 = a.b.B1
B2 = b.c.B2
Please note that the symbols ’b on the diagram and b in the script denote the same
co-action with the name b. We will use the following notations and definitions:
A(CSS i ) is the set of all actions of the CSSi script, e.g. A(B) = {b}
A(CSS i ) is the set of all co-actions of the CSSi script, e.g. A(B) = {c}
K(CSSi ) is the set of all agent constants of the CSSi script, e.g. K(B ) = {B}
2
3
Definition 1. We define the synchronization relation SR as follows:
a) Let CR be a communication relation. For any port p ∈ P we define the set:
CR(p) = {x ∈ P : (x, p) ∈ CR ∨ (p, x) ∈ CR}. (1)
If p ∈ OutP , then the set CR(p) contains all input ports connected with the port p.
If p ∈ InP , then the set CR(p) contains all output ports connected with the port p.
b) We define a mapping:
P {p} if CR(p) = ∅
SR : P → 2 , SR(p) = S (2)
CR(p) ∪ x∈CR(p) CR(x) if CR(p) 6= ∅
c) The synchronization relation SR is set by SR mapping:
def
(p1 , p2 ) ∈ SR ⊆ P × P ⇐⇒ SR(p1 ) = SR(p2 ). (3)
If an equivalence class contains only one port then this port is isolated and does not
communicate with any other port. If an equivalence class contains more then one port
then any two complementary ports belonging to the equivalence class are connected
one with the other. For the XCCS diagram in Fig.1 the equivalence classes of SR
relation are P /∼ = {{B1 .a}, {B1 .b, B2 .b}, {B2 .c}}.
We will use the following symbols:
V = {p ∈ P : ϑ(p) = v} - the set of all visible ports
I = {p ∈ P : ϑ(p) = i} - the set of all invisible ports
Iso = {p ∈ P : CR(p) = ∅} - the set of all isolated ports
Int(Bi ) = {a : a ∈ A(ρ(Bi )) ∧ Bi .a ∈
/ InP } - the set of all inner actions of block Bi
Int(Bi ) = {a : a ∈ A(ρ(Bi )) ∧ Bi .a ∈
/ OutP } - the set of all inner co-actions of block Bi
[
Int = Int(Bi ) - the set of all inner actions of the diagram
Bi ∈B
[
Int = Int(Bi ) - the set of all inner co-actions of the diagram
Bi ∈B
3 Conflicts and Shadows
We require that the resulting CCS script for a given XCCS diagram is in a Standard
Concurrent Form and preserves properties of the diagram, that means:
1. Synchronization may occur only between those pairs of actions and co-actions
which correspond to the labels of the ports connected on the diagram.
2. Actions and co-actions which correspond to inner actions are executable.
3. Actions and co-actions which correspond to visible isolated ports are executable.
4. Actions and co-actions which correspond to invisible isolated ports are not exe-
cutable.
3
4
Now we roughly describe the Trivial Conversion Algorithm:
1. The names of CSS scripts become the same as names of corresponding blocks.
2. The ambiguities of names of the agent constants in CSS scripts are eliminated.
3. Output CCS script is a Standard Concurrent Form of all modified CSS scripts.
4. In the restriction set of the main equation of CCS script we place labels of all
invisible ports.
If we apply the Trivial Conversion Algorithm to a given XCCS diagram, then it
can output a CCS script that does not satisfy requirements. We are able to precisely
identify the properties of those XCCS diagrams for which the trivial algorithm does not
produce a proper output. We call these properties conflicts and shadows. Shadows yield
non executable actions. Conflicts entail unwanted synchronizations whereas expected
synchronizations will not occur if the labels of connected ports have different names.
Let us define the properties in question.
Definition 2. We define the conflict of ports:
a) We say that ports Bi .a ∈ OutP and Bj .a ∈ InP are in conflict, iff
Bi 6= Bj ∧ (Bi .a → Bj .a) ∈
/ CR. (4)
We define the set of all conflicting output ports with the label a:
k .OutP (a) = {Bi .a : ∃Bj .a ∈ InP : Bi 6= Bj ∧ (Bi .a → Bj .a) ∈
/ CR} (5)
We define the set of all conflicting input ports with the label a:
k .InP (a) = {Bi .a : ∃Bj .a ∈ OutP : Bi 6= Bj ∧ (Bj .a → Bi .a) ∈
/ CR} (6)
Complementary ports are in conflict if they have the same labels and are placed on
different blocks and are not connected.
B1 B2
A = a.'b.c.'d.A;
a d a d
B = 'a.b.'c.d.B;
A B
b c b c
Fig. 2. Conflicts of ports
The conflicts of ports presented in Fig. 2 are as follows: i.B1 .a with v.B2 .a and
v.B1 .b with i.B2 .b and i.B1 .c with i.B2 .c and v.B1 .d oraz v.B2 .d. The letters i and v
indicate invisible and visible ports, respectively.
Definition 3. We define conflicts of ports and inner actions as follows:
a) We say that port Bi .a ∈ OutP and action a of the block Bj are in conflict, iff
Bi 6= Bj ∧ a ∈ Int(Bj ). (7)
4
5
b) We say that port Bi .a ∈ InP and co-action a of the block Bj are in conflict, iff
Bi 6= Bj ∧ a ∈ Int(Bj ). (8)
The output port of a given block and the action of another block are in conflict if the
label of the output port and the name of the inner action are the same. The input port of
a given block and the co-action of another block are in conflict, if the label of the input
port and the name of the inner co-action are the same.
B1 B2
A B A = 'a.'b.A;
a
B = a.b.B;
b
Fig. 3. Port B1 .a and action a as well as port B2 .b and co-action b are in conflict
Definition 4. The conflicts among inner action are defined as follows:
a) The action a of the block Bi and co-action a of the block Bj are in conflict, iff:
Bi 6= Bj ∧ a ∈ Int(Bi ) ∧ a ∈ Int(Bj ). (9)
We define the set of all blocks for which the action a is conflicting:
k .Int(a) = {Bi ∈ B : a ∈ Int(Bi ) ∧ a ∈ Int(Bj ) ∧ Bi 6= Bj } (10)
We define the set of all blocks for which the co-action a is conflicting:
k .Int(a) = {Bi ∈ B : a ∈ Int(Bi ) ∧ a ∈ Int(Bj ) ∧ Bi 6= Bj } (11)
Inner action and co-action of different blocks are in conflict if they have the same
names.
B1 B2
A B A = 'a.b.A;
a a
B = a.'b.B;
Fig. 4. Action b of the block B1 and co-action b of the block B2 are in conflict
Definition 5. The shadows of ports are defined as follows:
5
6
a) We say that port Bi .a ∈ OutP shadows port Bj .a ∈ OutP , iff
Bi 6= Bj ∧ ϑ(Bi .a) = i ∧ ϑ(Bj .a) = v (12)
b) We say that port Bi .a ∈ InP shadows port Bj .a ∈ InP , iff
Bi 6= Bj ∧ ϑ(Bi .a) = i ∧ ϑ(Bj .a) = v (13)
c) We say that port Bi .a ∈ OutP shadows port Bi .a ∈ InP , iff
ϑ(Bi .a) = i ∧ ϑ(Bi .a) = v (14)
d) We say that port Bi .a ∈ InP shadows port Bi .a ∈ OutP , iff
ϑ(Bi .a) = i ∧ ϑ(Bi .a) = v (15)
The invisible port of the given block shadows the visible port of another block if
both ports have the same label and are not complementary.
The invisible port shadows the visible port on the same block if both have the same
label and are complementary.
B1 B2
A = 'a.b.a.A;
a a a B = 'a.b.'b.B;
A B
b b b
Fig. 5. The shadows of ports
The shadows of ports presented in Fig. 5 are as follows: i.B1 .a shadows v.B2 .a and
i.B2 .b shadows v.B1 .b and i.B1 .a shadows v.B1 .a and i.B2 .b shadows v.B2 .b.
Definition 6. The shadows related to inner actions are defined as follows:
a) We say that port Bi .a ∈ OutP shadows co-action a of the block Bj , iff
Bi 6= Bj ∧ ϑ(Bi .a) = i ∧ a ∈ Int(Bj ). (16)
b) We say that port Bi .a ∈ InP shadows action a of the block Bj , iff
Bi 6= Bj ∧ ϑ(Bi .a) = i ∧ a ∈ Int(Bj ). (17)
c) We say that port Bi .a ∈ OutP shadows action a of the block Bi , iff
ϑ(Bi .a) = i ∧ a ∈ Int(Bi ). (18)
d) We say that port Bi .a ∈ InP shadows co-action a of the block Bi , iff
ϑ(Bi .a) = i ∧ a ∈ Int(Bi ). (19)
6
7
The invisible output port of a given block shadows an inner co-action of another
block if this co-action has the same name as the label of that port. The invisible input
port of a given block shadows an inner action of another block if this action has the
same name as the label of that port.
The invisible output port shadows his own inner action if this action has the same
name as the label of the port. The invisible input port shadows his own inner co-action
if this co-action has the same name as the label of the port.
B1 B2
A B A = 'a.b.a.A;
a
B = 'a.b.'b.B;
b
Fig. 6. The shadows related to inner actions
The shadows presented in Fig. 6 are as follows: i.B1 .a shadows co-action a of the
block B2 and i.B2 .b shadows action b of the block B1 and i.B1 .a shadows action a of
the block B1 and i.B2 .b shadows b of the block B2 .
4 Universal Conversion Algorithm
The priority of the relabelling is as follows: labels of visible isolated ports, inner actions
and co-actions, labels of visible connected ports, labels of invisible connected ports,
labels of invisible isolated ports.
We wish to retain the maximal number of names of visible isolated ports as they
correspond to observable actions and co-actions responsible for communication with
environment. On the other hand, we are the least interested in retaining names of invis-
ible isolated ports as they correspond to non executable actions and co-actions.
We introduce the following symbols:
[
Actions = A(CSS i ) the set of all actions contained in CSS scripts
CSS i ∈CSS
[
Actions = A(CSS i ) the set of all co-action contained in CSS scripts
CSS i ∈CSS
[
Agents = K(CSS i ) the set of all agent constants contained in CSS scripts
CSS i ∈CSS
E is the infinite set of labels, where E ∩ Actions = ∅ ∧ E ∩ Actions = ∅
C is the infinite set of agent constants, where C ∩ Agents = ∅.
Please note, the set E contains co-labels with the same names as the labels in E.
We will consider some finite subset E 0 ⊂ E of the set of labels E and some finite set
C 0 ⊂ C of the set of agent constants C. We will use the following notations:
7
8
– The ordered pair (Bi , CSSi ) represents the block Bi ∈ B and the CSS script
CSSi = ρ(Bi ) ∈ CSS assigned to that block.
– The symbol Bi∗ denotes the name of the block Bi and the symbol CSSi ∗ denotes
the name of CSSi script.
– The symbol #A denotes the cardinality of the set A, where # binds weaker than
operations in the field of sets.
The conversion algorithm is presented here:
1. The names of CSS scripts become the same as names of corresponding blocks.
We create a new set CSS 0 of CSS scripts, i.e. the set of sequences of algebraic
equations, in the following manner. For each agent block Bi ∈ B:
a) If for a pair (Bi , CSSi ) the names of the agent block and the CSS script are the
same, i.e. Bi∗ = CSSi ∗ , then we add the CSSi script to the CSS 0 set.
b) If for a pair (Bi , CSSi ) the agent constant Bi∗ ∈
/ K(CSSi ), then we replace the
name of the CSSi script and all the CSSi ∗ agent constants belonging to this
script with Bi∗ and then we add the Bi∗ script to the CSS 0 set.
c) If for a pair (Bi , CSSi ) the names of the agent block and CSS script are unlike,
i.e. Bi∗ 6= CSSi ∗ , but the agent constant Bi∗ ∈ K(CSSi ), then we replace
all the Bi∗ agent constants belonging to the CSSi script with the next agent
constant from C and then we replace the CSSi script name and all the CSSi ∗
agent constants belonging to this script with Bi∗ and then we add the Bi∗ script
to the CSS 0 set.
2. The ambiguities of names of the agent constants in CSS scripts are eliminated. We
create a new CSS 00 set of CSS scripts in the following manner. For each CSS script
CSSi ∈ CSS 0 :
For each agent constant C ∈ K(CSSi ) that is different from the name of the script,
i.e. C 6= CSSi ∗ , if there is another CSSj ∈ CSS 0 script such that C ∈ K(CSSj ),
then we replace all the C agent constants in the CSSi script with the next constant
from C and then we add CSSi to the CSS 00 set.
3. If the XCCS diagram is plain, then for each port Bi .a ∈ OutP we apply: all actions
a ∈ A(Bi∗ ) in CSS script Bi∗ are changed to co-actions a.
4. We create the quotient set P /∼ of all possible equivalence classes of the set of
ports P by synchronization relation SR. To the equivalence classes of SR we will
assign consecutive labels from the set E 0 or labels from the set CA. We assume that
ports from equivalence classes that have been assigned labels from the set E 0 are
removed from the set P .
a) We eliminate conflicts among visible isolated ports. For all labels a ∈ CA of
visible isolated input and output ports we apply:
If 0 < #V ∩ Iso ∩ k .InP (a) < #V ∩ Iso ∩ k .OutP (a), then to the equivalence
classes of ports from the set V ∩ Iso ∩ k .InP (a) we assign the next label from
the set E 0 .
If 0 < #V ∩ Iso ∩ k .OutP (a) ≤ #V ∩ Iso ∩ k .InP (a), then to the equivalence
classes of ports from the set V ∩ Iso ∩ k .OutP (a) we assign the next label from
the set E 0 .
8
9
b) We eliminate conflicts of inner actions and co-actions with visible isolated ports.
For every inner action a ∈ Int and co-action a ∈ Int we apply:
If the action a is in conflict with visible isolated port Bi .a ∈ OutP , then in
all CSS scripts that are assigned to blocks from the set k .Int(a) all actions a
assume the name of the next label from the set E 0 .
If the co-action a is in conflict with visible isolated port Bi .a ∈ OutP , then in
all CSS scripts that are assigned to blocks from the set k .Int(a) all co-actions a
assume the name of the next label from the set E 0 .
c) We eliminated conflicts among inner actions and co-actions. For every inner
action a ∈ Int we apply:
If 0 < #k .Int(a) < #k .Int(a), then in all CSS scripts assigned to blocks from
the set k .Int(a) all actions a assume the name of the next label from the set E 0 .
If 0 < #k .Int(a) ≤ #k .Int(a) then in all CSS scripts assigned to blocks from
the set k .Int(a) all co-actions a assume the name of the next label from the set
E0.
d) We relabel visible connected ports. In this step we begin from the least numerous
equivalent classes. For every equivalence class of synchronization relation SR
we apply:
If in the equivalence class exists a port with some label a ∈ CA and all other
ports in this class when relabelled with this label a will not be conflicting with
other visible ports and inner actions, then to this class we assign the label a,
otherwise we assign the next label from the set E 0 .
e) We relabel invisible connected ports. In this step we begin from the least numer-
ous equivalent classes. For every equivalence class of synchronization relation
SR we apply:
If in the equivalence class exists a port with some label a ∈ CA and all other
ports in this class when relabelled with this label a will not conflict and shadow
with: visible ports, inner actions, other invisible connected ports and previously
„relabelled ports”, then to this class we assign the label a, otherwise we assign
the next label from the set E 0 .
f) We relabel invisible isolated ports. For every one element equivalence class of
SR we apply:
If the port from this class is in conflict with or shadows: visible port, inner action
or co-action, previously „relabelled ports”, then to this port we assign the next
label from the set E 0 .
g) We eliminate conflicts among invisible isolated ports. For all labels a ∈ CA of
invisible isolated input and output ports we apply:
If 0 < #I ∩ Iso ∩ k .InP (a) < #I ∩ Iso ∩ k .OutP (a), then to the equivalence
classes of ports from the set I ∩ Iso ∩ k .InP (a) we assign the next label from
the set E 0 .
If 0 < #I ∩ Iso ∩ k .OutP (a) ≤ #I ∩ Iso ∩ k .InP (a), then to the equivalence
classes of ports from the set I ∩ Iso ∩ k .OutP (a) we assign the next label from
the set E 0 .
5. We relabel actions and co-actions in CSS scripts from the CSS 00 set. For every port
Bi .a ∈ InP and for every port Bi .a ∈ OutP we apply:
9
10
If the equivalence class [Bi .a]SR has been assigned to the label e, then in CSS script
Bi∗ all a actions are relabelled to e.
If the equivalence class [Bi .a]SR has been assigned to the label e, then in CSS script
Bi∗ all co-actions a are relabelled to e.
6. We create the output CCS script. The main agent equation takes the form:
S = (B1 |B2 | . . . |Bn )\{Res} (20)
where B1 , B2 , . . . , Bn ∈ CSS 00 , and the set Res contains all labels which has
been assigned to the equivalence classes of SR with invisible ports and labels of
remaining invisible ports. Under the main expression we place all definitions of
CSS scripts.
4.1 Example Conversion
CCS process algebra can be used to verify modular asynchronous circuits [8]. Let us
then examine a simple XCCS model of NAND gate presented in Fig. 7.
And
a0 Neg
a1 c0 a0 b0
And Neg
b0 c1 a1 b1
b1
Fig. 7. XCCS model of NAND gate
Definitions of CSS scripts assigned to the blocks are as follows:
And = a0.(b0.’c0.And + b1.’c0.And) + a1.(b0.’c0.And + b1.’c1.And);
Neg = a0.’b1.Neg + a1.’b0.Neg;
The algorithm executes as follows:
1. The names of CSS scripts are already the same as names of corresponding blocks.
2. There are no any ambiguities of names of agent constants in CSS scripts.
3. Skipped as it is full XCCS diagram.
4. Assume that we have the subset E 0 = {b0_1, b1_1} ⊂ E of labels E. We partition
the set of ports P into equivalence classes P /∼ of synchronization relation SR.
a) For every label a ∈ CA of visible isolated input and output port:
V ∩ Iso ∩ k .InP (b0) = {And.b0} V ∩ Iso ∩ k .OutP (b0) = {N eg.b0}
V ∩ Iso ∩ k .InP (b1) = {And.b1} V ∩ Iso ∩ k .OutP (b0) = {N eg.b1}
10
11
The following conditions hold:
0 < #V ∩ Iso ∩ k .OutP (b0) = 1 ≤ #V ∩ Iso ∩ k .InP (b0) = 1
0 < #V ∩ Iso ∩ k .OutP (b1) = 1 ≤ #V ∩ Iso ∩ k .InP (b1) = 1
Thus, to the equivalence classes of ports from set V ∩ Iso ∩ k .OutP (b0) and
V ∩ Iso ∩ k .OutP (b1) we assign consecutive labels from the set E 0 :
– [N eg.b0]SR = {N eg.b0} 7→ b0_1
– [N eg.b1]SR = {N eg.b1} 7→ b1_1
b) Skipped as the diagram does not have inner actions.
c) Skipped as the diagram does not have inner actions and co-actions.
d) Skipped as the diagram does not have visible connected ports.
e) We consider equivalence classes of invisible connected ports. In both of these
classes we find a label that will not cause conflicts and shadows with visible
ports and invisible connected ports when the relabelling is applied, thus:
– [And.c0]SR = {And.c0, N eg.a0} 7→ c0 ∈ CA
– [And.c1]SR = {And.c1, N eg.a1} 7→ c1 ∈ CA
f) Skipped as the diagram does not have invisible isolated ports.
g) Skipped as the diagram does not have invisible isolated ports.
5. We consider equivalence classes that have been assigned the labels:
– [N eg.b0]SR = {N eg.b0} 7→ b0_1
– [N eg.b1]SR = {N eg.b1} 7→ b1_1
– [And.c0]SR = {And.c0, N eg.a0} 7→ c0
– [And.c1]SR = {And.c1, N eg.a1} 7→ c1
After the relabelling the CSS scripts look like these:
– And = a0.(b0.c0.And + b1.c0.And) + a1.(b0.c0.And + b1.c1.And)
– Neg = c0.b1_1.N eg + c1.b0_1.N eg
6. We specify the output CCS script:
NAND = (And|N eg)\{c0, c1}
And = a0.(b0.c0.And + b1.c0.And) + a1.(b0.c0.And + b1.c1.And)
N eg = c0.b1_1.N eg + c1.b0_1.N eg
5 Conclusions and Future plans
We presented the Universal Conversion Algorithm that is helpful when we use XCCS
modelling language as a tool supporting fast and flawless development of CCS process
algebra scripts. This algorithm takes into consideration the priority of actions in XCCS
diagram and strife to minimize the number of relabelled actions for the sake of clarity.
We plan to elaborate analogous conversion algorithm for a hierarchical version of
XCCS modelling language. This would allow easy development and management of
11
12
the libraries of CCS scripts. In this approach, any CCS script can be represented as
a hierarchical agent block. Two or more hierarchical blocks can be used to compile a
new model. We do not need to worry about unwanted synchronizations, non-executable
actions and absence of desired synchronizations. The conversion algorithm will care to
produce a proper resulting CCS script.
Until now, the creation and management of CCS script libraries was hardly possible
due to the nature of synchronization in CCS process calculus and lack of appropriate
tools.
References
1. Balicki, K., Szpyrka, M.: Formal definition of XCCS modelling language. Fundamenta In-
formaticae 93 (2009) 1–15
2. Milner, R.: A Calculus of Communicating Systems. Volume 92 of LNCS. Springer-Verlag
(1980)
3. Milner, R.: Communication and Concurrency. Prentice-Hall (1989)
4. Fencott, C.: Formal Methods for Concurrency. International Thomson Computer Press,
Boston, MA, USA (1995)
5. Aceto, L., Ingófsdóttir, A., Larsen, K., Srba, J.: Reactive Systems: Modelling, Specification
and Verification. Cambridge University Press, Cambridge, UK (2007)
6. Szpyrka, M., Balicki, K.: XCCS – graphical extension of CCS language. In: Proc. of Mixdes
2006, the 14th International Conference Mixed Design of Integrated Circuits and Systems,
Ciechocinek, Poland (2007) 688–693
7. Szpyrka, M., Matyasik, P.: Formal modelling and verification of concurrent systems with
XCCS. In: Proceedings of the 7th International Symposium on Parallel and Distributed Com-
puting (ISPDC 2008), Krakow, Poland (2008) 454–458
8. Joeli, M., Kol, R., eds.: Verification of Systems and Circuits Using L OTOS, Petri Nets, and
CCS. John Wiley and Sons, Chichester, UK (2008)
12