Information Technology Reference
In-Depth Information
acc
(
i
+1)
:=
LD x
x
var
(
j
+1)
:= u8(acc
(
i
)
)
ST var
acc
(
i
+1)
:= acc
(
i
)
+
x
ADD x
acc
(
i
+1)
:= acc
(
i
)
−
x
SUB x
acc
(
i
+1)
:= acc
(
i
)
and
x
AND x
Fig. 2. IL instructions and how the are represented in SSA form
byte
(0)
=u8(acc
(29)
)
=u8(acc
(28)
+
temp
(6)
)
=u8((acc
(27)
∗
128) + acc
(25)
)
=u8((
in7
∗
128) + u8(acc
(24)
+
temp
(5)
))
...
=u8((
in7
∗
128) + u8((
in6
∗
64) + u8((
in5
∗
32) + u8((
in4
∗
16)
+ u8((
in3
∗
8) + u8((
in2
∗
4) + u8((
in1
∗
2) + u8(
in0
))))))))
.
from_byte
=
from
_
Here, each step consists of a replacement of a LHS by its corresponding
RHS expression by a look-up in the list of SSA expressions. In the step from
the second to the third line, e. g.,
acc
(29)
was replaced by
acc
(28)
+
temp
(6)
(cf. Fig. 1 line 38). Afterwards, we can apply some simplifications on the
expression found, to make them more readable and easier to understand.
This includes
(
false
or
false
)
is rewritten as
false
),
- the folding of constants (e. g.
- the removal of unnecessary casts,
- the elimination unused subexpressions (e. g.
(
true
or
expr
)
is rewritten as
true
).
These steps are repeated until there are no further simplifications.
The crucial point here is that the final invariant for
form_byte
is exactly
the invariant that was manually specified as the
LTL
formula (1) by Pavlovic
et al. This means we can derive the invariant without a time-consuming
model checking process here. Often, these invariants also give insight into the
program behavior without manual writing specifications.
Now, we will formalize the derivation of the invariants. For each non-
temporary program variable
var
,wehavesomeinstance
var
(0)
which corre-
sponds to the value of the variable at the beginning of the PLC cycle. This
can be either an input value read from a sensor or the last value of the pre-
vious cycle. For each output variable
out
i
, on the other hand, we have some
final value
out
i
(
n
i
)
, where
n
i
is maximal. This corresponds to the final output
value at the end of the PLC cycle. If we derive the invariants for all variables
out
i
(
n
i
)
of the program using this technique, we get the dependence — for
