Keywords

1 Introduction

Motivation and Topic. Automated production systems [34], such as industrial plants and assembly lines, are usually driven by Programmable Logic Controllers (PLCs). These computing devices are specially tailored to controlling automated production systems in safety-critical realtime environments. A malfunction may cause severe damage to the system itself or to the payload, or even harm persons within the reach of the system.

The topic of this paper is how to formally verify correctness of the software part of such systems, i.e., the PLC. To be precise, we focus on regression verification of PLC code – as opposed to proving that the PLC code satisfies a functional specification or to proving that the whole production system works correctly. That is, we verify that a version of PLC code after an evolution step shows the same reactive input/output behavior as the old one – allowing only desired deviations that are formally specified. The aim of regression verification is to formally prove that existing (good) behavior is retained during system evolution. The old version serves as specification for the new one.

Our Approach and Contribution. This work contributes to the field of formal PLC verification by defining a notion of reactive conditional and reactive relational equivalence together with a proof methodology, also in the presence of environment models. Our main contribution is the design, implementation, and evaluation of a regression verification method for PLC code.

A core element of our verification method is a translation of PLC code into the SMV input language for model checkers. Using this translation on both the old and the new software revision, we can construct a formula expressing that intended behavior is retained. We target PLC code written in the two languages Structured Text (ST) and Sequential Function Chart (SFC), which are part of IEC 61131, the industry standard for PLC software [19]; an adaptation to other languages is easily possible.

A further core element is the use of a model checker supporting invariant generation. It is an important insight that this allows the automatic generation of coupling invariants, which are a useful tool for efficient regression verification. Accordingly, we have adapted the concept of coupling invariants to the world of reactive systems. And we have implemented our approach in a toolchain using the model checker nuXmv [9]. It supports techniques for predicate abstraction and invariant generation by interpolant inspection [7, 24].

As full equivalence of PLC code revisions is not the goal in many cases, we have defined and implemented extensions where the behavior of the new code revision may deviate under certain specified conditions and in specified ways.

We have successfully evaluated our approach using the Pick-and-Place Unit, a benchmark case study for the evolution of automated production systems with several evolution scenarios [35]. We were able to demonstrate our method’s feasibility for practical evolution scenarios and its ability to uncover regression bugs.

PLCs execute their software in cycles with fixed cycle time. Consequently, PLC code can only cause timing problems if its execution time exceeds the cycle time. Otherwise, the code’s exact execution time is irrelevant. Thus, we assume that the cycle time constraint is ensured by other techniques, and we do not consider exact execution time in our method.

Advantages of Regression Verification for PLC Code. The main advantage of regression verification is that no functional or behavioral specification is needed (besides the old code version). In addition, regression verification is particularly well suited for the application area of software in automated production systems for the following reasons.

Automated production systems are designed for long deployment phases, often spanning several decades. But the requirements on production systems change over time. New types of products are to be manufactured. Systems are upgraded to increase throughput or to keep up with technological development. Moreover, flaws in the controlling software or the hardware design may have to be fixed. Production systems therefore frequently evolve during their lifetime. Thus, methods and means to safely update their hardware and software – including their PLCs – are of great importance. One has to ensure that a revision does not break existing intended behavior.

As opposed to (regression) testing, regression verification provides an equivalence proof for all possible inputs and not just for individual test cases. Also, while regression testing of PLC software requires either a hardware testbed or an executable hardware model, this is not needed for regression verification. It suffices to provide a formal description of how the hardware has changed during the evolution step (if the hardware has changed at all).

PLC systems can grow rather large, making a (non-regression) correctness verification challenging for fully automatic verification and bisimulation checkers. However, typical changes made during an evolution step are small in comparison to overall system size, so that regression verification is a much easier task.

Structure of this Paper. In Sect.  2, we present a small scenario from our case study as an introductory example. Then, in Sect.  3, we define the formal framework and introduce notions of equivalence between versions of PLC code. In Sect.  4, we discuss the use of environment models to avoid false alarms. The core part of our method, i.e., the translation itself and the toolchain are described in Sect.  5. In Sect.  6, we present the extensive case study that we used to evaluate our approach. We discuss related work in Sect.  7 and draw conclusions in Sect.  8. Some of the ideas presented in the following are adaptations of our regression verification method for imperative programs [11] to the – rather different – world of reactive automated production systems.

2 Introductory Example

As an introductory example, we present a considerably simplified version of a scenario from the case study described in Sect.  6 (see also Fig.  4). A stationary crane moves workpieces from a starting point (A) to one of two target points (B) and (C). In the original version, the plant treats all workpieces in the same way and transports them from the magazine (A) to the conveyor (B).

