# Conformity of Ladder Programs against State Transition Diagrams

Denis Cousineau, Hiroaki Inoue, Claude Marché, Florian Faissole, David Mentré

► To cite this version:

Denis Cousineau, Hiroaki Inoue, Claude Marché, Florian Faissole, David Mentré. Conformity of Ladder Programs against State Transition Diagrams. RR-9584, Inria. 2025, pp.31. hal-05001069

HAL Id: hal-05001069

https://inria.hal.science/hal-05001069v1

Submitted on 24 Mar 2025

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
<figure><img src="image_2.png" /></figure>

RÉPUBLIQUE
FRANÇAISE

Liberté
Égalité
Fraternité

Inria

# Conformity of Ladder Programs against State Transition Diagrams

Denis Cousineau, Hiroaki Inoue, Claude Marché, Florian Faisole, David Mentré

## RESEARCH REPORT

N° 9584

March 2025

Project-Team Toccata

ISSN 0249-6399

ISRN INRIA/RR-9584-FR+ENG
<figure><img src="image_3.png" /></figure>
<figure><img src="image_4.png" /></figure>

RÉPUBLIQUE
FRANÇAISE

Liberté
Égalité
Fraternité

Inria

# Conformity of Ladder Programs against State Transition Diagrams*

Denis Cousineau†, Hiroaki Inoue‡, Claude Marché§, Florian Faissole†, David Mentré†

Project-Team Toccata

Research Report n° 9584 — March 2025 — 28 pages

**Abstract:** Programmable logic controllers (PLC) are industrial digital computers used as automation controllers of manufacturing processes, such as assembly lines or robotic devices. The Ladder language, also known as Ladder Logic, is a programming language used to develop PLC software. Because of their widespread usage in industry, verifying that Ladder programs conform to their expected behavior is of critical importance.

In this work, we consider the description of the expected behavior under the form of a *state transition diagram*, describing scenarios of execution. Our approach consists in translating the Ladder code and the diagram into a program for the Why3 environment dedicated to deductive program verification. The verification proceeds by generating formal verification conditions, which are mathematical statements to be proved valid using automated theorem provers.

The ultimate goal is two-fold: first, by obtaining a complete proof, we can verify the conformity of the Ladder code with respect to the state transition diagram with a high degree of confidence. Second, when the proof is not fully completed, we obtain a counterexample, illustrating an execution scenario of the Ladder code which does not conform to the diagram.

**Key-words:** Formal specification, Deductive verification, Ladder language for programming PLCs, Why3 environment for deductive verification, State Transition Diagrams.

RESEARCH CENTRE
SACLAY - ÎLE-DE-FRANCE

1 rue Honoré d'Estienne d'Orves
Bâtiment Alan Turing
Campus de l'École Polytechnique
91120 Palaiseau

<footnote>* This work has been partially supported by the bilateral contract ProofInUse-MERCE between Inria team Toccata and Mitsubishi Electric R&D Centre Europe, Rennes.</footnote>

<footnote>† Mitsubishi Electric R&D Centre Europe, Rennes, France</footnote>

<footnote>‡ Mitsubishi Electric Corporation, Amagasaki, Japan</footnote>

<footnote>§ Université Paris-Saclay, CNRS, Inria, LMF, 91190, Gif-sur-Yvette, France</footnote>
# Analyse automatique de conformité de codes Ladder vis-à-vis de diagrammes états-transitions

**Résumé** : Les automates industriels programmables (Programmable Logic Controllers, PLC en abrégé) sont des dispositifs numériques industriels utilisés pour contrôler les processus de fabrication automatisés, tels que les lignes d'assemblage ou les robots de toute sorte. Le langage Ladder, également connu sous le nom de Ladder Logic, est un langage de programmation utilisé pour développer des logiciels pour PLC. Du fait de leur utilisation très répandue dans l'industrie, vérifier que les programmes Ladder sont conformes à leur comportement attendu est d'une importance cruciale.

Dans ce travail, nous considérons une description du comportement attendu sous la forme d'un *diagramme états-transitions* (State Transition Diagram, en abrégé STD), décrivant l'ensemble des scénarios d'exécution. Notre approche consiste à traduire le code Ladder et le diagramme en un programme pour l'environnement Why3 dédié à la vérification déductive des programmes. La vérification se déroule en générant des conditions formelles de vérification, qui sont des énoncés mathématiques destinés à être prouvés valides à l'aide de prouveurs automatiques de théorèmes.

Le but ultime est double : premièrement, en obtenant une preuve complète, nous pouvons vérifier la conformité du code Ladder par rapport au STD avec un degré élevé de confiance. Deuxièmement, lorsque la preuve n'est pas entièrement complétée, nous obtenons un *contre-exemple*, illustrant un scénario d'exécution du code Ladder qui n'est pas conforme au diagramme.

Ces recherches ont été partiellement financées par le contrat bilatéral ProofInUse-MERCE entre l'équipe Inria Toccata et Mitsubishi Electric R&D Centre Europe, à Rennes.

**Mots-clés** : Spécification formelle, preuve de programmes, langage Ladder pour la programmation des PLC, environnement Why3 pour la vérification déductive, diagrammes états-transitions.
# Contents

<table><tr><td>1</td><td>Introduction</td><td>5</td></tr><tr><td>2</td><td>Introduction to Ladder Programming</td><td>6</td></tr><tr><td>2.1</td><td>Ladder Logic</td><td>6</td></tr><tr><td>2.2</td><td>Specification of Expected Behavior using State Transition Diagrams</td><td>6</td></tr><tr><td>3</td><td>The Why3 Environment</td><td>8</td></tr><tr><td>3.1</td><td>Automatic Generation of Loop Invariants</td><td>9</td></tr><tr><td>3.2</td><td>Generation of Counterexamples</td><td>10</td></tr><tr><td>4</td><td>Translation of Ladder code and STDs to WhyML</td><td>11</td></tr><tr><td>4.1</td><td>Translation of the Ladder program</td><td>12</td></tr><tr><td>4.2</td><td>The Ladder loop and State Transition Diagrams</td><td>13</td></tr><tr><td>4.2.1</td><td>Cyclic execution</td><td>13</td></tr><tr><td>4.2.2</td><td>States, Transitions and Input Value Changes</td><td>13</td></tr><tr><td>5</td><td>Implementation and Experimental Results</td><td>18</td></tr><tr><td>5.1</td><td>Overview of the Implementation Approach</td><td>18</td></tr><tr><td>5.2</td><td>Results on correct code</td><td>20</td></tr><tr><td>5.3</td><td>Results on incorrect code</td><td>22</td></tr><tr><td>6</td><td>Discussions, Related Work and Future Work</td><td>25</td></tr></table>
List of Figures

