Information Technology Reference
In-Depth Information
in a symbolic representation (cp. Sect. 2). Then, this explicit form is used
to derive symbolic invariants by analyzing the SSA expressions stored in
output variables at the end of the PLC cycle (cp. Sect. 3). We additionally
present a second example, where two invariants are derived depending on the
actual input values and a third example analyzing an implementation of a
PLCopen safety function block. The paper is concluded by presenting related
work (cp. Sect. 4) and discussing results and future work (cp. Sect. 5).
2
Rewriting of IL Programs Into SSA Form
For the application of our method, we are analyzing IL programs, which
is is one of the standardized languages for programming PLCs [9]. It is
accumulator-based and similar to many machine languages. With its sim-
ple semantics it is ideal for deriving symbolic information.
We will motivate our approach with the
FromByte
program according
to Pavlovic et al. [15], which was translated to IL [17]. An excerpt of this
program is shown in Fig. 1 on the left side. It has eight Boolean inputs
named
in0
to
in7
and converts these to the byte represented by them. This
is accomplished by converting the inputs to the corresponding integer (
false
to
0
and
true
to
1
), multiplying them by their significance and adding up the
results in a temporary variable called
temp
.
For deriving symbolic invariants, we begin by rewriting IL programs into
an SSA form [5]. In this form, each IL instruction is written as an assignment.
Each of these assignments creates a new instance of the accumulator or a
variable, indicated by a superscript number. If, e. g., the current accumulator
acc
(
i
)
is incremented by
1
, the SSA expression
acc
(
i
+1)
:= acc
(
i
)
+1
would be generated. The superscript number is called
instance number
.On
the left hand side (LHS) of such expressions, there is either a new instance of
the accumulator or a new instance of some program variable. The right hand
is side (RHS) is either
- a constant,
- a program variable that was not yet used on a LHS,
- an arithmetic, logic or relational operation of existing LHSs, or
- a data type cast. For example, a cast of the accumulator to the
BYTE
type is written u
8(acc)
, indicating the 8 bit unsigned type.
The transformation of the IL program into SSA form is performed auto-
matically. In order to achieve this, different execution paths are separated by
partitioning the possible ranges of input variables as presented in [17]. Addi-
tionally, all loops are unrolled, removing conditional execution all together.
Formally, the translation is shown in Fig. 2 for the instructions
LD
,
ST
,
ADD
,
SUB
and
AND
. We assume that there are already
i
instances of the accumu-
lator, so a write to the accumulator creates instance
i
+1
. For the store to
