Wen Tang
email: wtang6@ncsu.edu

Emilie Chouzenoux
email: emilie.chouzenoux@centralesupelec.fr

Jean-Christophe Pesquet
email: jean-christophe.pesquet@centralesupelec.fr

Hamid Krim

DEEP TRANSFORM AND METRIC LEARNING NETWORKS

Keywords: Deep Dictionary Learning, Deep Neural Network, Metric Learning, Transform Learning, Proximal Operator, Differentiable Programming

Based on its great successes in inference and denosing tasks, Dictionary Learning (DL) and its related sparse optimization formulations have garnered a lot of research interest. While most solutions have focused on single layer dictionaries, the recently improved Deep DL methods have also fallen short on a number of issues. We hence propose a novel Deep DL approach where each DL layer can be formulated and solved as a combination of one linear layer and a Recurrent Neural Network, where the RNN is flexibly regraded as a layer-associated learned metric. Our proposed work unveils new insights between the Neural Networks and Deep DL, and provides a novel, efficient and competitive approach to jointly learn the deep transforms and metrics. Extensive experiments are carried out to demonstrate that the proposed method can not only outperform existing Deep DL, but also state-of-the-art generic Convolutional Neural Networks.

INTRODUCTION

Dictionary Learning/Sparse Coding has been successfully applied for solving various inference tasks, such as image denoising [START_REF] Elad | Image denoising via sparse and redundant representations over learned dictionaries[END_REF], image restoration [START_REF] Xu | Cloud removal based on sparse representation via multitemporal dictionary learning[END_REF], image super-resolution [START_REF] Zhong | Robust object tracking via sparsity-based collaborative model[END_REF], audio processing [START_REF] Grosse | Shift-invariant sparse coding for audio classification[END_REF], and image classification [START_REF] Zhang | Class relatedness orienteddiscriminative dictionary learning for multiclass image classification[END_REF].

Synthesis Dictionary Learning (SDL) is the early primary approach in this area. Then, Analysis Dictionary Learning (ADL)/Transform Learning, the dual problem of SDL, received more attention. DL based methods [START_REF] Aharon | K-svd: An algorithm for designing overcomplete dictionaries for sparse representation[END_REF][START_REF] Wang | Synthesis k-svd based analysis dictionary learning for classification[END_REF][START_REF] Tang | Structured analysis dictionary learning for image classification[END_REF][START_REF] Tang | Analysis dictionary learning: an efficient and discriminative solution[END_REF][START_REF] Tang | Analysis dictionary learning based classification: Structure for robustness[END_REF] for image classification usually focus on learning one-layer dictionary and its associated sparse representation. Since DL methods need to simultaneously learn the dictionary and its associated representation, thanks to a sparsity promoting regularization, they raise challenging numerical issues. To address such challenges, a number of dictionary learning solvers have been developed, including K-SVD [START_REF] Aharon | K-svd: An algorithm for designing overcomplete dictionaries for sparse representation[END_REF] and Fast Iterative Shrinkage-thresholding Algorithm (FISTA) [START_REF] Beck | A fast iterative shrinkagethresholding algorithm for linear inverse problems[END_REF] schemes, for instance. Although such alternating minimization methods provide practical solutions for DL, they remain prone to limitations and have a relatively high computational cost. To overcome such computational difficulties, differentiable programming has also been developed, to take advantage of the efficiency of neural networks, such as LISTA [START_REF] Gregor | Learning fast approximations of sparse coding[END_REF] and Sparse LSTM [START_REF] Zhou | Sc2net: Sparse lstms for sparse coding[END_REF].

Although the aforementioned differentiable programming methods are efficient at solving a single-layer DL problem, the latter formulation still does not lead to the best performance in image classification tasks. With the fast development of deep learning, Deep Dictionary Learning (DDL) methods [START_REF] Tariyal | Deep dictionary learning[END_REF][START_REF] Mahdizadehaghdam | Image classification: A hierarchical dictionary learning approach[END_REF] have thus come into play. [START_REF] Mahdizadehaghdam | Deep dictionary learning: A parametric network approach[END_REF] deeply stacks SDLs to classify images and achieves promising performance. Also, a deep model for ADL followed by a SDL is developed for image super-resolution in [START_REF] Huang | A deep dictionary model for image super-resolution[END_REF]. Unsupervised DDL approaches have also been proposed, with interesting results [START_REF] Gupta | Deconfuse: a deep convolutional transform-based unsupervised fusion framework[END_REF][START_REF] Maggu | Unsupervised deep transform learning[END_REF].

However, to the best of our knowledge, there is no method for training such kind of end-to-end deep dictionary models in a both fast and reliable manner. This work aims at ensuring the discriminative ability of single-layer DL while benefiting from the efficiency of end-to-end models. To this end, we propose a novel differentiable programming method, namely, Deep Transform and Metric Learning. To further benefit from the efficiency of DDL models, the resulting structures are stacked into a deep network, leading to a so-called DeTraMe Network (DeTraMe-Net). Our new approach not only increases the discrimination capabilities of DL, but also brings the flexibility to construct different DDL or Deep Neural Network (DNN) architectures. It also allows to overcome the roadblocks raised by initialization and gradient propagation issues arising in standard DDL methods. Although the authors of [START_REF] Wang | Deep networks for image super-resolution with sparse prior[END_REF] and [START_REF] Liu | Dictionary learning inspired deep network for scene recognition[END_REF] also used a CNN followed by an RNN for respectively solving super-resolution and sense recognition tasks, they directly used LISTA in their model. In turn, our method actually solves the same problem as LISTA.

