Information Technology Reference
In-Depth Information
this problem, we propose to use a different approach: Instead of verifying a
previously stated specification, our method derives symbolic invariants.
Invariants as such have long served for reasoning about correctness of
programs. They can describe relations between the valuations of variables
that hold after the execution of a program fragment regardless of the input
values [7]. Examples of invariants are, for instance,
x
=
−
y
or
x
≤
0
.
To derive invariants, our approach considers an input program written
in Instruction List (IL) and iteratively rewrites this program into a symbolic
representation over quantifier-free linear arithmetic with Boolean connectives,
following the semantics of the involved operations.
Our method is different from existing work in that it directly targets
PLCs running in the
cyclic execution mode
, which consists of three steps,
each of which is executed atomically: reading inputs, processing data, writing
outputs. Our approach translates the semantics of the instruction set into
linear constraints and then uses a set of rewriting rules to derive invariants.
Since PLCs are typically running in safety-critical systems where timeliness is
a strong concern, most of these programs do not consist of long running loops
(not to say, infinite loops). This property ensures that the derived arithmetic
expressions do not grow without bounds.
In previous work, Pavlovic et al. [15] have translated programs written
in
Statement List
into the input language of the model checker
[4].
Their most important contribution was the formal verification of the program
depicted in the left hand side of Fig. 1. As input for
NuSMV
NuSMV
, they used the
following specification given in the temporal logic
LTL
[6]:
G
(
PC
=2
⇒
Byte
=(
Bit0
+2
∗
Bit1
+4
∗
Bit2
+8
∗
Bit3
(1)
+16
∗
+32
∗
+64
∗
+ 128
∗
))
Bit4
Bit5
Bit6
Bit7
In summary, this specification states that the program converts a bit-
vector of length 8 into an unsigned byte. The approach described by Pavlovic
et al., however, has two drawbacks. On the one hand, the runtime require-
ments for their approach is significant: Model checking took approximately
8h (even though this could be reduced to 113s with manual intervention). On
the other hand, the specification needs to be formulated manually.
Our method can be seen as a response to these problems: By rewriting
the instructions in the program, it derives the stated invariant automatically.
Further, the runtime is essentially non-measurable, requiring less than 0.1s
overall. In summary, we make the following contributions:
- We detail an automatic approach for deriving invariants from PLC pro-
grams written in IL.
- We present the effectiveness of this approach on three examples, where
precise and expressive invariants were derived.
Our approach is as follows. The program is first rewritten into a so-called
static single assignment (SSA) form, that explicitly shows all calculation steps
