Information Technology Reference
In-Depth Information
acc
(0)
:=
in
0
(0)
1
LD
in0
acc
(1)
:=
8(acc
(0)
)
2
BOOL_TO_BYTE
u
temp
(0)
:=
8(acc
(1)
)
3
ST
u
temp
acc
(2)
:=
in
1
(0)
4
LD
in1
acc
(3)
:=
8(acc
(2)
)
5
BOOL_TO_BYTE
u
acc
(4)
:= acc
(3)
∗
2
6
MUL
2
acc
(5)
:= acc
(4)
+
temp
(0)
7
ADD
temp
temp
(1)
:=
8(acc
(5)
)
8
ST
temp
u
.
.
acc
(29)
:= acc
(28)
+
temp
(6)
38
ADD
temp
from
_
byte
(0)
:=
8(acc
(29)
)
39
ST
u
from_byte
Fig. 1. Program
FromByte
and equivalent SSA form
byte variable
var
a new instance
var
(
j
+1)
is created assuming that there are
already
j
instances. The symbol
x
represents either a constant or an existing
LHS and is unchanged.
For now, this approach is limited to integer arithmetic and Boolean logic.
Converting to other types results in separate invariants for all possible integer
values.
For the
FromByte
program the results are presented on the right side
of Fig. 1. In the first line, the instance
acc
(0)
of the accumulator is created,
resembling the load instruction of the variable
in0
.Afterthe
39
lines of
(a
BYTE
cast of the 29
th
instance of
the accumulator) is assigned to the output variable
from_byte
. Based on
this final expression, we will derive the invariant of this program in the next
section.
8(acc
(29)
)
the program, the expression u
3
Generation of Invariants
In this section we will use the SSA form defined in the last section to generate
symbolic invariants. The key idea is that for each variable introduced in SSA,
we still have symbolic information how the value was calculated if we inspect
the corresponding RHS. By inducing and thereby replacing all LHSs with the
corresponding RHS expressions until we reach constants or variables with an
instance number of
, we can build up symbolic expressions for each LHS. If
we do this for the output variable
from_byte
of the example program at
the end of the PLC cycle, we obtain the following resolution steps:
0