<table><tr><td>1</td><td>Ladder code for the 2HANDS_TIMER example.</td><td>6</td></tr><tr><td>2</td><td>State Transition Diagram of 2HANDS_TIMER example.</td><td>7</td></tr><tr><td>3</td><td>Toy example of a WhyML program with formal specifications.</td><td>8</td></tr><tr><td>4</td><td>Intermediate syntax for the 2HANDS_TIMER STD of Figure 2.</td><td>11</td></tr><tr><td>5</td><td>WhyML global variables for the devices and the timer.</td><td>12</td></tr><tr><td>6</td><td>WhyML function modeling the SET instruction.</td><td>12</td></tr><tr><td>7</td><td>WhyML code modeling Ladder timers.</td><td>13</td></tr><tr><td>8</td><td>WhyML code modeling one scan of the 2HANDS_TIMER program.</td><td>13</td></tr><tr><td>9</td><td>WhyML Boolean variables modeling the states of the STD.</td><td>14</td></tr><tr><td>10</td><td>Abstract WhyML function modeling non-deterministic changes of input values.</td><td>14</td></tr><tr><td>11</td><td>WhyML Boolean variable modeling the abstract timer of the STD.</td><td>14</td></tr><tr><td>12</td><td>Abstract function for transitions (part 1).</td><td>15</td></tr><tr><td>13</td><td>Abstract function for transitions (part 2).</td><td>16</td></tr><tr><td>14</td><td>WhyML code for multiple scans of the 2HANDS_TIMER program.</td><td>17</td></tr><tr><td>15</td><td>Output of the tool on the nominal 2HANDS_TIMER program.</td><td>20</td></tr><tr><td>16</td><td>The loop invariant automatically generated by Why3.</td><td>21</td></tr><tr><td>17</td><td>Some incorrect variant of Ladder code for 2HANDS_TIMER.</td><td>22</td></tr><tr><td>18</td><td>WhyML program modeling two unrolling of execution of the original program loop.</td><td>23</td></tr><tr><td>19</td><td>First step of execution of the error scenario.</td><td>24</td></tr><tr><td>20</td><td>Last step of execution of the error scenario.</td><td>24</td></tr></table>
# 1 Introduction

Programmable logic controllers (PLC) are industrial digital computers used as automation controllers of manufacturing processes, such as assembly lines or robotic devices. PLCs can simulate the hard-wired relays, timers and sequencers they have replaced, via software that expresses the computation of outputs from the values of inputs and internal memory. The Ladder language, also known as Ladder Logic, is a programming language used to develop PLC software. This language uses circuit diagrams of relay logic hardware to represent a PLC program by a graphical diagram. This language was the first available to program PLCs, and is standardized since 2013 in the IEC 61131-3 standard [26]. It is one language among other languages for programming PLCs, and is widely used and very popular among technicians and electrical engineers.

Because of the widespread usage of PLCs in industry, verifying that a given Ladder program is conforming to its expected behavior is of critical importance. In this work, we consider the description of the expected behavior under the form of a *state transition diagram*, abbreviated as STD, describing scenarios of execution. Our approach consists in automatically translating the Ladder code and the STD into a program written in the WhyML language, which is the input language of the Why3 environment for deductive program verification. In WhyML, expected behaviors of program are expressed using *contracts*, which are annotations expressed in formal logic. The Why3 environment offers tools for checking that the WhyML code conforms to these formal contracts. This verification process is performed using automated theorem provers, so that at the end, if the back-end proof process succeeds, the conformity of the Ladder code with respect to the STD is verified with a high degree of confidence. Yet, a complete formal proof is not the only expected feedback from our tool chain: we also want to obtain useful feedback when the proof does not fully succeed. More precisely, in such a case of proof failure, we aim at obtaining a *counterexample* which must illustrate an execution scenario of the Ladder code which does not conform to the STD.

In the remaining of this report, we start in Section 2 by introducing the basics of Ladder programming, and the way their expected behaviors are expressed using STDs. In Section 3 we introduce the Why3 features that are needed for the translation of Ladder code and STDs into WhyML programs, which is described in Section 4. Section 5 presents our experiments and their results, both in the case of complete proof success and in the case of proof failures, where counterexamples are generated. We present related work and future work in Section 6.
<figure><img src="image_5.png" /><figcaption>Figure 1: Ladder code for the 2HANDS_TIMER example.</figcaption></figure>

# 2 Introduction to Ladder Programming

## 2.1 Ladder Logic

A Ladder program (a *diagram*) takes inputs values (*contacts*) that correspond to the fact that physical relays are either wired, not wired, pulsing (rising edge) or downing (falling edge), and other values stored in the internal memory of the PLC (Boolean values, integers, floating-point, strings, etc.). A Ladder program can output Boolean values to the physical relays of the factory (*coils*) or it can call instructions, that may modify the values of the internal memory of the PLC (*devices*). Graphically, contacts are located at the left of the diagram. They can be combined in a serial way or in a parallel way, the obtained value being then the conjunction, resp. the disjunction, of the two contact values. Coils and instructions are activated when the combination of contacts at their left gives a wired value, and they can also be parallelized (in that case, there are either all activated or all deactivated). A line with contacts, coils and instructions is called a *rung*, and a program is composed of several rungs. Such a Ladder program is executed cyclically in a synchronous way: first inputs are read, then the program is executed and eventually outputs are written. One single execution of the program is called a *scan*.

In this report, we use as running example a simplified version of a safety Ladder program that can be found in Mitsubishi Electric's documentation [23]. In this system, which we call 2HANDS_TIMER, we consider two inputs buttons ($X_0$ and $X_1$), and one output ($Y_0$). The principle behind this device is a safety of activation of the output, where the two buttons should be actuated simultaneously (one with each hand actually) and during a large enough amount of time (that corresponds to 30 scans, roughly 3 seconds), before the output $Y_0$ is activated.

We can implement this system with the simple program given in Figure 1. The first rung of the program expresses that when both input devices $X_0$ and $X_1$ are active, the timer device $T_0$ is incremented, with a threshold set to 30 (and otherwise, the timer $T_0$ should be reset). The second rung implements the fact that if $T_0$ has reached its threshold, then instruction SET is called on output device $Y_0$.

## 2.2 Specification of Expected Behavior using State Transition Diagrams

In a former work [5], we studied the verification of conformity of Ladder programs with respect to a particular form of specifications called *timing-charts*. Timing-charts detail a specification of expected output values, given a scenario of input values along time. In this report, we focus on a more general kind of specification, namely *State Transition Diagrams* (STD). An STD can be viewed as a (timed) state machine where transitions are triggered by input values given to the program, and expected output values are given as invariants of the different states. With respect to timing charts, an STD is intended to describe *all* intended scenarios of execution, instead of only one.

An example of such an STD is given in Figure 2. It describes the expected behavior of the running example 2HANDS_TIMER. It contains 5 states named $S_0$ to $S_4$, where $S_0$ is the *initial* state. Transitions are depicted as arrows between states, with labels that express the *condition* of the transition. Such a condition is expressed by saying which of the input values are changed, together with optional timing
<figure><img src="image_6.png" /><figcaption>Figure 2: State Transition Diagram of 2HANDS_TIMER example.</figcaption></figure>

information, as is the transition from $S_3$ to $S_4$ in Figure 2. In the initial state $S_0$, both inputs $X_0$ and $X_1$ are false. If $X_0$ becomes true (and $X_1$ stays false) then the system reaches state $S_1$. Otherwise, if $X_1$ becomes true (and $X_0$ stays false) then it reaches state $S_2$. If both $X_0$ and $X_1$ become true, then it reaches state $S_2$. Transitions from a state to itself are implicit (if no input changes, the system stays in the current state). We call the transition from $S_3$ to $S_4$ a *timed transition* since its triggering condition depends on time: it becomes true after thirty consecutive executions in $S_3$.

Invariants are shown in diamond-shaped boxes in states. In this example, there is only one output $Y_0$. The STD states that it should be false in all states except $S_4$, in which it should be true.
```h
val s0 : ref bool
val s1 : ref bool
val s2 : ref bool
val c : ref int

val random_bool () : bool

let toy ()
    requires { !s0 ^ not !s1 ^ not !s2 ^ !c = 0 }
    diverges
    writes { s0, s1, s2, c }
= while not !s2 do
    if !s1 then c := !c +1;
    let tmp = random_bool () in
    if !s0 && tmp then
        (s0 := False; s1 := True; c := 0)
    else
        if (!s1 && (!c > 42)) then (s1 := False; s2 := True)
    done;
    assert { !c >= 43 }
```

<caption>Figure 3: Toy example of a WhyML program with formal specifications.</caption>

## 3 The Why3 Environment

