Information Technology Reference
In-Depth Information
fication. The variables of the program not shown are not relevant for the in-
variant. By this invariant, we can deduce that if we are in state
init
and the
Activate
signal is reset, the outputs
Ready
and
S_EStopOut
are reset
and the state
idle
is signaled, independently of all other inputs or program
states.
To gain an overview over program behavior, we provide a means for fil-
tering the invariants for certain inputs or outputs. There are, for instance,
only
invariants generated where the input
Activate
is
false
. Similar in-
variants can be inspected for the state variables
S_i
or output variables like
S_EStopOut
.
10
4
Related Work
Transferring formal verification methods from theory to practical applications
is an active topic, and particularly important for safety-critical systems. This
includes, but is not limited to model checking [17] and static program anal-
ysis [3,8]. Additionally, techniques based on exact decision procedures have
found application, for instance, the work by Sülflow and Drechsler [19] on
SAT-based equivalence checking. More comprehensive overviews of existing
approaches for formlization and verification of PLC programs are given else-
where [2,13,1].
Invariant generation using program rewriting is a widely appreciated con-
cept in the fundamental research on program verification [14], e.g., in the
context of verifying heap-manipulating programs [11]. However, to the best
of our knowledge, the concept of applying rewriting logic was not applied to
PLC programs before, where it allows to derive strong invariants due to the
limitations of the underlying hardware platform. Often, even simple logics as
the one described in this work suce for deriving expressive invariants.
5
Discussion & Future Work
Invariants are a simple means to represent properties of programs. The logic
considered in this paper — in contrast to other logics used for specifying
properties such as
LTL
or
CTL
— is easy to formulate and understand. Usu-
ally, invariants are used in formal verification techniques like model checking
to specify properties to be proven. In this paper, we proposed a new approach
that automatically derives invariants for all variables of a program, i. e., an
over-approximation of properties of the variables is generated automatically.
Thus, users do not need to provide properties of a program and use formal
verification techniques to prove these properties, which might be error-prone
and lengthy. The invariants derived can then be analyzed by users to check
whether the program behaves as expected.
Two specifics enabled the automatic generation of invariants for PLC pro-
grams and facilitated the scalability of the approach described: the underlying
hardware of the PLCs and the usage of SSA form. The underlying hardware