Fig. 1.
figure 1

Sequential Function Charts for the example. (a) Original SFC, (b) SFC after revision.

Full size image

A new revision of the PLC software is introduced to differentiate the controller’s behavior according to the type of workpiece. All metallic workpieces are now first delivered to the stamp (C) where they are treated (signal stamped) and are only afterwards delivered to (B). All non-metallic workpieces still go directly to (B). An additional inductive sensor (signal M) is installed at (A) to detect whether a workpiece is metallic or not.

Figure  1 shows sequential function charts (SFCs) for the two versions of the PLC program. The boxes (called steps) contain actions (blocks of code) and the transitions between steps are annotated with guards. In each execution cycle, one step is active and is executed. If at the end of the cycle one of the guards at an outgoing transition is satisfied, the corresponding successor step is made the active step. Otherwise the current step remains active and is repeated in the next cycle. In the example, the actions assign values to output (Turn, Lift) and internal variables (metallic, stamped). The guard conditions are Boolean input variables corresponding to sensor input (A, B, C represent input from sensors for crane position) and Boolean internal variables (metallic). In the original SFC, the steps correspond to the actions of moving the crane to the magazine, picking up the workpiece, moving the crane to the conveyor, and putting down the workpiece. In the revised SFC, there is a case distinction on metallic, and two new steps have been added to move metallic pieces to the stamp and dropping them there. After the workpiece has been stamped, the internal variable metallic is set to \(\mathrm {FALSE}\) and then the step Pickup becomes active, i.e., from there on the SFC continues in the same way as if a non-metallic workpiece has just been picked up at (A).

Note that this is a simple example. In general, actions and guards can be considerably more complex and contain conditional statements and loops.

In case there are metallic workpieces, the behavior of the PLC is obviously different. But in case that only non-metallic workpieces are ever detected by sensor (M), the new software version should do the same as the old version. So this is a scenario for using regression verification to prove conditional equivalence for the unchanged case.

3 Formalizing Equivalence of PLC Programs

We define a formal framework for the behavior of reactive PLC software together with adequate notions of equivalence between them.

There are various possibilities for defining system boundaries when modeling an automated production system. One can model the whole system or only individual components. Even when focusing on the PLC, one could still include models of peripheral hardware components like connecting data buses. However, our method concentrates on the software that runs on the controller and disregards all effects outside the software for now. Section  4 discusses measures to take the environment into consideration.

PLCs are reactive systems with a cyclic data processing behavior, repeating the same control procedure indefinitely. A PLC cycle typically consists of the following steps: (1) read input values, (2) execute task(s), (3) write output values, (4) wait. As reactive systems, PLCs require a notion of equivalence that involves traces, which means that if the old and the new revision are presented with the same sequence of input sensor readings, they must produce the same sequence of actuator output stimuli.

We call the piece of code that is executed cyclically on the controller a PLC program. A PLC program P consists of the instructions \(\varPi \) to be executed and a set of declarations \(\varDelta \) of input, output and state variables. In the introductory example in Sect.  2, the declarations of the program contain the Boolean input (sensor) variables A, B, C and M; Lift and Turn are output (actuator) variables (the declarations are not shown in Fig.  1).

The internal state of a PLC program consists of an assignment of values to its state variables (in the example, the Boolean variable metallic). There is always an implicit state variable \( active\_step \) storing which of the steps in the SFC program is active. The declarations \(\varDelta \) induce an input value space I, an output value space O, and state space S, each as the Cartesian product of the value ranges of the corresponding program variables. In the example, I is \({bool}\times {bool}\times {bool}\times {bool}\). We assume the initial values of state variables to be determined by their declarations (using default values in case no initial value is given), i.e., the initial state \(s_0 \in S\) is fixed by \(\varDelta \).

Definition 1

(Semantics of PLC programs). The semantics \(\rho (P)\) of a PLC program P is a state transition function \( \rho (P) : S \times I \rightarrow S \times O. \)

The semantics \(\rho (P)\) depends on the instructions in \(\varPi \). These may read from the state and the input variables (in S and I) and write to the state variables and to the output variables (in S and O).

To be able to consider the effects of a PLC program over time, the above definition needs to be extended to sequences of inputs and outputs. We denote infinite sequences of elements in I (\(\omega \)-words) with \(\bar{i} \in I^\omega \); their components are accessed using subscript indices, i.e., \(\bar{i} = \langle i_1, i_2, \ldots \rangle \). The PLC program as a stateful system needs an initial state \(s_0\) from which it is launched. As mentioned above, \(s_0\) is determined by the variable declarations \(\varDelta \).