Why3 is an environment for deductive program verification (see http://www.why3.org), providing the language WhyML for specification and programming [17, 8, 18]. It is a generic environment in several ways. First, WhyML is used as an intermediate language for verification of programs written in C, Java, Ada [16, 20] and Rust [14]. The specification component of WhyML [7], used to write program annotations and background theories, is an extension of first-order logic. The specification part of the language serves as a common format for theorem proving problems, *proof tasks* in Why3's jargon. Why3 generates proof tasks from user lemmas and annotated programs, using a weakest-precondition calculus, then dispatches them to multiple provers. It is another aspect of the genericity of Why3: its ability to dispatch proof tasks to many different provers. In practice, for the proof of programs, provers of the SMT (*Satisfiability Modulo Theories*) family are the most successful ones, indeed at least if they support quantified formulas, which is the case for Alt-Ergo [9], CVC4 [2], cvc5 [1] and Z3 [13].

We illustrate the main Why3 features we need on a toy WhyML program presented in Figure 3. This code involves four global variables, `s1`, `s2` and `s2` of type Boolean and `c` of type `int`, that is a mathematical, unbounded integer in WhyML. The function `toy` takes no arguments, and is equipped with a *formal contract*. This construct first includes a pre-condition (introduced by keyword `requires`) stating that function entrance `s0` is true, `s1` and `s2` are false and `c` is 0. The contract also includes the clause `writes` that expresses which global variables are potentially modified by that function. Notice the WhyML syntax for mutable variables, inspired by OCaml, requiring to write a bang symbol to access their values. The body of that function is a simple imperative code involving a while loop, conditional statements and assignments. This code also includes a call to the function `random_bool` which is declared *abstractly*, that is without body, so that as is, it may return any Boolean value, non-deterministically. This code ends by an other kind of formal annotation, namely a code `assertion` stating that the value of `c` must
be greater than or equal to 43 after the loop.

Given such an annotated code, the Why3 core engine generates a *verification condition* (VC for short), corresponding to the assertion. It is a mathematical formula that, if proven valid, guarantees that the assertion will hold for any execution of the program. In the Why3 environment, external provers are called to attempting to prove this VC valid, but here none of them succeeded. This is naturally expected in the classical setting of deductive verification, because for proving properties of programs involving loops, one should state appropriate *loop invariants*. For example, we can add such an invariant in our toy example as follows:

```
...
= while not !s2 do
    invariant { !s2 → !c >= 43 }
...
```

With that change, Why3 now generates no less than eight VCs, stating that this invariant initially holds when entering the loop, and that it is preserved by an arbitrary iteration of the loop body, which contains six different paths of execution, hence six VCs. The last VC remain for proving the assertion, but this time with the extra knowledge that the invariant holds at loop exit. All these eight VCs are proved valid using external provers.

For the work presented here, we make use of two specific and still quite recent and advanced features of Why3, namely the capability of *automatically generating loop invariants* [21], and the capability of *generating counterexamples* [3] from failed proof attempts.

## 3.1 Automatic Generation of Loop Invariants

The WhyML code that will be automatically generated from Ladder code and an associated STD is a single while loop, whose body operates on quite a large number of variables. As seen above, and as usual in deduction-based program verification, proving those programs with loops require to insert appropriate loop invariants, that in principle should be written by the user.

Nevertheless, in the context of this paper, the objective is to build a fully automatic tool for bringing deductive verification of STD specifications to Ladder developers, for whom writing the appropriate loop invariants by hand would be a tedious and difficult task. Fortunately, there exist methods to automatically infer such invariants, in particular the technique of *abstract interpretation*, which roughly consists in computing an over-approximation of all the reachable program states, from any possible execution. For our work, we built upon the prototype of automatic invariant generation inside Why3 that we designed earlier for timing chart verification [21]. This prototype uses a special form of BDD (*binary decision diagram*) combined with the Apron [19] library to support linear integer abstraction domains. The use of BDDs is crucial for handling Boolean variables.

We illustrate that process on our toy example above. Instead of adding a loop invariant, we instruct Why3 to use abstract interpretation to automatically infer such a loop invariant. In practice we have to annotate the function declared with the attribute `bddinfer`.

```
let toy [@bddinfer] ()
    requires { ... }
...
```

The generated loop invariant is then as follows:

```
...
while not !s2 do
    invariant {
        if !s2 = True then !s1 = False ^ !s0 = False ^ 43 <= !c
    }
...
```
```pascal
else if !s1 = True then !s0 = False ∧ 0 <= !c ∧ !c <= 42
else !s0 = True ∧ !c = 0
}
...
```

With this loop invariant added, all the VCs generated are automatically proved valid, including the initialization and preservation of that loop invariant, and also the assertion after the loop.

Essentially, it is to be noted that the loop invariant quite precisely covers the different states of the program, and it is in particular sufficient to prove the final assertion, avoiding the user the burden of adding its own invariant.

## 3.2 Generation of Counterexamples

When a given proof task fails to be proved, we need to have some feedback so as to understand why it is not proved. In Why3, when a proof is attempted with an SMT solver, and the goal is not proved, then the solver is able to propose a *model*, which is supposed to contradict the goal. The Why3 core implements an approach that turns such a model, expressed at the level of the proof task, back to a *potential counterexample* expressed at the level of the WhyML source code [12, 3].

Let's illustrate this feature again on our toy example. Assume that we introduce a modification of the code, changing the final assertion as follows.

```pascal
assert { !c >= 53 }
```

Still assuming that we ask to generate a loop invariant using bddinfer, all generated VCs are proved except the assertion itself. For this VC, Why3 proposes a counterexample where the values of variables at loop exit are respectively false for `s0` and `s1`, true for `s2` and 43 for `c`, so the user is reasonably informed that in their program, the value of `c` when the assertion is reached can be 43 and thus not larger or equal to 43.

Similarly, let's modify the original toy example by changing the line

```pascal
if !s0 && tmp then
  (s0 := False; s1 := True; c := 0)
```

into

```pascal
if !s0 && tmp then
  (s0 := False; s2 := True; c := 0)
```

In that case, the assertion is again not proved, and the counterexample proposed is false for `s0` and `s1`, true for `s2` and 0 for `c`, exhibiting the fact the loop is exited too early.

Notice that for the use of this feature to our use case of verifying Ladder code, there is a challenge to address, that is to turn the potential counterexample proposed by Why3 into a meaningful counterexample at the level at the Ladder code and the STD. This challenge is addressed below in Section 5.3.
```
@start
'vars
input : x0 x1;
output : y0;

'states
s0 : !y0; x0 x1;
s1 : !y0; x0 x1;
s2 : !y0; x0 x1;
s3 : !y0; x0 x1;
s4 : y0; ;

'init
[*] --> s0 : !x0 !x1;

'transitions
s0 --> s3 : x0 & x1;
s0 --> s1 : x0;
s0 --> s2 : x1;
s1 --> s3 : x1 ;
s1 --> s2 : !x0 & x1;
s1 --> s0 : !x0 ;
s2 --> s3 : x0 ;
s2 --> s1 : !x1 & x0;
s2 --> s0 : !x1 ;
s3 -[ 30 ]-> s4 : ;
s3 --> s0 : !x0 & !x1;
s3 --> s2 : !x0;
s3 --> s1 : !x1;

@end
```

<caption>Figure 4: Intermediate syntax for the 2HANDS_TIMER STD of Figure 2.</caption>

## 4 Translation of Ladder code and STDs to WhyML

We designed and implemented an automated translation scheme to turn a given Ladder program, associated with an STD, into a WhyML program. As it was described in our work on timing charts [4, 5], Ladder programs are parsed from an XML representation exported by Mitsubishi Electric's IDE GX Works 3 [23]. To ease our translation scheme, we defined an intermediate syntax for describing STD. That syntax is illustrated in Figure 4 for our running example, from the STD of Figure 2.

That syntax is mostly self-explanatory, with four sections defining respectively the variables, the states, the initial state and the transitions. In the section 'states, the name of each state is accompanied first with the invariant, and then the list of input variables that can change when in that state. In our simple example, it is not so meaningful since, except in state s4, we suppose that both inputs can change between any two executions. But it can be mandatory for more complex examples involving environment hypotheses on input changes. Note also that in section 'transitions, the order of lines is important
```hml
val x0 : ref bool
val x1 : ref bool
val y0 : ref bool
val t0current : ref int
val t0setting : ref int
```

<caption>Figure 5: WhyML global variables for the devices and the timer.</caption>

```hml
let set (input : bool) (device : ref bool) : unit
    writes { device }
    ensures { !device ↔ (input ∨ old !device) }
    = if input then device := true
```

<caption>Figure 6: WhyML function modeling the SET instruction.</caption>

regarding the transition conditions (at the end of each line): the previous conditions are assumed not to hold. For example, in the second transition starting from `s0`, the condition is `x0` but it is also assumed that the previous condition for `s0`, namely `x0 & x1`, does not hold, in other words `x1` must be false.

We recall in Section 4.1 how we translate the Ladder program itself, and we describe in Section 4.2 how we use this translation for modeling the successive executions of the program and verifying that it satisfies the given STD.

## 4.1 Translation of the Ladder program

We propose an imperative formalization, in which all devices (inputs, outputs, timers, local memory, etc...) are modeled as WhyML global mutable variables. This is illustrated in Figure 5 for our running example. Timers are modeled by two integer variables, as detailed below.

Our translation relies on predefined models of Ladder instructions as WhyML functions. For example, Figure 6 depicts the function that corresponds to the SET instruction. This function takes two arguments, first the input of the instruction (whether it should be activated or not), and second the device on which it may have an effect. Both the code and the contract of the function state the intended behavior of the SET function: if the instruction is activated then the considered device is activated (otherwise its value does not change).

In Figure 7, we describe how we model timers. Each timer is translated into two integer variables, e.g. `t0current` and `t0setting`. We model the timer instruction with the `timer_coil` function. As for Ladder timers, this instruction, when activated, sets the threshold of the timer and increment its counter. When it is deactivated, it resets the counter to zero (remind that the timer instruction should be activated during a number of consecutive scans that correspond to the threshold, for the timer to end). The `timerContact` function models the fact that the timer device is activated when its counter reaches its threshold value.

The former elements of our formalization of Ladder instructions are sufficient to construct the translation of the Ladder program of Figure 1, which is given in Figure 8. See [5] for more details on the translation scheme for Ladder code.
let timer_coil (input : bool) (tcurrent : ref int) (tsetting : ref int) (v : int) : unit
writes { tcurrent, tsetting }
ensures { !tsetting = v }
ensures { (input ∧ !tcurrent = (old !tcurrent +1) )
  ∨ (not input ∧ !tcurrent = 0) }
= tsetting := v;
  if input then tcurrent := !tcurrent + 1 else tcurrent := 0

let timerContact (tcurrent : ref int) (tsetting : ref int) : bool
ensures { result = (!tcurrent >= !tsetting) }
= return (!tcurrent >= !tsetting)

<caption>Figure 7: WhyML code modeling Ladder timers.</caption>

let common_1 = !x0 && !x1 in
timer_coil common1 t0current t0setting 30;
let common_2 = timer contact !t0current !t0setting in
set common_2 y0

<caption>Figure 8: WhyML code modeling one scan of the 2HANDS_TIMER program.</caption>

## 4.2 The Ladder loop and State Transition Diagrams

Our objective is to provide a WhyML formalization that allows to prove that a Ladder program satisfies an STD specification, or to explicit an error scenario when it is not the case.

### 4.2.1 Cyclic execution

In the translation of timing-charts [4, 5], we chose to encode timing-chart specifications as consecutive while-loops where guard conditions were the input values that would make the system transition to the next state. It was convenient to accommodate the relative inefficiency of the first implementation of Why3's loop invariant generation feature. But it is not adapted to the verification of STDs, in which execution paths in states are not necessary just single linear paths: there can be two transitions that target different states from a same state, states can be reached several times in an execution path, etc.

Thanks to recent improvements in performance of Why3's loop invariant generation feature, we can rely on a new formalization for STD that uses only one infinite loop, Boolean variables to describe the current state, and an *abstract* WhyML function (that is, a function with a contract but no body, as the `random_bool` function of Figure 3) to model non-deterministic transitions between states.

### 4.2.2 States, Transitions and Input Value Changes

We model the current state of the considered STD with a Boolean variable for each state, as shown in Figure 9, and we specify that exactly one of them is true at each step of execution. Notice that this modeling is better than, say, a unique integer variable recording the current state, as Boolean variables are much better suitable for the loop invariant generation based on BDDs.
```pascal
val s0 : ref bool
val s1 : ref bool
val s2 : ref bool
val s3 : ref bool
val s4 : ref bool
```

<caption>Figure 9: WhyML Boolean variables modeling the states of the STD.</caption>

```pascal
val input_change () : ()
writes { x0, x1 }
```

<caption>Figure 10: Abstract WhyML function modeling non-deterministic changes of input values.</caption>

```pascal
val t_s3_s4 [@model] [@model_trace:t_s3_s4] : ref bool
```

<caption>Figure 11: WhyML Boolean variable modeling the abstract timer of the STD.</caption>

The transitions, as well as the possible changes of input values are expressed as post-conditions of an abstract function modeling state change. In our simple running example, both inputs $X_0$ and $X_1$ can have their values modified between any step of execution. So the only post-condition we specify is the fact that predicate `input_change` can write both $X_0$ and $X_1$ as shown in Figure 10. More complex STD can specify different changes of input values depending on the current state, for formalizing, e.g. environment hypotheses that specify that some sequences of input changes are physically impossible. In that case, we can provide more precise post-conditions as we do below for transitions.

We express transitions as a single post-condition of another abstract function named `transition`. This post-condition expresses at once all possible transitions, given the current state before execution and possibly other conditions. To handle timed transitions, we define a Boolean variable for each of them (here `t_s3_s4` as in Figure 11 for the transition between $S_3$ and $S_4$), and use them in the conditions of those timed transitions. We might call those variables *abstract counters* (for differentiation from *concrete counters* in the code, like $T_0$ in our example program).

We detail the abstract function `transition` for our running example in Figure 12 and Figure 13. The pre-condition specifies that exactly one of the state Boolean variables is true before execution. The post-condition is a large disjunction of formulas, each of these formula representing one possible transition. For example, lines 10 to 25 of Figure 12 describe all the transitions from state $S_0$. Lines 10 to 13 specify the implicit self-transition (if $X_0$ and $X_1$ are not actuated then we stay in $S_0$ and the value of the abstract counter `t_s3_s4` is left unchanged). Other transitions are formalized the same way. Concerning the abstract counter `t_s3_s4` for the timed transition from $S_3$ to $S_4$, we emphasize that:

* it is initialized to 1 in all transitions leading to $S_3$ from another state (see lines 25, 42 and 59)

* it is incremented in the implicit transition from $S_3$ to itself (line 76)

* its value is used to decide transition to $S_3$ or to $S_4$ from $S_3$ (lines 74 and 78)

We can finally model the behavior of multiple scans of the Ladder program w.r.t. the STD, as shown in Figure 14. We define a WhyML function `pgm_2hands_timer`. Note the `@bdd-infer` attribute to ask
```c
1  val transition () : ()
2  writes { s0, s1, s2, s3, s4 }
3  writes { t_s3_s4, state changed }
4  requires { old !s0 ∧ not (old !s1) ∧ not (old !s2) ∧ not (old !s3) ∧ not (old !s4) (* State: s0 *)
5    ∨ not (old !s0) ∧ old !s1 ∧ not (old !s2) ∧ not (old !s3) ∧ not (old !s4) (* State: s1 *)
6    ∨ not (old !s0) ∧ not (old !s1) ∧ old !s2 ∧ not (old !s3) ∧ not (old !s4) (* State: s2 *)
7    ∨ not (old !s0) ∧ not (old !s1) ∧ not (old !s2) ∧ old !s3 ∧ not (old !s4) (* State: s3 *)
8    ∨ not (old !s0) ∧ not (old !s1) ∧ not (old !s2) ∧ not (old !s3) ∧ old !s4 (* State: s4 *)
9  ensures { (* transitions from state s0 *)
10    old !s0 ∧ not (old !s1) ∧ not (old !s2) ∧ not (old !s3) ∧ not (old !s4) (* Source: s0 *)
11    ∧ not !x0 ∧ not !x1 (* Guard: no button pressed *)
12    ∧ !s0 ∧ not !s1 ∧ not !s2 ∧ not !s3 ∧ not !s4 (* Target: s0 *)
13    ∧ !t_s3_s4 = old !t_s3_s4 (* Action: t_s3_s4 unchanged *)
14    ∨ ( old !s0 ∧ not (old !s1) ∧ not (old !s2) ∧ not (old !s3) ∧ not (old !s4) (* Source: s0 *)
15    ∧ !x0 ∧ not !x1 (* Guard: button x0 pressed but not x1 *)
16    ∧ not !s0 ∧ !s1 ∧ not !s2 ∧ not !s3 ∧ not !s4 (* Target: s1 *)
17    ∧ !t_s3_s4 = old !t_s3_s4 (* Action: t_s3_s4 unchanged *)
18    ∨ ( old !s0 ∧ not (old !s1) ∧ not (old !s2) ∧ not (old !s3) ∧ not (old !s4) (* Source: s0 *)
19    ∧ not !x0 ∧ !x1 (* Guard: button x1 pressed but not x0 *)
20    ∧ not !s0 ∧ not !s1 ∧ !s2 ∧ not !s3 ∧ not !s4 (* Target: s2 *)
21    ∧ !t_s3_s4 = old !t_s3_s4 (* Action: t_s3_s4 unchanged *)
22    ∨ ( old !s0 ∧ not (old !s1) ∧ not (old !s2) ∧ not (old !s3) ∧ not (old !s4) (* Source: s0 *)
23    ∧ !x0 ∧ !x1 (* Guard: both buttons pressed *)
24    ∧ not !s0 ∧ not !s1 ∧ not !s2 ∧ !s3 ∧ not !s4 (* Target: s3 *)
25    ∧ !t_s3_s4 = 1 (* Action: t_s3_s4 set to 1 *)
26    (* transitions from state s1 *)
27    ∨ ( not (old !s0) ∧ old !s1 ∧ not (old !s2) ∧ not (old !s3) ∧ not (old !s4) (* Source: s1 *)
28    ∧ not !x0 ∧ not !x1 (* Guard: no button pressed *)
29    ∧ !s0 ∧ not !s1 ∧ not !s2 ∧ not !s3 ∧ not !s4 (* Target: s0 *)
30    ∧ !t_s3_s4 = old !t_s3_s4 (* Action: t_s3_s4 unchanged *)
31    ∨ ( not (old !s0) ∧ old !s1 ∧ not (old !s2) ∧ not (old !s3) ∧ not (old !s4) (* Source: s1 *)
32    ∧ !x0 ∧ not !x1 (* Guard: button x0 pressed but not x1 *)
33    ∧ not !s0 ∧ !s1 ∧ not !s2 ∧ not !s3 ∧ not !s4 (* Target: s1 *)
34    ∧ !t_s3_s4 = old !t_s3_s4 (* Action: t_s3_s4 unchanged *)
35    ∨ ( not (old !s0) ∧ old !s1 ∧ not (old !s2) ∧ not (old !s3) ∧ not (old !s4) (* Source: s1 *)
36    ∧ not !x0 ∧ !x1 (* Guard: button x1 pressed but not x0 *)
37    ∧ not !s0 ∧ not !s1 ∧ !s2 ∧ not !s3 ∧ not !s4 (* Target: s2 *)
38    ∧ !t_s3_s4 = old !t_s3_s4 (* Action: t_s3_s4 unchanged *)
39    ∨ ( not (old !s0) ∧ old !s1 ∧ not (old !s2) ∧ not (old !s3) ∧ not (old !s4) (* Source: s1 *)
40    ∧ !x0 ∧ !x1 (* Guard: both buttons pressed *)
41    ∧ not !s0 ∧ not !s1 ∧ not !s2 ∧ !s3 ∧ not !s4 (* Target: s3 *)
42    ∧ !t_s3_s4 = 1 (* Action: t_s3_s4 set to 1 *)
43  (* transitions from state s2 *)
```

<caption>Figure 12: Abstract function for transitions (part 1).</caption>

Why3 to infer loop invariants. We instruct Why3 not to try to prove that the program terminates with the attribute diverges.

From lines 3 to 13, we assume the initial values of devices, concrete and abstract timers, and states, before execution of the program. All input and output devices are not activated, we give arbitrary values to concrete and abstract timer variables, and we suppose that the variable s0 is true, while other states variables are false, representing the fact that we start execution in initial state S0.

As said previously, we model the cyclic execution of the Ladder program as an infinite while-true loop. We state the state-unicity (exactly one of the states variables is true at a time) as an invariant of this loop (lines 17 to 22). And also declare as invariants the properties on output values for each state (lines 24 to 28).
<figure><img src="image_7.png" /><figcaption>Figure 13: Abstract function for transitions (part 2).</figcaption></figure>

Finally, the body of the loop is composed of calls to functions `input_change` then `transition` to model the possible modifications of input values, and the possible resulting transition to a state of the STD. The rest of the body is the direct translation of the Ladder program of Figure 8.
1 let pgm_2hands_timer [@bddinfer] ()
2 diverges
3 requires { not !x0 }
4 requires { not !x1 }
5 requires { not !y0 }
6 requires { !t0current = 0 }
7 requires { !t0setting = -1 }
8 requires { !t_s3_s4 = 0 }
9 requires { !s0 }
10 requires { not !s1 }
11 requires { not !s2 }
12 requires { not !s3 }
13 requires { not !s4 }
14 =
15 while True
16 do
17 invariant { [@expl:State_unicity]
18     ( !s0 ∧ (not !s1) ∧ (not !s2) ∧ (not !s3) ∧ (not !s4))
19     ∨ ((not !s0) ∧ !s1 ∧ (not !s2) ∧ (not !s3) ∧ (not !s4))
20     ∨ ((not !s0) ∧ (not !s1) ∧ !s2 ∧ (not !s3) ∧ (not !s4))
21     ∨ ((not !s0) ∧ (not !s1) ∧ (not !s2) ∧ !s3 ∧ (not !s4))
22     ∨ ((not !s0) ∧ (not !s1) ∧ (not !s2) ∧ (not !s3) ∧ !s4) }
23 }
24 invariant { [@expl:s0] !s0 → (not !y0) }
25 invariant { [@expl:s1] !s1 → (not !y0) }
26 invariant { [@expl:s2] !s2 → (not !y0) }
27 invariant { [@expl:s3] !s3 → (not !y0) }
28 invariant { [@expl:s4] !s4 → !y0 }
29
30 input_change();
31 transition();
32
33 let common_1 = !x0 && !x1 in
34 timer_coil common_1 t0current t0setting 30;
35 let common_2 = timer contact t0current t0setting in
36 set common_2 y0
37 done