Our main contributions are summarized below: 1) We theoretically transform one-layer dictionary learning into a transform learning and Q-Metric learning, and derive the conversion of DDL into DeTraMe-Net. 2) Such joint transform learning and Q-Metric learning are easily implemented into a combined linear layer and a RNN. A convolutional layer can be chosen for the linear part, and the RNN can also be simplified into a Convolutional-RNN. To the best of our knowledge, this is the first work which establishes an insightful bridge between DDL methods and the combination of Forward Neural Networks (FNNs) and RNNs. 3) The transform and Q-Metric learning use two independent variables, one for the metric and the other for the pseudo-inverse of the dictionary. This allows us to make a link with conventional SDL while introducing more discriminative power and allowing faster learning procedures than the original DL. 4) Q-Metric can also be viewed as a parametric non-separable nonlinear activation function, while in current neural network architectures, very few nonseparable nonlinear operators are used. As a module in a neural network, it can be flexibly inserted into any network architectures to easily construct DL layer. 5) The proposed DeTraMe-Net is demonstrated not only to improve the discrimination power of DDL, but also to achieve a better performance than the state-of-the-art CNNs.

The paper is organized as follows: In Section 2, we introduce the required background material. We derive the theoretical basis for our novel approach and its algorithmic solution in Section 3. Substantiating experimental results and evaluations are presented in Section 4. Finally, we provide some concluding remarks in Section 5.

PRELIMINARIES

Notation

Uppercase and lowercase bold letters respectively denote matrices and vectors throughout the paper. The transpose and inverse of matrices are respectively represented by the superscripts and -1 . The identity matrix is denoted by I. The lowercase a i,j represents the element in the i th row and j th column of matrix A, and a i represents the i th component of vector a.

Deep Dictionary Learning

An efficient DDL approach [START_REF] Mahdizadehaghdam | Deep dictionary learning: A parametric network approach[END_REF] consists of computing ŷ = ϕ(Cx (s) ) where

x (s) = P (s) • M D (s) • • • • • P (1) • M D (1) (x (0) ), (1)
and ŷ denotes the estimated label, C is the classifier matrix, ϕ is a nonlinear function, and • denotes the composition of operators. For every layer r ∈ {1, . . . , s}, P (r) is a reshaping operator, which is a tall matrix. Moreover, M D (r) is a nonlinear operator computing a sparse representation within a synthesis dictionary matrix D (r) . More precisely, for a given matrix

D (r) ∈ R mr×kr , M D (r) : R mr → R kr , x → argmin a∈R kr L R (D (r) , a, x), L R (D (r) , a, x) = 1 2 x -D (r) a 2 F + λψ r (a) + α 2 a 2 2 + (d (r) ) a, (2)
where (λ, α) ∈ (0, +∞) 2 , d (r) ∈ R kr , and ψ r is a function in Γ 0 (R kr ), the class of proper lower semicontinuous convex functions from R kr to (-∞, +∞]. A simple choice consists in setting d (r) to zero, while adopting the following specific form for ψ r :

ψ r = • 1 + ι [0,+∞) kr
, where ι S denotes the indicator function of a set S (equal to zero in S and +∞ otherwise). Note that Eq. ( 2) corresponds to the minimization of a strongly convex function (w.r.t. a), which thus admits a unique minimizer, so making the operator M D (r) properly defined.

DEEP TRANSFORM AND METRIC LEARNING

Proximal interpretation

In the following, the superscript denoting the layer r has been omitted for simplicity. We have then the following result [START_REF] Tang | Deep transform and metric learning network: Wedding deep dictionary learning and neural networks[END_REF]: Theorem 3.1 Let L R be the function defined by eq. ( 2). For every

D ∈ R m×k , let Q = D D + αI, let F = Q -1 D , and let c = Q -1 d. Then, for every x ∈ R m , M D (x) = argmin a∈R k L R (D, a, x) = prox Q λψ (Fx -c), (3)
where prox Q λψ denotes the proximity operator of function λψ in the metric

• Q = (•) Q(•) induced by Q [23, 24].
Therefore determining the optimal sparse representation a of x ∈ R m is equivalent to computing a proximity operator. Furthermore, this result shows that the SDL can be equivalently viewed as an ADL formulation involving the dictionary matrix F, provided that a proper metric is chosen.

Multilayer representation

Consequently, by substituting eq. (3) in eq. ( 1), the DDL model can be re-expressed in a more concise and comprehensive form as

ŷ =ϕ • A (s+1) • prox Q (s) λψs •A (s) • • • • • prox Q (1) λψ1 •A (1) (x (0) ), (4)
where the affine operators A (r) 1≤r≤s are defined as

A (r) : R kr-1 → R kr : z (r-1) → W (r) z (r) -c (r) , (5)
with k 0 = m 1 , W (1) = F (1) , and ∀r ∈ {2, . . . , s}, W (r) = F (r) P (r-1) , W (s+1) = CP (s) ∀r ∈ {1, . . . , s}, Q (r) = (D (r) ) D (r) + αI,

F (r) = (Q (r) ) -1 (D (r) ) , c (r) = (Q (r) ) -1 d (r) . (6)
Eq. ( 5) shows that we obtain a structure similar to an FNN using weight operators W (r) 1≤r≤s and bias parameters (c (r) ) 1≤r≤s , which is referred to as the transform learning part in our DeTraMe-Net method. In standard FNNs, the activation functions can be interpreted as proximity operators of convex functions [START_REF] Patrick | Deep neural network structures solving variational inequalities[END_REF]. Eq. ( 4) evidences that our model is actually more general in the sense that different metrics are introduced for these operators.

Prox computation

Reformulation (4) has the great advantage of exploiting algorithmic frameworks developed for FNNs provided that we are able to compute efficiently

prox Q λψ (Z) = argmin U∈R k×N 1 2 U -Z 2 F,Q + λψ(U), (7)
where

• F,Q = tr((•)Q(•) ) is the Q-weighted Frobenius norm.
Hereabove, Z is a matrix where the N samples associated with the training set have been stacked columnwise. A convention is used to construct X and Y from (x j ) 1≤j≤N and (y j ) 1≤j≤N . Various iterative splitting methods could be used to find the unique solution to the above convex optimization problem [START_REF] Patrick | Proximal splitting methods in signal processing[END_REF][START_REF] Komodakis | Playing with duality: An overview of recent primal-dual approaches for solving large-scale optimization problems[END_REF]. Our purpose is to develop an algorithmic solution for which classical NN learning techniques can be applied in a fast and systematic manner. Our approach will be grounded in the following result.