Definition 2

(Trace Semantics of PLC Programs). The behavior b(P) of a PLC program P with initial state \(s_0 \in S\) is the function \(b(P): I^\omega \rightarrow O^\omega \) defined by \(b(P)(\langle i_1,i_2,\ldots \rangle ) = \langle o_1, o_2, \ldots \rangle \) where \((s_n, o_n) = \rho (P)\big ((s_{n-1}, i_n)\big )\) for all \(n\in \mathbb {N}_{\ge 1}\).

This definition says that starting from the initial state \(s_0\), the PLC program is executed repeatedly, applying in each cycle \(\rho (P)\) to its current state \(s_{n-1}\) and the input tuple \(i_n \in I\) to produce the output tuple \(o_n \in O\) and the new state \(s_n\).

Trace semantics use the internal state in the definition, but when taking an outside look at the semantics, it defines input/output behavior and does not make statements about the internal state space. This is relevant for our initial definition of equivalence where programs are required to produce identical traces.

Definition 3

(Trace Equivalent PLC Programs). Two PLC programs P, Q whose declarations \(\varDelta _P, \varDelta _Q\) contain the same input/output variables are called perfectly equivalent if they produce the same output sequence when presented with the same input sequence, i.e., \(b(P)(\bar{i}) = b(Q)(\bar{i})\) for all \(\bar{i} \in I^\omega \).

They are called conditionally equivalent modulo the condition \(\varphi : I^\omega \rightarrow {bool}\) if they produce the same result for all input sequences that satisfy condition \(\varphi \), i.e., if \(\varphi (\bar{i})\) then \(b(P)(\bar{i}) = b(Q)(\bar{i})\) for all \(\bar{i} \in I^\omega \).

It is intuitively evident that replacing a PLC with a new revision whose program is trace equivalent to the original program does not change the observable behavior of the plant, provided everything else remains unchanged and timing effects are left aside.

Conditional equivalence relaxes the strict notion of perfect equivalence by requiring the same output sequence only if a condition \(\varphi \) holds. Intuitively this means that replacing a PLC with a new revision whose program is conditionally equivalent to the original program modulo \(\varphi \) does not change the plant’s behavior at least for those traces where all sensor signal readings satisfy \(\varphi \).

The example given in Sect.  2 is an example of conditional equivalence: The modified controller software (Fig.  1) is conditionally equivalent to the original version if every encountered workpiece is non-metallic. This condition can be expressed in Linear Temporal Logic (LTL [26]) as \(\varphi _{\mathrm {non-metallic}}(\bar{i}) = \mathbf{G }\, \lnot M\) recalling that M is the signal from the inductive metal detection sensor.

Perfect and conditional equivalence use equality to compare input and output traces. There are many cases, however, where full equality is not required or not appropriate. Equality of outputs may not be required for outputs relating to non-critical components of the system. And equality may not be the appropriate relation if the sensors and/or actuators of the plant have been modified, and thus the input/output spaces of the program revisions are different. It is therefore necessary to generalize the equivalence notion. To this end, we introduce binary relations \(\sim _{{in}}\) and \(\sim _{{out}}\).

Definition 4

(Relational Equivalence of Controllers). Two PLC programs P, Q with declarations \(\varDelta _P\) resp. \(\varDelta _Q\) are called relationally equivalent modulo relations \(\sim _{{in}}\subseteq I_P^\omega \times I_Q^\omega \) and \(\sim _{{out}}: O_P^\omega \times O_Q^\omega \) if they produce related output sequences when presented with related input sequences, i.e.,

figure a