<caption>Figure 14: WhyML code for multiple scans of the 2HANDS_TIMER program.</caption>
# 5 Implementation and Experimental Results

Since the beginning of our work on verification of Ladder programs, our aim is to prototype tools that could be used by regular engineers. For that purpose, we target fully automated proving and feedback of a meaningful error scenario when a violation is detected.

In Section 5.1, we describe the workflow of the implementation of our approach. Then, Section 5.2 presents the results obtained when executing the analysis on our running example, i.e., the implementation of Figure 1. Finally, in Section 5.3, we present the feedback given by our prototype when analyzing a slight modification of the nominal program that makes the verification of conformity to the STD fail.

## 5.1 Overview of the Implementation Approach

Towards our goal of providing a tool that targets regular Ladder engineers, it is important to be able to provide useful information to the user, in case it cannot be proved that a program conforms to an STD specification. In our work on timing-charts verification [5], we were able to provide, to the user, error scenarios that were composed of concrete values for *events* (that correspond to one execution in the WhyML model), and domains of possible values (given by the abstract interpretation engine behind Why3's loop generation) for *states* (that correspond to loops in the WhyML model). For STD verification, the model is composed of a single loop. Domains of possible values won't be sufficient, in that case, for user feedback. Our approach here is to build a complete error scenario using *iterated bounded unfolding* as detailed below.

Our implementation performs the following steps.

1. The tool takes two inputs: an XML representation of the Ladder program and an STD specification, written in the PlantUML language.

2. It translates the Ladder program as a WhyML program, and uses the STD to define the abstract functions *input_change* and *transition* as described in Section 4, to build the full translation as shown in Figure 14.

3. It sends this file to Why3, which generates first a loop invariant, then a set of verification conditions, and send them an SMT solver.

4. If all the verification conditions are proved we conclude that the program is conform to the STD, for any scenario of input changes that is compatible with the STD.

5. Otherwise,

(a) The tool determines which invariant(s) (say which invariants from lines 24-28 of Figure 8) is (are) not proved, and queries the SMT solver for a counterexample to each of the corresponding verification condition(s). Such a counterexample corresponds to a configuration, i.e. a set of values for all the variables involved in the modeling of the Ladder code and the STD, that potentially breaks the invariant after some execution of the loop body. Yet, this is not a *complete* scenario of execution of the system: we aim at getting all the values of the variables at each scan of execution, from the initial configuration up to the error.

(b) In order to build such a complete error, we use a technique of *iterated bounded unfolding* of the loop:

i. We build a new WhyML program, that asserts the same initial values of devices as in Figure 14.
ii. Instead of containing a while-loop, it contains a number *n* of copies of the body of the loop, that correspond to successive scans of the Ladder program. We instrument this WhyML code with additional variables to store the values of the state variables between two scans.

iii. Finally, the end of that WhyML program contains an assertion built as follows: we build a formula $\phi$ as a conjunction of equalities that express that the variables are equal to their values found at step (b) above, and we assert the negation of $\phi$.

iv. If the SMT solver proves that assertion, then it means the error configuration is not reachable within the number *n* of scans chosen at step (ii) above. In that case we retry from step (ii) with a larger value for *n*.

v. Otherwise, when the SMT solver cannot prove the assertion, then we ask again for a counterexample. Such a counterexample contains values for all the additional variables in step (ii), and from them we can finally build a complete error scenario of the Ladder code, from the initial configuration to the invariant violation.
<figure><img src="image_8.png" /><figcaption>Figure 15: Output of the tool on the nominal 2HANDS_TIMER program.</figcaption></figure>

## 5.2 Results on correct code

We apply our approach on the nominal Ladder program described in Figure 1, for which we successfully verify the STD of Figure 2. Figure 15 depicts the result we obtain when running the analysis. We could successfully prove the STD state invariants, thanks to the loop invariant that was inferred by Why3. For information, this invariant is shown in Figure 16. The key point is that the inferred invariant contains the fact that in state $S_3$, the value of the abstract counter $t_s3_s4$ is equal to the value of the concrete counter $t0current$ (see lines 11 and 13).

```
(if !s3 = True then (...) /\ !t_s3_s4 = !t0current)
```

This inferred invariant allows Why3 with solver CVC4 version 1.8 [2] to prove all the VCs, hence formally proving that the Ladder code conforms to the STD. A point to note is the huge improvement in performance of Why3's loop generation engine, since our last experiments concerning timing-charts verification. We can see that on this example, abstract interpretation takes less time than proving, contrary to previously [5].
1 > why3 prove --debug=bddinfer 2hands_timer.mlw
2 Invariant for loop [anonymous_loop_0] is
3 if !s4 = True
4 then !y0 = True /\ !s3 = False /\ !s2 = False /\ !s1 = False /\ !s0 = False
5 /\ (if !x0 = True
6 then if !x1 = True
7 then (1 <= !t0current /\ 29 <= !t_s3_s4) /\ !t0setting = 30
8 else (29 <= !t_s3_s4 /\ !t0setting = 30) /\ !t0current = 0
9 else (29 <= !t_s3_s4 /\ !t0setting = 30) /\ !t0current = 0)
10 else !y0 = False /
11 (if !s3 = True
12 then !s2 = False /\ !s1 = False /\ !s0 = False /\ !x0 = True /\ !x1 = True /
13 ((1 <= !t0current /\ !t0current <= 29) /\ !t0setting = 30) /\ !t_s3_s4 = !t0current
14 else if !s2 = True
15 then !s1 = False /\ !s0 = False /\ !x0 = False /\ !x1 = True /
16 (0 <= !t_s3_s4 /\ !t0setting = 30) /\ !t0current = 0
17 else if !s1 = True
18 then !s0 = False /\ !x0 = True /\ !x1 = False /
19 (0 <= !t_s3_s4 /\ !t0setting = 30) /\ !t0current = 0
20 else !s0 = True /
21 !x0 = False /
22 !x1 = False /
23 ((30 <= !t0setting /\ 0 <= !t_s3_s4) /\ !t0setting <= 1000) /\ !t0current = 0))