Theorem 3.2 [START_REF] Tang | Deep transform and metric learning network: Wedding deep dictionary learning and neural networks[END_REF] Assume that an elastic-net like regularization is adopted by setting

ψ = • 1 + ι [0,+∞) k×N + β 2λ • 2 F
with β ∈ (0, +∞). For every Z ∈ R k×N , the elements of prox Q λψ (Z) in eq. ( 7) satisfy for every i ∈ {1, . . . , k}, and j ∈ {1, . . . , N },

u i,j = qi,i qi,i+β z i,j -v i,j if q i,i z i,j > (q i,i + β)v i,j 0 otherwise, (8)
where v i,j = λ+ k =1, =i q i, (u ,j -z ,j ) qi,i+β .

We have observed that the choice of an elastic elasticnet like regularization has a positive influence in increasing stability and avoiding overfitting. Since Theorem 3.2 does not provide an explicit expression of prox Q λψ (Z), we compute it by adopting a block-coordinate approach and update the i-th row of U by fixing all the other ones. As Q is a positive definite matrix, q i,i > 0. Let

W = - q i, qi,i+β δ i- 1≤i, ≤k , h = qi,i qi,i+β 1≤i≤k ∈ [0, 1] k , b = λ q i,i +β 1≤i≤k ∈ [0, +∞) k , 1 = [1, . . . , 1] ∈ R N ,
where (δ ) ∈Z is the Kronecker sequence (equal to 1 when = 0 and 0 otherwise). Then, [START_REF] Tang | Structured analysis dictionary learning for image classification[END_REF] suggests that the elements of U can be globally updated, at iteration t, as follows

U t+1 = ReLU (h1 ) Z + W(U t -Z) -b1 , (9)
where denotes the Hadamard (element-wise) product. Note that a similar expression can be derived by applying a preconditioned forward-backward algorithm [START_REF] Chouzenoux | Variable metric forward-backward algorithm for minimizing the sum of a differentiable function and a convex function[END_REF] to Problem [START_REF] Wang | Synthesis k-svd based analysis dictionary learning for classification[END_REF], where the preconditioning matrix is Diag(q 1,1 , . . . , q k,k ). Given W, h, and b, this updating rule ( 9) can be viewed as an RNN structure for which U t is the hidden variable and Z is a constant input over time.

Algorithm 1 Deep Metric and Transform Learning

Initialization: Set t = 0.

1: while not converged and t < t max do 2:

Forward pass: U

for r = 1, . . . , s +

if r ≤ s then while not converged and tt < tt max do 8:

Update U tt+1 according to eq. ( 9); tt ← tt + 1

Ŷt = ϕ(Z (s+1) t ) 13:
Loss: L (θ t ) = L(Y, Ŷt ), θ t : vector of all parameters 14:

Backward pass:

15:

for r = 1, . . . , s + 1 do 16:

W (r) t+1 = W (r) t -ρ t ∂L ∂W (r) (θ t ) 17: c (r) t+1 = c (r) t -ρ t ∂L ∂c (r) (θ t ) 18:
end for 19:

for r = 1, . . . , s do 20:

W (r) t+1 = P D0 W (r) t -ρ t ∂L ∂ W (r) (θ t ) 21: h (r) t+1 = P [0,1] k h (r) t -ρ t ∂L ∂h (r) (θ t ) 22: b (r) t+1 = P [0,+∞) k b (r) t -ρ t ∂L ∂b (r) (θ t ) 23:
end for 24:

t ← t + 1 25: end while

Training procedure

We have finally transformed our DDL approach in an alternation of linear layers and specific RNNs. Let ρ t > 0 be the Table 1. CIFAR10 and CIFAR100 with + is trained with simple translation and flipping data augmentation. All the presented results are re-implemented over 5 runs by using the same settings, and are calculated by their means and standard deviations. learning rate at iteration t, the simplified form of a training method for DeTraMe-Net is provided in Alg. 1. The constraints on the parameters of the RNNs have been imposed by projections. In Alg. 1, P S denotes the projection onto a nonempty closed convex set S and D 0 is the vector space of k × k matrices with diagonal terms equal to 0.

EXPERIMENTS AND RESULTS

In this section, our DeTraMe-Net method is evaluated on two popular datasets, namely CIFAR10 [START_REF] Krizhevsky | Learning multiple layers of features from tiny images[END_REF] and CIFAR100 [START_REF] Krizhevsky | Learning multiple layers of features from tiny images[END_REF]. Since the common NN architectures are plain networks such as ALL-CNN [START_REF] Tobias Springenberg | Striving for simplicity: The all convolutional net[END_REF] and residual ones, such as ResNet [START_REF] He | Deep residual learning for image recognition[END_REF] , we compare DeTraMe-Net with these two respective state-of-theart architectures. We replace all the ReLU activation layers in PlainNet with Q-Metric ReLU, leading to DeTraMe-PlainNet, and replace the ReLU layer inside the block in ResNet by Q-Metric ReLU, giving rise to DeTraMe-ResNet. More detailed information can be found in [START_REF] Tang | Deep transform and metric learning network: Wedding deep dictionary learning and neural networks[END_REF]. First we compare our DeTraMe-Net with DDL [START_REF] Mahdizadehaghdam | Deep dictionary learning: A parametric network approach[END_REF]. Although DeTraMe-Net needs more parameters, DeTraMe-Net presents two main advantages: (1) A better ability to discriminate: in comparison to DDL in the top table of Table 2, in terms of averaged performance, 0.01% and 0.92% accuracy improvements are respectively obtained on these two datasets.

(2) DeTraMe-Net is implemented in a network framework, with no need for extra functions to compute gradients at each layer, which greatly reduces the time costs. The bottom part of Table 2 shows that our method with 6 times more parameters than DDL only requires half training time and a faster testing time by a factor 100. Moreover, by taking advantage of the developed implementation frameworks for neural networks, DeTraMe-Net can use up to 110 layers, while the maximum number of layers in [START_REF] Mahdizadehaghdam | Deep dictionary learning: A parametric network approach[END_REF] is 23.