Note that conditional equivalence can be expressed as relational equivalence (if \(I_P=I_Q\) and \(O_P=O_Q\)) by choosing \((\bar{i}=\bar{i}') \wedge \varphi (\bar{i})\) for the input relation \(\sim _{{in}}\) and \(\bar{o}=\bar{o}'\) for the output relation \(\sim _{{out}}\).

If a revision adds or removes existing variables from the declarations, the canonical relations to be considered are the conjoined equalities between all signals shared by both revisions (i.e., the variables in \(\varDelta _P \cap \varDelta _Q\)). This is called projected equivalence. The introductory example in Sect.  2 is a projected equivalence if the metallic detector is assumed absent in the first version and only introduced in the second. Another example of relational equivalence is shown in the case study in Sect.  6.

4 Environment Models to Increase Precision

False alarms can occur if the two revisions of a PLC program behave differently on input sequences that cannot actually occur in the application. For example, the crane from Sect.  2 can never be in more than one of the positions A, B, C at the same time. Assuming correctly working sensors, not more than one of the Boolean input variables A, B, C can be true at the same time. Thus, it would be irrelevant if the two program revisions were to react differently in case A and B were signaled simultaneously but would still be equivalent for all realistic inputs. It is therefore sensible to add such knowledge on the possible sensor inputs as assumptions to the process and perform a conditional regression verification. In the example, it is possible to encode the assumption in form of the LTL condition \(\mathbf{G }(\lnot (A\wedge B) \wedge \lnot (B\wedge C)\wedge \lnot (A\wedge C))\).

But in more involved cases, it is difficult or error-prone to express properties of the physical system correctly in form of temporal logic conditions on the PLC inputs. Then it is more intuitive to use a model of the environment taking the output of PLC program as input. This restricts the search space, increases precision of regression verification and avoids false alarms. Figure  2 depicts a model of the crane restricting the input space for the variables corresponding to the crane’s position and direction. Besides the three states for positions A, B, C in which the corresponding variable is true, there are three intermediate states between the positions where none of variables is true. The crane behavior model shows that when the crane turns to the right from position A to position B, first variable A is true, then no variable is true, and then B is true. By making environment models non-deterministic (like in the example), one can abstract from details like concrete numbers of waiting cycles.

Fig. 2.
figure 2

Finite automaton modeling crane position sensor readings.

Full size image

One evolution scenario of the case study in Sect.  6 describes a case where the PLC program revisions are only equivalent if an environment model is used.

5 Regression Verification Method and Toolchain

This section reports on how we achieve regression verification for PLC software by construction of a verification condition from two PLC program revisions, the equivalence relations \(\sim _{{in}}, \sim _{{out}}\), the condition \(\varphi \), and environment models.

The workflow of our method – shown in Fig.  3 – covers several transformation steps. The resulting verification condition consisting of a transition system and a property is presented to a model checker that can come back with three possible results: First, it may report that the verification property holds for the transition system in which case the two PLC programs are trace equivalent (modulo the condition, relations, and environment models). Second, it may report a counterexample with a concrete (finite) input trace that leads to the equivalence violation. There are no “false positives”: Every reported violation uncovers a case of unequal behavior. However, it may be that the environment is not modeled precisely enough, and that the failure is a false alarm in the sense that it cannot occur in practice with the real hardware. The variables range over finite datatypes and the model checking problem is, in theory, decidable. Depending on the size and complexity of the verification condition, it is still possible that the model checker runs out of resources (time or memory) and does not come back with an answer, which is the third possible result.

Fig. 3.
figure 3

Overview over the regression verification method.

Full size image

5.1 From PLC Code to Model Checker Input

The IEC 61131-3 standard [19] defines two textual and three graphical PLC programming languages. According to the ARC industry advisory group [1], the use of PLC systems compliant with IEC 61131-3 currently is and will remain the state of industrial practice for the next five to ten years. We consider input PLC programs written in the textual language Structured Text (ST) or in the graphical language Sequential Function Chart (SFC).

For a uniform treatment of programs regardless of the particular language, we define an intermediate language ST\(_0\) into which all incoming programs are translated. ST\(_0\) is a sublanguage of ST, and despite their notational differences, programs in all 61131-3 programming languages can be represented in it (provided they do not have unbounded loops). PLC programs are time-critical and are required to finish within their cycle time. It is hence reasonable to assume programs do not contain loops with an unbounded number of iterations.

The language ST\(_0\) is essentially the loop- and call-free fragment of ST reduced to fewer, more basic datatypes. The only types of statements in ST\(_0\) are assignments and if-then-else conditionals. During normalization to ST\(_0\), loops are fully unwound and function block invocation are inlined. To make loop unwinding possible, a bound for the number of iterations must be statically computable for all loops in the code. Inlining is also feasible since recursion is not featured in the IEC 61131-3 framework.

To demonstrate our method, we implemented such translations to ST\(_0\) for ST and SFC. The translation from SFC to ST\(_0\) is problematic since the standard leaves many semantical issues unanswered. We resolved this issue by following the formal semantics for SFCs given in [4] when translating SFC to ST\(_0\).

The normalized code in ST\(_0\) is symbolically executed to derive a state transition system as model checker input. Naïve implementations of symbolic execution (or weakest precondition calculi) may produce program representations whose size is exponential in that of the original program. This is due to an explicit enumeration of all possible paths through the program. Since ST\(_0\) programs resulting from translating SFC code involve many consecutive and nested if-statements to encode the original state machine, the number of paths through the program is huge and explicitly enumerating them is infeasible. For example, the last scenario (Ev14) of our case study (Sect.  6) yields some 13 billion paths, such that the resulting proof obligation would not fit into the available memory.

Instead we produce a smaller program representation by not explicitly enumerating all paths but following the concept of \(\varPhi \)-nodes (known from static single assignment [10]) to merge the effects of the branches of an if-statement. This approach is also similar to the optimized weakest-precondition-calculus from [12].

During symbolic execution, a symbolic variable map \({\mathcal V}: \textit{Vars}_\varDelta \rightarrow \textit{Terms}_\varDelta \) is updated, which assigns to all declared variables their current symbolic value (a term). Stmt \(_\varDelta \) denotes the set of all ST\(_0\)-statements, and \(t^{\mathcal V}\) is the symbolic evaluation of an expression t in the symbolic variable assignment \({\mathcal V}\).

Definition 5

(Symbolic Execution). Symbolic execution of ST\(_0\) code is the operator \(se : (\textit{Vars}_\varDelta \rightarrow \textit{Terms}_\varDelta ) \times Stmt_\varDelta \rightarrow (\textit{Vars}_\varDelta \rightarrow \textit{Terms}_\varDelta )\) with

$$\begin{aligned}&se({\mathcal V}, v:=t) := {\mathcal V}[ v := t^{\mathcal V}] \qquad \qquad se({\mathcal V}, S{;}T) := se(se({\mathcal V}, S), T) \\&\qquad \ \ se({\mathcal V}, \mathrm {if}\ c\ \mathrm {then}\ S\ \mathrm {else}\ T) := \varPhi (c^{\mathcal V}, se({\mathcal V}, S), se({\mathcal V}, T)) \end{aligned}$$

where the map \(\varPhi (c, {\mathcal V}_1, {\mathcal V}_2): \textit{Vars}_\varDelta \rightarrow \textit{Terms}_\varDelta \) is, for all \(v\in \textit{Vars}_\varDelta \), defined by:

$$\begin{aligned} \varPhi (c, {\mathcal V}_1, {\mathcal V}_2)(v)&:= {\left\{ \begin{array}{ll} {\mathcal V}_1(v) &{} \text {if}\ {\mathcal V}_1(v) = {\mathcal V}_2(v) \\ \mathrm {if}\ c\ \mathrm {then}\ {\mathcal V}_1(v)\ \mathrm {else}\ {\mathcal V}_2(v) &{} \text {otherwise} \end{array}\right. } \end{aligned}$$

Essentially, this transformation moves the conditions of if-then-else statements into the variable assignment in form of if-then-else expressions. While this procedure cannot guarantee that the result is not exponentially larger than the input, our experiences show that the results are acceptable in practice.

The state transition system for a program P is computed as follows: The operator se is applied to the instructions \(\varPi \) of P with the identity mapping \(id_\varDelta \) as the starting point, resulting in the symbolic variable map \(se(\varPi , id_\varDelta )\). The symbolic assignments in this map provide the state transition definitions for the state variables and the output terms for the output variables.

5.2 Encoding Regression Verification

The proof obligation handed to the symbolic model checker consists of a state transition system and a property that is to be proved as an invariant for it. The state transition system is a composition of the two systems that result from translating the two PLC program revisions P and Q and the models for the environment as introduced in Sect.  4.

All variables of the input spaces \(I_P\) and \(I_Q\) make up the input variables of the combined model. If \(\varDelta _P\) and \(\varDelta _Q\) share common input variables, these can also be shared in the combined model, thus reducing the input state space size.

If the sensor readings are constrained by an environment model, the input signals of that model are input signals of the entire state transition system while input signals of the PLC programs corresponding to sensor readings are taken from the outputs of the environment model. In the example environment model for the crane positions (Fig.  2), the PLC program takes the three inputs A, B, C from position sensors, while the composed verification model merely takes as input the indeterministic choice whether to remain in the current model state or whether to move on a step. This has two effects: (1) The input space size is reduced and (2) the modeling is more precise.

The condition \(\varphi \) from Definition  3 and the input and output relations \(\sim _{{in}}, \sim _{{out}}\) from Definition  4 make up the invariant that is part of the model checking proof obligation. In the current version of our toolchain, we require that the condition \(\varphi \) can be expressed in LTL by a formula of the form \(\mathbf{G }\,\psi \), where \(\psi \) is a propositional formula over the input variables in \(I_P\) without modal operators. That is, it must be possible to express the desired condition on the input sequence as a property of individual inputs. Correspondingly, we require that the relations \(\sim _{{in}}, \sim _{{out}}\) can be expressed by LTL formulas \({\sim _{{in}}} = \mathbf{G }\, \tau _{{in}}\) resp. \({\sim _{{out}}} = \mathbf{G }\, \tau _{{out}}\), where \(\tau _{{in}}\) and \(\tau _{{out}}\) are propositional formulas over the variables in \(I_P \cup I_Q\) resp. \(O_P \cup O_Q\). We then employ a fresh internal state variable \({pre}: {bool}\) to model the temporal condition within the invariant as follows:

$$\begin{aligned} \mathbf {init}({pre}) :={} {true}~(1) \quad \mathbf {next}({pre}) :={} {pre}\wedge \psi \wedge \tau _{{in}}~(2) \quad \mathbf {invariant}\ {pre}\rightarrow \tau _{{out}}~(3) \end{aligned}$$

The variable \({pre}\) is initialized to true (1) and is invalidated (2) as soon as input values violate either the condition (\(\psi \)) or the input relation (\(\tau _{{in}}\)). If the guarded invariant (3) holds for the transition system, then the equivalence of the two programs is guaranteed. What in fact is proved using the auxiliary variable \({pre}\) is the LTL property \( (\lnot \psi \vee \lnot \tau _{{in}})\ \mathbf{R \,}\tau _{{out}}\) stating that the output relation \(\tau _{{out}}\) must hold at least as long as neither the condition \(\psi \) nor the relation \(\tau _{{in}}\) have been violated (\(\mathbf{R \,}\) is the “release” operator of LTL). This entails relational equivalence between P and Q. All relations and conditions occurring in our case study fall into the restricted category of specifications described above. Although this is not implemented at the moment, other classes of LTL constraints can be used in our method by encoding them as invariants along the lines of [27].

5.3 Coupling Invariants

Modern model checkers allow the application of state abstraction methods (like IC3) to find proofs for safety properties more efficiently. Regression verification using symbolic model checkers with such abstractions is particularly promising since the two software revisions are closely related if the newer one results from the adaptation of the older one to a new application scenario. In such cases, it is likely that the old and the new version of the program have a similar – yet not necessary equal – encoding of their state spaces.

The upcoming abstraction theorem allows us to reason about safety properties of two PLC programs P and Q using an invariant \(\textit{Inv}: S_P \times S_Q \rightarrow {bool}\) over their state spaces \(S_P\) and \(S_Q\). Such a predicate, building a bridge between the state spaces, is called a coupling predicate.

Theorem 1

(Coupling Invariant Abstraction). We consider two PLC programs P and Q with common input space I, common output space O, and state spaces \(S_P\) and \(S_Q\). Let \(s_0 \in S_P\) and \(s_0' \in S_Q\) be the initial states.

Then, P and Q are (perfectly) trace equivalent if and only if there exists a coupling predicate \(\textit{Inv}: S_P \times S_Q \rightarrow {bool}\) such that, for all states \(s \in S_P, s' \in S_Q\) and inputs \(i\in I\),

\(\textit{Inv}(s_0, s'_0)\) holds, \(\textit{Inv}(s, s')\) implies \(\textit{Inv}(t, t')\), and \(\textit{Inv}(s, s')\) implies \(o=o'\),

where \((t,o) = \rho (P)(s,i)\) and \((t',o') = \rho (Q)(s',i)\).

Similar theorems can be formulated for relationally equivalent PLC programs.

The more similar the state space encodings of the old and the new program version are, the closer the coupling predicate is to equality on the state spaces. This becomes evident when a PLC program P is verified against itself. In this case, the equality relation itself can be used as coupling predicate and satisfies the conditions in Theorem  1 regardless of what P computes.

Development of PLC programs is often an incremental process, i.e., the new revision results from a modification of the code in the old version. Often, parts of the state are not affected by the changes (and behave like in the old revision) whereas other parts are affected. An inductive invariant implying equivalence then comprises equality between the unmodified state variables, and a more general coupling invariant must be generated only for the affected variables.

Fig. 4.
figure 4

Schematic of the hardware setup of the PPU case study [35].

Full size image

The regression verification method using invariants is complete, but the user of the verification tool would have to find and formalize all coupling invariants which can be large and unintuitive. Instead, we rely upon the capabilities of state-of-the-art symbolic model checkers to automatically infer inductive invariants. In our case, the required system invariant (3) (which usually is not inductive itself) is used as a starting point for an interpolant-based search for a stronger inductive invariant that implies the one given in the problem specification.

We show in our case study that even with large state spaces, this state abstraction mechanism allows us to prove equivalence of non-trivial programs. The model checker nuXmv is capable of coming up with the required coupling predicates using Incremental Construction of Inductive Clauses for Indubitable Correctness (IC3) [7, 24]. If this invariant generation mechanism is switched off, the tool relies on more traditional symbolic model checking techniques. Then, even the smaller ones of the problems in the case study could not be solved.

In cases where the search for an inductive invariant takes too long, parts of the coupling invariant can be specified manually (within (3)) – the workload for the invariant generation can thus be shared between user and model checker.

6 Case Study

We have evaluated our approach by applying it to the benchmark evolution scenarios of the Pick-and-Place Unit (PPU), which is illustrated in Fig.  4. The PPU is an open case study for the machine manufacturing domain [35]. Despite being a bench-scale, academic demonstration case, the PPU is complex enough to demonstrate selected challenges that arise during engineering of automated production systems. To explore evolution in this context, sixteen scenarios (i.e., variants of the PPU) covering different aspects of evolution have been defined [22, 36]. There are both pure software changes as well as changes that incorporate adaptations to the mechanics and automation hardware of the PPU.

For all of the scenarios developed for the PPU, both the structure and the behavior of the PPU are documented using the Systems Modeling Language (SysML) [35]. Also, IEC 61131-3 automation software code for the PLC is available for each evolution scenario – implemented in CODESYS2, an industrial development tool for automation software executable on PLCs. The PPU has 22 digital input, 13 digital output, and 3 analogue output signals and defines a number of simple discrete event automation tasks [33].

In the following, we discuss three evolution scenarios from the PPU and show how they can be subject to regression verification. More details can be found in [38]; see Table  1 for the time required for verification.

Conditional Equivalence. The evolution scenario Ev3 in [35] has been used as the introductory example in Sect.  2 in a much simplified version. In the full scenario, the new stamping hardware for metallic products brings with it a new emergency stop button \(E_2\) (triggering the same emergency logic as the existing button \(E_1\)) and a new start switch \({S}_{\text {3}}\) (complementing \({S}_{\text {1}}\) and \({S}_{\text {2}}\) already present). Only after all start switches have been pressed, the plant starts processing workpieces. Trace equivalence between the two revisions of this evolution step can only be shown for traces where these new components do not influence the flow of signals already present in the old software. This is the case if (1) no metallic workpiece is ever detected at M. (2) button \(E_2\) is only pressed if simultaneously \(E_1\) is also pressed, and (3) \({S}_{\text {3}}\) is not activated after the other switches \({S}_{\text {1}}\) and \({S}_{\text {2}}\) have been pressed. The LTL formula over the corresponding input variables for conditional equivalence of the PLC programs is \( \mathbf{G }(\lnot M ~\wedge ~(E_2 \rightarrow E_1) ~\wedge ~ (S_1 \wedge S_2 \rightarrow S_3)) \). Using this condition, equivalence can indeed be proved by our toolchain.

Relational Equivalence. In evolution step Ev14, the three position sensors at A, B and C are replaced by a single angle transmitter that continuously reports the angular position of the crane (in degrees). The input spaces for the PLC programs differ such that relational equivalence is to be shown here.

In correspondence with the hardware setup (see Fig.  4) and the requirements of the production system, we model the relation that binds the old Boolean position inputs A, B, C to the new angular input \(\alpha \) as

$$\begin{aligned} \mathbf{G }((A \leftrightarrow 0 \le \alpha \le 5) \wedge (B \leftrightarrow 90 \le \alpha \le 95) \wedge (C \leftrightarrow 180 \le \alpha \le 185)). \end{aligned}$$

In the thus defined input relation \(\sim _{{in}}\) each position switch corresponds to a \(5^\circ \) interval in the angular input space. This also shows that relations in our approach can be more complex than just a biunique mapping between values.

Using an Environment Model. In evolution scenario Ev6, the hardware remains unmodified, but the software is changed to optimize the handling of non-metallic workpieces (see [35] for details). The PLC programs before and after the optimization should be equivalent for traces where only metallic or only non-metallic workpieces are detected, but the programs are not equivalent. An inspection of the code reveals that a condition within an SFC has been reformulated. As a first guess one could assume that the two conditions are equivalent and use this as condition for the conditional equivalence proof. Indeed, the equivalence proof succeeds using that assumption (Ev6+A for both cases, Ev6+A\(_\mathrm{{m}}\) for metallic and Ev6+A\(_\mathrm{{nm}}\) for non-metallic pieces only). However, using an ad-hoc assumption about the input state is not satisfactory even if it could be justified by a manual inspection. Instead, a more intuitive and convincing item, an environment model of the crane (essentially the one shown in Fig.  2) can be added, using which the PLC programs are proven equivalent with (Ev6+AEM) and even without the assumption (Ev6+EM).

Results. Using our method and toolchain, automatic regression verification was successful for all scenarios from the PPU case study. Table  1 shows statistics for our experiments. The evolution scenarios were verified using nuXmv version 1.0.1 on an Intel Dual-Core with 2.7 GHz and 4 GB RAM running OpenSUSE 12.2.

Not all evolution scenarios include a modification of the software. The scenarios for which the equivalence verification is trivial have been omitted from the table. The verification times for the same problem on the same machine may vary considerably in multiple runs due to random choices in the symbolic model checker which have a great impact on the verification time.

The regression verification method can not only be used for verifying equivalence of PLC programs up to intended differences, but unintentional differences between programs can also be found using our approach. The evaluation of our approach revealed a few unintentional regressions in the PPU. In four cases, new intermediate code blocks are added into SFCs that cause a regression by delaying the system answer one cycle for each workpiece. Since the cycle time is very short in the PPU (4 ms), the discrepancy between the programs was not found by testing. Moreover, regression verification discovered that a fix for a safety violation was not applied to an earlier version in the PPU evolution sequence. It is possible that the crane tries to grab a workpiece while it is still in motion which might under very unfortunate circumstances cause damages.

Table 1. Results of the experiments. scenario is the name of the evolution scenario in [35], in is the size of the sensor input space in bits, state the size of the state space in bits, min/max show the minimum and maximum time needed for verification using nuXmvin seconds (s), minutes (m) or hours (h). +EM indicates that an environment model has been used.
Full size table

7 Related Work

The verification of PLC programs w.r.t. temporal logic specifications (for safety, liveness, and time properties) has been subject of a number of publications already. The paper [40] gives an overview of the field, and the survey [21] discusses transformation processes for program languages to verifiable models. Various translations from IEC 6113-3 languages into the input languages of model checkers have been presented: Brinksma et al. [8] present a translation of SFCs into Promela input for the SPIN model checker [17]; De Smet et al. [28] translate all languages within IEC 61131-3 into input for the symbolic model checker Cadence-SMV [25]; and Bauer et al. [3] translate SFCs into timed automata to be used with UPPAAL [5]. This model checker is also used to verify properties of continuous function charts (CFC) in [37]. In [4, 6] a unifying semantics for SFC is given where the ambiguities of the standard are addressed in a formal fashion.

Süflow and Drechsler [30] present a framework to verify that the same program behaves equivalently on different PLC platforms; a scenario closely related to ours. The authors employ a SAT solver to verify the arising proof conditions.

Strichman and Godlin [13–15, 29] coined the term regression verification and presented a verification methodology based on replacing function calls by uninterpreted function symbols within a bounded software model checking framework for C programs. In [13] they define “reactive equivalence,” which is closely related to our notion of perfect trace equivalence. In earlier work [11], we presented an automated approach to regression verification based on invariant generation using Horn clauses. Many other approaches [2, 16, 31, 32, 39] exist on regression verification for imperative programming languages.

Equivalence checking is an established issue for the verification of hardware circuits. In sequential equivalence checking the perfect trace equivalence between clocked circuits is analysed; see [18] or [20] for an overview. Lu and Cheng [23] present an approach based on inferred invariants, conditional or relational equivalence are not considered.

8 Conclusion and Future Work

We have presented a method and toolchain for the automatic regression verification of PLC software by means of a symbolic model checker. In this process, the old software revision serves as specification for the new one. Conditions can be specified under which systems must behave equivalently, relations can be specified how the equivalence is to be understood, and models of environment can be added to make the process more precise.

Evaluation proved our method to be applicable to non-trivial PPC software. Automatic regression verification was successful for all scenarios from the PPU case study. The evaluation also showed that the use of \(\varPhi \)-nodes in the translation from PPU code to model checking input as well as the automatic generation of coupling invariants is indispensable for non-trivial programs.

Currently, our toolchain supports notions that compare PLC behavior cycle by cycle. Future work will allow for conditions and relations to relate variables of different cycles. Another interesting path of investigation is the use of abstractions to factor out parts of PLCs that have not been touched by evolution and need not be proved equivalent.