<caption>Figure 16: The loop invariant automatically generated by Why3.</caption>
<figure><img src="image_9.png" /><figcaption>Figure 17: Some incorrect variant of Ladder code for 2HANDS_TIMER.</figcaption></figure>

## 5.3 Results on incorrect code

We tested our approach on an incorrect program, a variant of our running example, that does not satisfy the STD specification. This program is depicted in Figure 17. The error consists in the fact that it does not use the right threshold for the timer: 40 instead of 30. When we attempt to prove that this buggy version of the code satisfies the STD specification, we detect a violation for the invariant concerning state $S_4$, and we can exhibit a counterexample i.e. values such that, after the execution of the body of the loop, the variable state s4 is true but the output variable y0 is false. The values of the counterexample are the following:

* $s_3$ is true and other state variables are false;

* both $x_0$ and $x_1$ are true;

* both $t_0current$ and $t_3_s4$ are equal to 29.

Indeed, in that case, after execution of the body of the loop, the value of the abstract timer $t_{s3_s4}$ is equal to 30, so we reach $S_4$ on the side of the STD, while $t_0current$ is also equal to 30, but since the threshold $t_0setting$ is set to 40, $y_0$ is not set to true yet.

As explained in Section 5.1, we now proceed with iterated unbound unfolding. We show in Figure 18 one of the successive WhyML programs that the tool builds: the one in which we unroll the loop twice. Notice the final assertion that expresses that the error configuration is not reachable. In this example, unrolling twice is not sufficient to build an explicit error scenario: the prover is able to prove that the assertion holds. The process must be iterated until reaching 29 unrolls, with which the tool is finally able to build a fully explicit error scenario from the initial configuration. The (smallest) error scenario found consists in $X_0$ and $X_1$ being activated from the beginning, 30 consecutive scans (we reach $S_3$ at the first execution, stay in $S_3$ for 28 scans, and in last scan, we reach $S_4$ but $Y_0$ is not activated).