DeTraMe-Net vs. Generic CNNs

We next compare DeTraMe-Net with generic CNNs with respect to two different aspects: Accuracy and Capacity.

Accuracy. As shown in Table 1, with the same architecture, using DeTraMe-Net structures achieves an overall better performance than all various generic CNN models do. For PlainNet architecture, DeTraMe-Net increases the accuracy with a median of 3.99% on CIFAR10, 5.11% on CIFAR100 and 0.45% on SVHN. For ResNet architecture, DeTraMe-Net also consistently increases the accuracy with a median of 0.05% on CIFAR10, 0.13% on CIFAR100.

Capacity. In terms of depth, comparing improvements with PlainNet and ResNet, shows that the shallower the network, the more accurate. It is remarkable that DeTraMe-Net leads to more than 42% accuracy increase for PlainNet 3-layers on CIFAR10 and CIFAR100. When the networks become deeper, they better capture discriminative features of the classes, and albeit with smaller gains, DeTraMe-Net still achieves a better accuracy than a generic deep CNN, e.g. around 0.11% and 0.05% higher than ResNet 110 on CIFAR10 and CIFAR100.

CONCLUSION

Starting from a DDL formulation, we have shown that the introduction of metrics within standard activation operators, gives rise to a novel Joint Deep and Transform Learning problem. This has allowed us to show that the original DDL can be performed thanks to a network mixing FNN and RNN parts, so leading to a fast and flexible network framework for building efficient DDL-based classifiers. Our experiments illustrate that the resulting DeTraMe-Net performs better than the original DDL approach and state-of-the-art generic CNNs.

0

  as the null matrix and set tt = 0 7:

Table 2 .

 2 The results with * are reported in the original paper. The top table provides the accuracy of DeTraMe-Net vs. DDL, where DeTraMe-Net 9 and DDL 9 follow the same ALL-CNN[START_REF] Tobias Springenberg | Striving for simplicity: The all convolutional net[END_REF] architecture. The bottom one is the efficiency comparison, where the architectures are different from the top ones

* This research work was generously supported in part by the U.S. Army Research Office under agreement W911NF1910202.


Cláudio Belo Lourenço

Denis Cousineau

Florian Faissole

Claude Marché

David Mentré

Hiroaki Inoue

Automated Verification of Temporal Properties of Ladder Programs

Keywords: Ladder language for programming PLCs, Timing charts, Formal specification, Deductive verification, Why3 environment

Programmable Logic Controllers (PLCs) are industrial digital computers used as automation controllers in manufacturing processes. The Ladder language is a programming language used to develop PLC software. Our aim is to prove that a given Ladder program conforms to an expected temporal behaviour given as a timing chart, describing scenarios of execution. We translate the Ladder code and the timing chart into a program for the Why3 environment, within which the verification proceeds by generating verification conditions, to be checked valid using automated theorem provers. The ultimate goal is two-fold: first, by obtaining a complete proof, we can verify the conformance of the Ladder code with respect to the timing chart with a high degree of confidence. Second, when the proof is not fully completed, we obtain a counterexample, illustrating a possible execution scenario of the Ladder code which does not conform to the timing chart.

Introduction

Programmable Logic Controllers (PLCs) are industrial digital computers used as automation controllers in 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 one of the first available for programming PLCs, and is now standardised in the IEC 61131-3 standard [START_REF] Ramanathan | The IEC 61131-3 programming languages features for industrial control systems[END_REF]. It is one language among other languages for programming PLCs, and is still 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 conforms to its expected behaviour is of critical importance. In this work, we consider the description of the expected temporal behaviour under the form of a timing chart, describing scenarios of execution. Our approach consists in automatically translating the Ladder code and the timing chart into a program written in the WhyML language, which is the input language of the generic Why3 environment for deductive program verification [START_REF] Bobot | Let's verify this with Why3[END_REF]. In WhyML, expected behaviours 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 conformance of the Ladder code with respect to the timing chart 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 succeed, our long-term goal being to build a tool that would be useful to regular Ladder programmers. More precisely, in such a case of proof failure, we aim at obtaining a counterexample which must illustrate a possible execution scenario of the Ladder code which does not conform to the timing chart.

This paper is organised as follows. We start in Section 2 by introducing the basics of Ladder programming, and the way their expected temporal behaviours are expressed using timing charts. The translation of Ladder code and timing charts into WhyML programs is described in Section 3. Section 4 presents our experiments and their results, both in the case of a complete proof success and in the case of a proof failure, where a counterexample is generated. We discuss related work and future work in Section 5. For sake of concision some technical details are omitted, such details are available in an extended research report [START_REF] Belo Lourenço | Formal analysis of Ladder programs using deductive verification[END_REF].

