The composition of the two program components, M 1 and M 2 , denoted M 1 ||M 2 , synchronizes on
read-write actions on the same channel. Between two synchronized actions, the individual actions of both
systems interleave.
1: while(true)
2:
password:=readInput;
3
while(password≤ 999)
4:
password:=readInput;
5:
password2:=encrypt(password);
q0
q1
q2
q3
q4
read ?xpw
xpw ≤999
read ?xpw
999
getEnc?xpw2
Fig. 1: Modeling a communicating program as an automaton M 2
Figure 1 presents the code of a communicating program (left) and its corresponding automaton M 2
(right). The automaton alphabet consists of constraints (e.g. x pw ≤ 999), assignment actions (e.g. y pw :=
2 · y pw in M 1 of Figure 2), and communication actions (e.g. enc!x pw sends the value of variable x pw over
channel enc, and getEnc?x pw2 reads a value to x pw2 on channel getEnc).
The specification P is modeled as an automaton that does not contain assignment actions. It may contain
communication actions in order to specify behavioral requirements, as well as constraints over the variables
of both system components, that express requirements on their values in various points in the runs.
Consider, for example, the program M 1 and the specification P seen in Figure 2, and the program M 2
of Figure 1. M 2 reads a password on channel read to the variable x pw , and once it is long enough (has
at least four digits), it sends the value of x pw to M 1 through channel enc. M 1 reads this value to variable
y pw and then applies a simple function that changes its value, and sends the changed variable back to M 2 .
The property P reasons about the parallel run of the two programs. The pair (getEnc?x pw2 , getEnc!y pw )
denotes a synchronization of M 1 and M 2 on channel getEnc. P makes sure that the parallel run of M 1 and
M 2 always reads a value and then encrypts it – a temporal requirement. In addition, it makes sure that the
value after encryption is different than the original value, and that there is no overflow – both are semantic
requirements on the program variables. That is, P expresses temporal requirements that contain first order
constraints. In case one of the requirements does not hold, P reaches the state r 4 which is an error state.
Note that P here is not complete, for simplicity of presentation (see Definition 5 for a formal definition of
a complete program).
p0
p1
p2
enc?ypw
ypw :=2·ypw
getEnc!ypw
r1
r2
r0
r4
r3
read ?xpw
(getEnc?xpw2,getEnc!ypw )
read ?xpw
xpw !=xpw2
ypw <2 64
xpw ==xpw2
ypw ≥2 64
M1
P
Fig. 2: The programs M 1 , M 2 , and the specification P
212
H. Frenkel et al.
read-write actions on the same channel. Between two synchronized actions, the individual actions of both
systems interleave.
1: while(true)
2:
password:=readInput;
3
while(password≤ 999)
4:
password:=readInput;
5:
password2:=encrypt(password);
q0
q1
q2
q3
q4
read ?xpw
xpw ≤999
read ?xpw
999
getEnc?xpw2
Fig. 1: Modeling a communicating program as an automaton M 2
Figure 1 presents the code of a communicating program (left) and its corresponding automaton M 2
(right). The automaton alphabet consists of constraints (e.g. x pw ≤ 999), assignment actions (e.g. y pw :=
2 · y pw in M 1 of Figure 2), and communication actions (e.g. enc!x pw sends the value of variable x pw over
channel enc, and getEnc?x pw2 reads a value to x pw2 on channel getEnc).
The specification P is modeled as an automaton that does not contain assignment actions. It may contain
communication actions in order to specify behavioral requirements, as well as constraints over the variables
of both system components, that express requirements on their values in various points in the runs.
Consider, for example, the program M 1 and the specification P seen in Figure 2, and the program M 2
of Figure 1. M 2 reads a password on channel read to the variable x pw , and once it is long enough (has
at least four digits), it sends the value of x pw to M 1 through channel enc. M 1 reads this value to variable
y pw and then applies a simple function that changes its value, and sends the changed variable back to M 2 .
The property P reasons about the parallel run of the two programs. The pair (getEnc?x pw2 , getEnc!y pw )
denotes a synchronization of M 1 and M 2 on channel getEnc. P makes sure that the parallel run of M 1 and
M 2 always reads a value and then encrypts it – a temporal requirement. In addition, it makes sure that the
value after encryption is different than the original value, and that there is no overflow – both are semantic
requirements on the program variables. That is, P expresses temporal requirements that contain first order
constraints. In case one of the requirements does not hold, P reaches the state r 4 which is an error state.
Note that P here is not complete, for simplicity of presentation (see Definition 5 for a formal definition of
a complete program).
p0
p1
p2
enc?ypw
ypw :=2·ypw
getEnc!ypw
r1
r2
r0
r4
r3
read ?xpw
(getEnc?xpw2,getEnc!ypw )
read ?xpw
xpw !=xpw2
ypw <2 64
xpw ==xpw2
ypw ≥2 64
M1
P
Fig. 2: The programs M 1 , M 2 , and the specification P
212
H. Frenkel et al.