In practice, the tool finally exports this error scenario as an HTML page allowing to navigate in the error scenario, with the different scans represented as the values of inputs and internal memory before execution and the (possibly implicit) transition taken in the STD, during execution. We show in Figure 19 and Figure 20 the first and last pictures that correspond to the first and last scans of the error scenario. As you can see, the tool explicits all input, output and local memory device values, for each scan, and shows which state and transition are active at that time. We believe that all this information provides a useful feedback to the programmer to easily and rapidly understand where the error comes from.
1 let pgm_2hands_timer_error_40_unroll_2 ()
2 requires { not !x0 }
3 requires { not !x1 }
4 requires { not !y0 }
5 requires { !t0current = 0 }
6 requires { !t0setting = -1 }
7 requires { !t_s3_s4 = 0 }
8 requires { !s0 }
9 requires { not !s1 }
10 requires { not !s2 }
11 requires { not !s3 }
12 requires { not !s4 }
13 =
14 (* Scan 1 *)
15 input_change();
16 (* keep track of inputs values *)
17 scan1_x0 := !x0; scan1_x1 := !x1;
18 transition();
19 (* keep track of states values *)
20 scan1_s0 := !s0; scan1_s1 := !s1; scan1_s2 := !s2; scan1_s3 := !s3; scan1_s4 := !s4;
21 (* program body *)
22 let common_1 = !x0 && !x1 in
23 timer_coil common_3 t0current t0setting 40;
24 let common_2 = timer contact t0current t0setting in
25 set common_4 y0;
26
27 (* Scan 2 *)
28 input_change();
29 (* keep track of inputs values *)
30 scan2_x0 := !x0; scan2_x1 := !x1;
31 transition();
32 (* keep track of states values *)
33 scan2_s0 := !s0; scan2_s1 := !s1; scan2_s2 := !s2; scan2_s3 := !s3; scan2_s4 := !s4;
34 (* program body *)
35 let common_1 = !x0 && !x1 in
36 timer_coil common_3 t0current t0setting 40;
37 let common_2 = timer contact t0current t0setting in
38 set common_2 y0;
39
40 (* Try to reach the potential counterexample values *)
41 assert { not ( (not !s0 ^ not !s1 ^ not !s2 ^ !s3 ^ not !s4)
42     ^ (!x0 ^ !x1)
43     ^ (!t0current = 29)
44     ^ (!ts3_s4 = 29)) }