Introduction to Ladder Programming

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 values, 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 (Boolean conjunction) or in a parallel way (disjunction). Coils and instructions are activated when the combination of contacts at their left gives a wired value, and they can also be parallelised (in that case, they 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. Running example. A rather simple example of a PLC controlling a carriage line is depicted in Figure 1, with the corresponding Ladder program in Figure 2. This example comes from a Mitsubishi Electric training manual for programming PLCs [START_REF]Mitsubishi Programmable Controllers training manual -MELSEC iQ-R Series basic course[END_REF]. To our knowledge, timing charts are generally used to specify programs of comparable size, e.g. Function Blocks, which are kind of library functions that are shipped together with a PLC and a programming environment. We illustrate some principles of Ladder Logic on the first rung of this example: this rung expresses the fact that output Y70 receives the value of the Boolean formula (X0 ∨ Y70) ∧ (¬ M2), i.e. if the corresponding physical devices are activated such that the Boolean formula is true, then Y70 is activated, and is deactivated otherwise.

The program also makes use of the Ladder instructions SET, RST and PLS. The SET instruction activates its device argument (either an internal memory device or an output device) when its input is activated, and does nothing otherwise. For instance, in Figure 2, Y71 is activated when both the common front (X0 ∨ Y70) ∧ (¬ M2) and the internal memory device M1 are activated. The RST instruction is the opposite: the device argument is deactivated when the input is activated. The PLS (pulse) instruction activates its device argument on a rising edge of its input, i.e. when the input has just been activated, then it deactivates its device argument on the next scan.

The diagram also uses a timer instruction on a special device T0 which is activated once the timer finishes. When its input is activated, the instruction sets the threshold (here 30) of the timer and increments a counter. After 30 consecutive scans in which both the common front and output Y73 are activated, Fig. 2: Carriage line control: Ladder program the device T0 is activated (and it remains activated until the input of the timer instruction is deactivated). Specification of expected temporal behaviour. Because of its synchronous nature, the language hardly lends itself to exhaustive functional specifications. Since the work made on AutomationML [START_REF] Drath | AutomationML -the glue for seamless automation engineering[END_REF] by an industrial and academic consortium, the practice, among PLC designers, is to use the timing chart paradigm, which describes the expected temporal behaviour of the PLC for a nominal execution scenario. A timing chart specifies the evolution of outputs over the execution of scans, according to the evolution of inputs. It is made of a succession of events, i.e. scans with either changes of inputs that may lead to changes of outputs, or endings of timers that lead to changes of outputs. Events are separated by stable states, i.e. arbitrary-length successions of scans in which the values of both inputs and outputs are unchanged.

Figure 3 depicts the timing chart specification of the carriage line control example. Events of the timing chart are depicted as 1, 2, . . . , 11. In the rest of the paper, we use the notation (1 → 2), . . . , (10 → 11) to depict stable states. The initial and final states of the timing chart are respectively depicted by idle and end. The timing chart of Figure 3 also contains a fixed-duration sequence of events and stable states (represented by an arrow, between events 5 and 8), whose duration is 3 seconds. We call fixed-duration sequence the concerned sequence of events and stable states. Typically, the Ladder program is executed periodically every 100 milliseconds, therefore, the fixed-time period of 3 seconds is made of 30 scans. Here, the given implementation uses the timer device T0 in order to satisfy this aspect of the specification.

Our main goal is the verification that a Ladder diagram conforms to such a timing chart specification. A first idea would be to envision the use of deductive verification techniques, in the wake of our previous work on Ladder instruction-Fig. 3: Timing chart specification for the Carriage line control level verification [START_REF] Cousineau | Automated deductive verification for ladder programming[END_REF]. However, not all variables used in the Ladder program of Figure 2 are addressed by the timing chart. Indeed, internal memory devices (e.g. M1 and M2) and timers (e.g. T0) are introduced by the developer in order to make the program satisfy its specification, but do not belong to this specification. As an example, in the carriage line control program, the M2 device acts as a termination flag which stops the execution of the PLC as soon as it is activated. There is no doubt that M2 remains false during execution of the timing chart scenario. However, deductive verification would lack this information to check that outputs satisfy their specification. This kind of issue is at the heart of our strategy that is to integrate a method for inferring loop invariants.

Translation of Ladder Programs to WhyML

Our prototype automatically translates Ladder programs given as XML files and timing charts given as PlantUML [START_REF] Roques | PlantUML standard library[END_REF] files into WhyML programs. After a short introduction to the Why3 environment in Section 3.1, we describe in Section 3.2 how we translate the Ladder program itself, and in Section 3.3 how we use this translation for modeling the successive executions of the program and verifying that it satisfies the given timing chart.

The Why3 Environment

Why3 is an environment for deductive program verification, providing the language WhyML for specification and programming [START_REF] Bobot | Let's verify this with Why3[END_REF]. A detailed introduction to Why3 is given in our extended report [START_REF] Belo Lourenço | Formal analysis of Ladder programs using deductive verification[END_REF]. Among the recent features of Why3 of particular interest for our work are the ability to generate loop invariants and to produce counterexamples when a proof fails [8]. Indeed, the first of these features had to be improved in order to support our work on Ladder programs, this is a contribution that some of us made to Why3 [START_REF] Belo Lourenço | Formal analysis of Ladder programs using deductive verification[END_REF].

We illustrate those features on a toy WhyML program presented in Figure 4a. This code involves two global variables, b of type Boolean and x of type integer (a mathematical, unbounded integer in WhyML). The function toy takes no arguments, and is equipped with a formal contract involving a pre-condition (keyword requires) stating that the value of x on function entry is required to lie between 0 and 10, and two post-conditions (keyword ensures) stating respectively that at exit, b is false and that x is smaller than 200. The clause writes expresses which global variables are potentially modified by that function. Notice the WhyML syntax for mutable variables, inspired by ML, requiring to write an exclamation mark to access their values. The body of that function is a simple imperative code involving a while loop and a conditional. This code ends by an other kind of formal annotation, namely a code assertion stating that the value of x must be greater or equal to 75 after the loop.

Given such an annotated code, the Why3 core engine generates three verification conditions (VCs), corresponding to the assertion and the two postconditions. When calling provers for attempting to prove these VCs, only the assertion is proved valid: it directly follows from the negation of the loop condition. None of the post-conditions are proved valid, which is expected in the classical setting of deductive verification, because for proving properties about loops one should state appropriate loop invariants. These could be added by hand, but to make the process more automatic we rely on the automatic generation of such invariants. We use a technique based on abstract interpretation, for which an early prototype existed for Why3 [START_REF] Baudin | Deductive verification with the help of abstract interpretation[END_REF], prototype that we extended in particular to support Boolean variables [START_REF] Belo Lourenço | Formal analysis of Ladder programs using deductive verification[END_REF]. The generated loop invariant is then as follows:

(!b = false ∧ 0 <= !x <= 10) ∨ (!b = true ∧ 2 <= !x <= 51) ∨ (!b = false ∧ 53 <= !x <= 102)
and with this loop invariant, the post-conditions are proved valid.

Assume now that we replace the loop condition with (!x < 300). Still assuming that we ask for generation of a loop invariant, all generated VCs are proved except the second post-condition. For this VC, Why3 proposes a counterexample where the values of b and x at loop exit are respectively false and 300. Indeed, these values satisfy the loop invariant, but with those the post-condition !x <= 200 is not valid.

Translation of Ladder Codes

The translation relies on models of Ladder instructions as WhyML functions, defined by some of the authors in a previous work [START_REF] Cousineau | Automated deductive verification for ladder programming[END_REF]. For example, Figure 4b 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 behaviour of the SET function: if the instruction is activated then the considered device is activated (otherwise its value does not change). The WhyML functions modeling RST, PLS, and timer instructions are detailed in the extended research report [START_REF] Belo Lourenço | Formal analysis of Ladder programs using deductive verification[END_REF].

Given this formalisation of Ladder instructions, we can now give, in Figure 5b, the translation of the full Ladder program of Figure 2. The translation makes use of auxiliary variables f1,. . . ,f8 which corresponds to the common fronts depicted on Figure 5a.

The Ladder loop, and the Encoding of Timing Charts

By definition, timing charts are made of successive events and stable states. Checking that a program conforms to a timing chart means that, under the hypotheses on input values, the values of outputs are correct according to the order of appearance of events and stable states in the timing chart scenario. In addition, fixed-time duration information (timer-related sequence of events) also need to be verified. We propose and implement an automatic process that takes a Ladder diagram and a timing chart specification and returns the corresponding WhyML formalisation.

Events and stable states as loops. The formalisation is made of a succession of do-while style loops4 (except for the initial stable state of the timing chart). The Each do-while loop corresponds to a pair made of an event (the first iteration do) and the following stable state (while). The guard of the loop corresponds to the assumptions on inputs, i.e. the values taken by the inputs at the corresponding event and during the following stable states. The verification conditions on outputs are modelled as loop invariants: the invariant initialisation corresponds to the event while its preservation corresponds to the stable state.

The initial state of the timing chart (values of devices before the PLC starts) is handled in its own way. Basically, all outputs and internal memory devices are initially deactivated. The initial values of inputs are read at the beginning of the timing chart. The initial state is formalised as a while loop (and not a do-while loop) whose guard corresponds to the values of inputs at the initialisation of the timing chart. Indeed, the initial state of the timing chart is a stable state which does not begin with an event. The invariants to be proved for this loop correspond to the fact that outputs remain deactivated.

The events last during one scan, while stable states have an arbitrary duration and end when the next event is reached, i.e. when an input changes or a timer coils. In order to model this behaviour, the body of each loop iteration is enriched with an assignment of the concerned input to a random Boolean value, that may or may not update its value and lead to a new event. The WhyML code of Figure 6 gives an example of formalisation of an event.

It is for the event 1 and the stable state (1 → 2), the latter being terminated when event 2 is reached, i.e. when x0 is deactivated. The encoding of one scan (from Figure 5b) is intentionally duplicated. Deductive verification is unfortunately not sufficient to directly prove the invariants on outputs. Indeed, as mentioned in Section 2, the specification used to generate the formalisation lacks information on internal memory devices. To bypass this difficulty, we rely on the invariant generation plug-in for Why3 (already presented in Section 3.1) to generate additional loop invariants for each while loop of the formalisation. For instance, in each loop of the formalisation, the inference of the invariant not !m2 would be needed.

Timer-related sequences of events. One of the most technical points of our work concerns the formalisation of fixed-duration sequences, e.g. events and stable states from 5 to 8 in the timing chart of the carriage line control (Figure 3).

We have to capture the fact that the total duration of this sequence is exactly 3 seconds. Since timing charts specifications do not make explicit which timer device is used to implement this aspect, we cannot, in the general case, guess which timer device appearing in the code is used for any of the fixedduration sequences appearing in the timing chart. That is why we introduce a fresh internal counter for each fixed-duration sequence of the timing chart, add the duration constraint in the guard of each loop associated to the concerned stable states and increment the value of that counter at each loop iteration. The timer is incremented accordingly, therefore, the counter is supposed to reflect the current value of the timer.

In addition, there are two ways to reach the end of the loops corresponding to intermediate stable states of the fixed-duration sequences: an input change or the maximal number of scans being reached by the counter. We have to capture the fact that the termination of intermediate stable states ( (5 → 6) and (6 → 7) in our example) is due to an input update and not because the maximal number of scans has been reached. To enforce this property, we insert an assume clause after the loop end. In our example, we use c1 as a counter associated with the 3 seconds fixed-duration sequence. As an illustration, we give the shape of the formalisation of event 5 and stable state (5 → 6), ending with the deactivation of X4 while the number of elapsed scans of the fixed-duration sequence is not reached yet. The resulting WhyML code is given in Figure 7. For stable state (7 → 8), i.e. the last stable state before the end of the fixed-duration sequence, there is only one way to end the loop (!c1 >= 29) so there is no need for any assume clause.

Note that the condition we use is !c1 < 29 and not !c1 <= 29 (or equivalently !c1 < 30). The reason is technical: at the end of the stable state (7 → 8), the counter reaches the value 29. The timer's current value is also equal to 29. The scan for event 8 begins and the current value of the timer is incremented during its execution (more precisely at rung 5), therefore, its value becomes equal to 30 and the timer coils.

At this stage, another pitfall remains. As explained previously, we cannot, in the general case, make explicit the equality between the introduced counter c1 and the current value of the timer in the formalisation of Figure 7. Nonetheless, we can benefit from the invariant inference mechanism presented in Section 3.1. Indeed, this invariant generator does not only compute numerical domains for each variable independently: it makes use of relational domains (provided by the Apron library [START_REF] Jeannet | Apron: A library of numerical abstract domains for static analysis[END_REF]) to infer logical relations between variables. In particular, we successfully obtain the invariant !c1 = t0.current that makes explicit the role of the introduced counter.

Implementation and Experimental Results

Our first goal is to be able to fully automatically prove that a Ladder program like our running example of in Figure 2 is conforming to a timing chart. Our secondary goal is that we want to give back, to the users, meaningful and easyto-use information when they try to prove an incorrect implementation.

In Section 4.1, we describe the workflow of the proprietary implementation of our approach. Then, Section 4.2 presents the results obtained when executing the analysis on a correct carriage line control implementation, i.e., the implementation of Figure 2. Finally, in Section 4.3, we present the feedback given by our toolbox when analysing one slight modification of the nominal program that makes the verification of conformance to the timing chart fail.

Overview of the Approach

The implemented approach proceeds as follows. -Why3 infers a loop invariant for the WhyML loop that models the state that is associated to the event, thus adding information on values of internal memory to the information on output values computed in the previous step. -Why3 computes the verification conditions that correspond both to the inferred invariants and the invariants that correspond to the timing chart specification, and dispatches them to SMT solvers. 5. The previous step is repeated for all events. Note that besides the hypotheses on the values of inputs and outputs at the start of the event, which are given by the timing chart, the proving process also needs hypotheses on the values of internal memory values at the beginning of the event. Those values are given by the loop invariant inferred for the previous event. Hence we store, during the process, the inferred invariants for each event in order to use them as preconditions for the next event. 6. If a proof obligation fails at event n, we build a WhyML program concatenating all the previous events and the faulty one, with loops enriched with the consecutively inferred invariants. Provers are called on this WhyML program and provide counterexamples (see Section 4.3). 7. On the contrary, if all events and stable states are proved, we conclude that the Ladder program satisfies the timing chart specification.

This approach of proving each event, one by one, until a specification violation is detected, is motivated by the fact that abstract interpretation, in our examples, is far more time-consuming than proving. In the case a violation is detected, our approach avoids to launch abstract interpretation for all the events that follow the one for which the violation has been detected.

Results on correct code

We apply our approach on the nominal Ladder program described in Figure 2, for which we successfully verify the timing chart specification. Figure 8 depicts the result we obtain when running the analysis. In accordance with our strategy presented in Section 4.1, we consecutively infer invariants and then prove verification conditions for each pair (event, stable state), starting from the initial (idle) state of the timing chart. We observe that abstract interpretation is for now quite expensive, therefore, the proof time is negligible (6s) compared to the time for inference of invariants (137s).

Results on incorrect code

Let us assume the verification of a proof obligation fails for a faulty event (the case of a faulty stable state is similar). Our goal is to provide the most relevant information possible to the Ladder programmer, who may not be used to deductive verification. For that purpose, we propose an error scenario following the timing chart until the faulty event, mixing concrete values provided by counterexamples generated by Why3, and abstract domains provided by abstract interpretation.

Error scenarios. When a proof obligation fails as assumed above, Why3 is able to provide a counterexample. Since such a proof obligation comes from the verification of the concatenation of the consecutive events from the very first one to the faulty one, the information we get provides the values of the inputs, outputs and internal devices at the beginning of each event until the faulty one. Due to the way Why3 handles loops during the computation of verification conditions for SMT-solvers (that is, the loop invariant is the only known fact for the code after the loop [START_REF] Belo Lourenço | Formal analysis of Ladder programs using deductive verification[END_REF]), we do not have any information on the values the devices take during the stable states. We think that this lack of information concerning values of devices during stable states may be an impediment to the understanding of the cause of the specification violation. That is why we propose to enrich the counterexample values with the domains of devices values given by abstract interpretation. This leads to the notion of error scenario that provides:

1. For each event that precedes the faulty one (including the faulty one), the values of devices before the beginning of the scan of this event, obtained from the counterexample trace provided by Why3. 2. For each stable state that precedes the faulty event, an over-approximation of domains of devices values, obtained by abstract interpretation. In order to convince ourselves that this notion of error scenario should be useful to Ladder programmers, we implemented different slight modifications of the carriage line control program, introducing bugs. We present one of them in this article, another one is described in the extended research report [START_REF] Belo Lourenço | Formal analysis of Ladder programs using deductive verification[END_REF]. The corresponding Ladder diagram is depicted in Figure 9. The modification compared to the original code is circled.

The timer setting duration is here set to 40 scans instead of 30. We use our tool to get the reason of the proof failure, i.e. that Y73 is equal to true while it should be false. The obtained reason is rather intuitive: event 8 corresponds to 30 elapsed scans from timer's start. As the timer has a duration of 40 scans, it has not ended yet, therefore, Y73 is not reset yet, as highlighted by the error scenario of Figure 10a.

The trace shows that the setting value of the timer (here 40) is not reached. In particular, the current value of the timer evolves between 3 and 29 in the stable state between events 7 and 8, showing that the current event follows three other events in the fixed-duration sequence. Moreover, at the beginning of the scan of event 8, the current value of the timer and its associated counter c1 are both equal to 29, which is exactly the value we expect when leaving the fixed-duration sequence of events. The timing chart violation is depicted by Figure 10b.

Qualitative analysis of the experiments. As a conclusion, we think that this notion of error scenario mixing concrete values provided by counterexamples to VCs, and abstract domains provided by abstract interpretation, should be useful to Ladder programmers in order to understand why a program does not conform to a given timing chart specification. A weakness of this approach is that in some cases, the concrete and abstract values might seem irrelevant. For example, for a timer counter c, we might have an abstract domain that states that c can take all the values between, say, 3 and 29 for a state, but the concrete value given for the next event might be 4. For that example, it means that the loop corresponding to the state is executed exactly once in the error scenario, before executing the next event. In that case, it might be very interesting to use the concrete values of counterexamples to refine the domain [3;29] into [3;4], and even make explicit to the programmer that there is exactly one execution of the program for the considered state.

We presented a new method for formally verifying that a given Ladder code complies with an expected temporal behaviour expressed by a timing chart. By translating both the Ladder code and the timing chart to a WhyML program, and making use of the loop invariant generation capability of Why3, we are able to provide a fully automatic process to achieve 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 error scenario which exposes why the Ladder code does not conform to the timing chart. Our method 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 counterexample scenarios on wrong mutants.

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 timing chart, which is described in Section 3. It also relies on the soundness of the VC generation process of Why3, which is not formally proven correct but validated on numerous applications [START_REF] Bobot | Let's verify this with Why3[END_REF]. Regarding trust in Why3, it is important to notice that the prototype implementation of loop invariant generation is not part of the trusted code base, because the loop invariants generated are later on checked for validity by the VC generation process. It is indeed fortunate to not have to rely on the soundness of this part of Why3 implementation, since we had to make significant extensions to it (mostly, support for Boolean variables, and adaptation of the API for external use) for the current purpose. The last part of the tool chain that must be trusted is the back-end SMT solver.

Regarding the generated errors scenarios, we have noticed that they are satisfactory on our case study, but due to the inherent incompleteness of countermodel generation with SMT solvers, we cannot guarantee that the generated scenarios are always valid. There are on-going work in the Why3 development team to increase the trust into the validity of generated counterexamples [START_REF] Becker | Explaining counterexamples with giantstep assertion checking[END_REF].

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. In 2014, Ovatman et al. [START_REF] Ovatman | An overview of model checking practices on verification of PLC software[END_REF] published a summary of those techniques. In 2016, Darvas et al. [START_REF] Darvas | Formal verification of safety plc based control software[END_REF] proposed a newer model-checking based tool and compared with former similar tools. The general drawback of the model-checking approach is that the verification it provides cannot be exhaustive, it cannot model any possible number of executions during the states of a timing chart, contrary to deductive verification. On the other hand, abstract interpretation has also been used for a long time for verifying software, in particular microcontroller software [START_REF] Fehnker | Automatic bug detection in microcontroller software by static program analysis[END_REF][START_REF] Nguyen | Integrating static program analysis tools for verifying cautions of microcontroller[END_REF] and PLC software [START_REF] Biallas | Efficient handling of states in abstract interpretation of industrial programmable logic controller code[END_REF] (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 properties. Finally, in a previous work [START_REF] Cousineau | Automated deductive verification for ladder programming[END_REF], some of us used the Why3 deductive verification platform for detecting run-time errors of Ladder programs. This work only considered one single execution of Ladder programs and was therefore also not suited for verifying temporal properties. To our knowledge, the present paper is the first one to combine abstract interpretation and deductive verification for verifying temporal properties of Ladder programs.

Outside the context of Ladder, Stouls and Groslambert proposed an approach for proving temporal properties of C code [START_REF] Stouls | Vérification de propriétés LTL sur des programmes C par génération d'annotations[END_REF], based on a translation from LTL formulas into annotations in the ACSL language [START_REF] Baudin | ACSL: ANSI/ISO C Specification Language, version 1.16[END_REF]. These LTL formulas express temporal properties of sequences of functions calls, which are very different from our kind of specifications. Their approach is similar to ours in the sense that they automatically translate temporal properties into annotated code, to be proved correct using deductive verification. They also identified a need for automatically generating extra intermediate annotations, for which they use their own variant of abstract interpretation. A successor of this work is the CaFE plug-in of Frama-C [START_REF] De Oliveira | Au temps en emporte le C[END_REF], which makes use of the Frama-C plug-in EVA for abstract interpretation. Unlike us, the approaches above do not provide any facilities for explaining errors.

Future work. During our work, we had to improve the loop invariant generation feature of Why3, in particular the support for Boolean values. Even enough for our case study, there is clearly room for improvement in this implementation, required to make the tool chain more efficient. 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.

As mentioned at the end of Section 4.3, there is some need for improvement in the counterexample generation part of the chain. The inherent incompleteness of the SMT solvers implies that the proposed counterexample might be wrong. We are planning to incorporate in our tool-chain a recent technique that doublechecks the validity of counterexamples a posteriori [START_REF] Becker | Explaining counterexamples with giantstep assertion checking[END_REF], which roughly amounts to symbolically executing the scenario it describes, and detect carefully at which step its behaviour diverges from what the timing chart allows.

On the error scenario side, as explained in the end of Section 4.3, the parts of a scenario that come from abstract interpretation domains, that correspond to the possible values of devices during states, could be refined using the concrete values given by the counterexamples for next events. This way, we might propose an even more understandable and useful error scenario to Ladder programmers, in case an error is detected in their code.

A longer-term goal is to augment the trust in the translation from Ladder to WhyML. We have some plans for designing a systematic and automatic validation process to confront our translation against existing test suites for Ladder programs.

Fig. 1 :

 1 Fig. 1: Carriage line control: System description

Fig. 4 :

 4 Fig. 4: Examples of WhyML code

  (a) Ladder code with common fronts let f1 = (!x0 || !y70) && (not !m2) in y70 := f1; let f2 = !x1 && !x3 in pls (f1 && f2) m1 cc0; let f3 = !m1 in set (f1 && f3) y71; let f4 = !y71 && !x2 in rst (f1 && f4) y71; set (f1 && f4) y73; let f5 = !y73 in timer_coil (f1 && f5) t0 30; let f6 = timer_contact t0 in rst (f1 && f6) y73; set (f1 && f6) y74; let f7 = !y74 && !x4 in rst (f1 && f7) y74; set (f1 && f7) y72; let f8 = !y72 && !x3 in rst (f1 && f8) y72; m2 := f1 && f8 (b) WhyML encoding

Fig. 5 :

 5 Fig. 5: Encoding of one scan of the Ladder program for the carriage line control

<Fig. 6 :

 6 Fig. 6: WhyML formalisation of event 1 and stable state (1 → 2)

<Fig. 7 :

 7 Fig.7: WhyML formalisation of event 5 and stable state(5 → 6)

1 .

 1 The tool takes two inputs: an XML representation of the Ladder program, and a timing chart specification written in the PlantUML language. 2. It translates the Ladder program as a WhyML program. 3. It derives, from the timing chart the different guard conditions (hypotheses on input values) and invariants (output values to prove) for formalising the successive events of the timing chart. 4. Then, for each event,

Fig. 8 :

 8 Fig. 8: Output of the tool on the nominal carriage line control program

Fig. 9 :

 9 Fig. 9: An incorrect version of the carriage line control

  (a) Output of the tool (b) Violation of the timing chart

Fig. 10 :

 10 Fig. 10: Incorrect Ladder program: analysis results

There are no do-while loops in WhyML, we just mean by do-while style loop a code piece of the following form with two occurrences of the loop body: "body; while cond do body done"

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