Information Technology Reference
In-Depth Information
1
VAR_INPUT X: BYTE; END_VAR
2
VAR
Y: BYTE; END_VAR
3
LD
X
4
GT
100
5
JMPC
m
6
LD
Y
7
ADD
1
8
ST
Y
9
RET
10
m: LD
Y
11
SUB
1
12
ST
Y
13
RET
Fig. 3. Example program with input-dependent invariants
each cycle — of the new variable values on the old values (possibly input
values) as symbolic invariants.
These invariants sometimes depend on the actual values of the inputs,
which we will now show on an additional example. The program shown in
Fig. 3 has two variables
X
,
Y
of type
BYTE
, where
X
is an input variable and
Y
is an internal variable. In each cycle,
Y
is decremented if
X
is greater than
100
, otherwise incremented. Since this program has two different execution
paths for
X
∈
[0
, we get two different invariants for
this program. Generating the invariants for the second program, results in
the two invariants
,
100]
and
X
∈
[101
,
255]
100] =
⇒ Y
(1)
=u8(
Y
(0)
+1)
X
∈
[0
,
255] =
⇒ Y
(1)
=u8(
Y
(0)
−
1)
∈
[101
,
and
X
for the distinct execution paths, where
Y
(0)
and
Y
(1)
are the values in
Y
before and after executing the cycle.
As a real-world example, we also generated invariants for an implementa-
tion of the PLCopen safety function block
emergency stop
[16], kindly pro-
vided by Soliman and Frey [18]. The function block has
5
Boolean inputs and
2
16
possible configura-
tions). The implementation uses the internal variables to control the current
state while monitoring the emergency stop signal, the reset function, etc.
With our method, we derive
the implementation uses
11
internal variables (giving
75
invariants for the function block. A typical
invariant is:
Activate
(0)
=
false Ready
(1)
=
false
∧ S
1
(0)
=
false
=
⇒∧S
_
EStopOut
(1)
=
false
∧ S
2
(0)
=
true ∧ S
1
(1)
=
true ∧ S
2
(1)
=
false.
The variables
S
1
and
S
2
indicate the states
idle
and
init
, while the other
variables are the input and output variables according to the PLCopen speci-