<caption>Figure 18: WhyML program modeling two unrolling of execution of the original program loop.</caption>
<figure><img src="image_10.png" /><figcaption>Figure 19: First step of execution of the error scenario.</figcaption></figure>

<figure><img src="image_11.png" /><figcaption>Figure 20: Last step of execution of the error scenario.</figcaption></figure>
# 6 Discussions, Related Work and Future Work

We presented an original methodology for formally verifying that a given Ladder code conforms to an expected behavior expressed by a state transition diagram. By translating both the Ladder code and the diagram into a WhyML program, and making use of the loop invariant generation capability of Why3, we are able to provide a fully automatic process to proceed with such a verification, with a high level of confidence. Moreover, when this proof-based process fails at some point, we have a way to propose an explicit scenario of execution which exposes why the Ladder code is not conforming to the STD. Our methodology is implemented in a prototype which we experimented on a case study, demonstrating the effectiveness of our approach, both for formally proving the correct version and for providing a counterexample scenario on a wrong mutant.

The level of confidence of our approach must be understood in terms of the trusted code base of the whole process. It first relies on the soundness of the translation from Ladder code and the STD, which is described in Section 4. It also relies on the soundness of the VC generation process of Why3, which is not formally proven correct but validated on numerous applications [8]. Regarding trust in Why3, it is important to notice that the loop invariant generation feature is *not* part of the trusted code base, because the loop invariants generated are later on checked for validity by the VC generation process. The last part of the tool chain that must be trusted is the back-end SMT solver.

Regarding the scenarios generated, one weakness of our former approach [5] is that, due to the inherent incompleteness of counter-model generation of SMT solvers, it cannot guarantee that the generated scenarios are always valid. With our new approach, the construction of the error scenario is explicit and detailed down to each scan, hence we can be sure it is a valid error scenario.

**Related work.** PLC software verification is a vast domain and numerous works have been published on that subject. The majority of them use model-checking to verify functional and temporal properties. A summary of those techniques is given by Ovatman et al. [25]. The drawback of model-checking is that the verification it provides cannot be exhaustive, it cannot model any possible number of executions of the STD, contrary to deductive verification. On the other hand, abstract interpretation has also been used for a long time for verifying software, in particular micro-controller software [15, 24] and PLC software [6] (in combination with model-checking). Contrary to model-checking, abstract interpretation gives a full guarantee when it detects no error in a program, but it is dedicated to compute the possible values of variables during the execution of a program, and is not suited for verifying temporal specifications. Finally, in a former work, some of us [11] used the Why3 deductive verification platform for detecting runtime errors of Ladder programs. This work only considered one single execution of Ladder programs and was therefore also not suited for verifying temporal specifications.

**Future work.** In the future, we plan to experiment our method on examples of Ladder programs that require WhyML translations involving arrays, and we have to ensure that the loop invariant generation could succeed when we are mixing all involving data-types: integers, Boolean, arrays, and also bounded integers in the future.

A more long-term goal is to augment the trust in the translation from Ladder to WhyML. We are currently designing [10] a systematic and automatic validation process to confront our translation against existing test suites for Ladder programs.

Immediate future work will consist in making our prototype tool more robust and experiment it on real-world use cases of larger size, in particular STDs that come from Mitsubishi Electric's manual on Safety Function Blocks [22].

**Acknowledgments.** The authors thank François Cellier for his help on the design and implementation of the formalization of State Transitions Diagrams in Why3.
References

[1] Haniel Barbosa, Clark W. Barrett, Martin Brain, Gereon Kremer, Hanna Lachnitt, Makai Mann, Abdalrhman Mohamed, Mudathir Mohamed, Aina Niemetz, Andres Nötzli, Alex Ozdemir, Mathias Preiner, Andrew Reynolds, Ying Sheng, Cesare Tinelli, and Yoni Zohar. cvc5: A versatile and industrial-strength SMT solver. In Dana Fisman and Grigore Rosu, editors, *Tools and Algorithms for the Construction and Analysis of Systems*, volume 13243 of *Lecture Notes in Computer Science*, pages 415–442. Springer, 2022. doi:10.1007/978-3-030-99524-9_24.

[2] Clark Barrett, Christopher L. Conway, Morgan Deters, Liana Hadarean, Dejan Jovanović, Tim King, Andrew Reynolds, and Cesare Tinelli. CVC4. In *Computer Aided Verification*, volume 6806 of *Lecture Notes in Computer Science*, pages 171–177. Springer, 2011. doi:10.1007/978-3-642-22110-1_14.

[3] Benedikt Becker, Cláudio Belo Lourenço, and Claude Marché. Explaining counterexamples with giant-step assertion checking. In José Creissac Campos and Andrei Paskevich, editors, *6th Workshop on Formal Integrated Development Environments (F-IDE 2021)*, Electronic Proceedings in Theoretical Computer Science, May 2021. URL: https://hal.inria.fr/hal-03217393, doi:10.4204/EPTCS.338.10.

[4] Cláudio Belo Lourenço, Denis Cousineau, Florian Faissole, Claude Marché, David Mentré, and Hiroaki Inoue. Formal analysis of Ladder programs using deductive verification. Research Report RR-9402, Inria, April 2021. URL: https://hal.inria.fr/hal-03199464.

[5] Cláudio Belo Lourenço, Denis Cousineau, Florian Faissole, Claude Marché, David Mentré, and Hiroaki Inoue. Automated formal analysis of temporal properties of Ladder programs. *International Journal on Software Tools for Technology Transfer*, 24(6):977–997, 2022. URL: https://hal.inria.fr/hal-03737869, doi:10.1007/s10009-022-00680-0.

[6] Sebastian Biallas, Stefan Kowalewski, Stefan Stattelmann, and Bastian Schlich. Efficient handling of states in abstract interpretation of industrial programmable logic controller code. In *12th International Workshop on Discrete Event Systems*, pages 400–405. IFAC, 2014.

[7] François Bobot, Jean-Christophe Filliâtre, Claude Marché, and Andrei Paskevich. Why3: Shepherd your herd of provers. In *Boogie 2011: First International Workshop on Intermediate Verification Languages*, pages 53–64, Wrocław, Poland, August 2011. URL: http://hal.inria.fr/hal-00790310.

[8] François Bobot, Jean-Christophe Filliâtre, Claude Marché, and Andrei Paskevich. Let's verify this with Why3. *International Journal on Software Tools for Technology Transfer (STTT)*, 17(6):709–727, 2015. See also http://toccata.gitlabpages.inria.fr/toccata/gallery/fm2012comp.en.html. URL: http://hal.inria.fr/hal-00967132/en, doi:10.1007/s10009-014-0314-5.

[9] Sylvain Conchon, Albin Coquereau, Mohamed Iguernlala, and Alain Mebsout. Alt-Ergo 2.2. In *SMT Workshop: International Workshop on Satisfiability Modulo Theories*, Oxford, United Kingdom, July 2018. URL: https://hal.inria.fr/hal-01960203.

[10] Denis Cousineau, Hiroaki Inoue, Claude Marché, and David Mentré. A methodological guide for the validation of logic modelling of Ladder instructions. Technical Report 0522, Inria, 2024. URL: https://inria.hal.science/hal-04487766.

[11] Denis Cousineau, David Mentré, and Hiroaki Inoue. Automated deductive verification for ladder programming. In *F-IDE – Fifth Workshop on Formal Integrated Development Environments*, volume
310 of *Electronic Proceedings in Theoretical Computer Science*, pages 7–12, 2019. doi:10.4204/EPTCS.310.2.

[12] Sylvain Dailler, David Hauzar, Claude Marché, and Yannick Moy. Instrumenting a weakest pre-condition calculus for counterexample generation. *Journal of Logical and Algebraic Methods in Programming*, 99:97–113, 2018. URL: https://hal.inria.fr/hal-01802488, doi:10.1016/j.jlamp.2018.05.003.

[13] Leonardo de Moura and Nikolaj Bjørner. Z3, an efficient SMT solver. In *TACAS*, volume 4963 of *Lecture Notes in Computer Science*, pages 337–340. Springer, 2008. doi:10.1007/978-3-540-78800-3_24.

[14] Xavier Denis, Jacques-Henri Jourdan, and Claude Marché. Creusot: a foundry for the deductive verification of Rust programs. In *International Conference on Formal Engineering Methods - ICFEM*, Lecture Notes in Computer Science, Madrid, Spain, 2022. Springer. URL: https://hal.inria.fr/hal-03737878.

[15] Ansgar Fehnker, Ralf Huuck, Bastian Schlich, and Michael Tapp. Automatic bug detection in microcontroller software by static program analysis. In *SOFSEM – Theory and Practice of Computer Science*, volume 5404 of *Lecture Notes in Computer Science*, pages 267–278. Springer, 2009. doi:10.1007/978-3-540-95891-8_26.

[16] Jean-Christophe Filliâtre and Claude Marché. The Why/Krakatoa/Caduceus platform for deductive program verification. In Werner Damm and Holger Hermanns, editors, *19th International Conference on Computer Aided Verification*, volume 4590 of *Lecture Notes in Computer Science*, pages 173–177, Berlin, Germany, July 2007. Springer. URL: https://hal.inria.fr/inria-00270820v1, doi:10.1007/978-3-540-73368-3_21.

[17] Jean-Christophe Filliâtre and Andrei Paskevich. Why3 — where programs meet provers. In Matthias Felleisen and Philippa Gardner, editors, *Proceedings of the 22nd European Symposium on Programming*, volume 7792 of *Lecture Notes in Computer Science*, pages 125–128. Springer, March 2013. URL: http://hal.inria.fr/hal-00789533.

[18] Jean-Christophe Filliâtre and Andrei Paskevich. Abstraction and genericity in Why3. In Tiziana Margaria and Bernhard Steffen, editors, *9th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation (ISoLA)*, volume 12476 of *Lecture Notes in Computer Science*, pages 122–142, Rhodes, Greece, October 2020. Springer. See also https://usr.lmf.cnrs.fr/~jcf/isola-2020/. URL: https://hal.inria.fr/hal-02696246.

[19] Bertrand Jeannet and Antoine Miné. Apron: A library of numerical abstract domains for static analysis. In Ahmed Bouajjani and Oded Maler, editors, *Computer Aided Verification*, pages 661–667. Springer, 2009.

[20] Nikolai Kosmatov, Claude Marché, Yannick Moy, and Julien Signoles. Static versus dynamic verification in Why3, Frama-C and SPARK 2014. In Tiziana Margaria and Bernhard Steffen, editors, *7th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA)*, volume 9952 of *Lecture Notes in Computer Science*, pages 461–478, Corfu, Greece, October 2016. Springer. URL: https://hal.inria.fr/hal-01344110, doi: 10.1007/978-3-319-47166-2_32.

[21] Claude Marché and Denis Cousineau. De l'avantage de nuancer les décisions binaires. In *35es Journées Francophones des Langages Applicatifs*, 2024. URL: https://inria.hal.science/hal-04342273.
[22] Mitsubishi Electric Corporation. MELSEC iQ-R Safety Function Block Reference (for GX Works3). https://dl.mitsubishielectric.com/dl/fa/document/manual/plc/bcn-p5999-0815/bcnp59990815c.pdf, 2016. [Online; accessed 14-June-2022].

[23] Mitsubishi Electric Corporation. MELSEC iQ-R Safety Function Block Reference, 2018. BCN-P5999-0814-C, [Online; accessed 11-May-2025]https://www.mitsubishielectric.com/dl/fa/document/manual/plc/bcn-p5999-0815/bcnp59990815c.pdf.

[24] T. Nguyen, T. Aoki, T. Tomita, and J. Endo. Integrating static program analysis tools for verifying cautions of microcontroller. In *APSEC – Asia-Pacific Software Engineering Conference*, pages 86–93, 2019. doi:10.1109/APSEC48747.2019.00021.

[25] Tolga Ovatman, Atakan Aral, Davut Polat, and Ali Ünver. An overview of model checking practices on verification of PLC software. *Software & Systems Modeling*, 15:1–24, 2014. doi:10.1007/s10270-014-0448-7.

[26] R. Ramanathan. The IEC 61131-3 programming languages features for industrial control systems. In *WAC – World Automation Congress*, pages 598–603, 2014. doi:10.1109/WAC.2014.6936062.
<figure><img src="image_12.png" /></figure>

RÉPUBLIQUE
FRANÇAISE

Liberté
Égalité
Fraternité

Inria

RESEARCH CENTRE
SACLAY - ÎLE-DE-FRANCE

1 rue Honoré d'Estienne d'Orves
Bâtiment Alan Turing
Campus de l'École Polytechnique
91120 Palaiseau

Publisher
Inria
Domaine de Voluceau - Rocquencourt
BP 105 - 78153 Le Chesnay Cedex
inria.fr

ISSN 0249-6399