T Ranger
email: tom.ranger@univ-reims.fr

A Philippot

B Riera

Algebraic Synthesis of Safety Logical Filter on Manufacturing Systems

Keywords: Discrete Event Systems, Programmable Logic Controllers, Safety, Formal Methods, Algebraic Approaches

This work focuses on the management of safety constraints for the control of cyberphysical manufacturing systems. A methodology for constructing a set of constraints to ensure the safety of an existing control law is proposed. The resolution of this constraint set is performed using algebraic synthesis. This tool facilitates the implementation of a logic filter in a way that complies with IEC 61131-3.

INTRODUCTION

In this article, we will focus on the control of industrial manufacturing systems. These systems being controlled by Programmable Logic Controllers (PLCs) they can be modeled by discrete event systems (DES) [START_REF] Cassandras | Introduction to discrete event systems[END_REF] with logical Inputs (sensors), logical Outputs (actuators) and internal variables (observers). The development of Industry 4.0 requires new design paradigms for the control of cyber-physical manufacturing systems. One of them being the ability to ensure operational safety. In order to guarantee this reliability we decided to use formal approaches. The most common one discussed in the literature is Supervisory Control Theory (SCT) [START_REF] Ramadge | Control of discrete event systems[END_REF]. However, the use of PLCs imposes a synchronous operation which is opposed to the asynchronous character of finite state automata used in SCT. Moreover, the SCT addresses the problem of supervisor synthesis where it is necessary to obtain controllers for implementation in a PLC. The difference between the 2 is major, indeed where a supervisor will limit the evolution of the system by remaining as permissive as possible a controller will force to follow a single path. This is why we decided to use an approach based on the use of safety constraints placed after the controller in order to act as a logical safety filter [START_REF] Pichard | Safety of manufacturing systems controllers by logical constraints with safety filter[END_REF] to compensate for possible safety flaws in the PLC program. This kind of filter can be applied to any control program, for which it is necessary to be exhaustive when writing the safety constraints because no assumption can be made on the control law. They can also be defined in conjunction with the control law, this approach simplifies the definition of these two elements [START_REF] Zaytoon | Synthesis and implementation of logic controllers -a review[END_REF]. The previous work used a SAT solver minimizing the Hamming distance to solve the security constraints, which involved implementing an online solving algorithm. Another method of solving the constraints is therefore preferred.

The use of algebraic synthesis [START_REF] Hietter | Algebraic synthesis of dependable logic controllers[END_REF] was chosen. This approach allows the solution of systems of Boolean equations. The solution obtained is presented in the form of a logical relation, which allows to get rid of the online solution algorithm.

The first part of this article presents the notion of logic filter and the use of algebraic synthesis as a solution tool. In the second part a methodology for the implementation of a logic filter using algebraic synthesis is presented. Finally the use of this method is illustrated in the last part.

STATE OF THE ART

All the equations in this paper are based on Boolean algebra (B, +, ., , 0, 1) (Definition 15.5 of [START_REF] Grimaldi | Discrete and Combinatorial Mathematics: An Applied Introduction[END_REF] where "+", ".", " " are respectively the logical operators OR, AND and NOT.

Logical filter

The principle of operation of a logic filter is to insert a validation block at the end of the control program. The purpose of this block is to detect possible violations of safety constraints among the whole output vector. The detection of one of these violations can lead to the blocking of the system in a stable state or to the modification of the output vector in order to ensure the respect of the safety constraints.

Our approach of logical filters is based on the one developed at CReSTIC [START_REF] Marangé | Prevention of human control errors by robust filter for manufacturing system[END_REF], [START_REF] Pichard | Safety of manufacturing systems controllers by logical constraints with safety filter[END_REF]. A logical filter takes place after the program execution as shown in figure 1. Two kinds of modifications can occur to the command law. In the case of a blocking filter, a constraint violation will lead the system to a predetermined and stable state. In the case of a corrective filter, a constraint violation will lead to an output adjustment to fit with the filter constraint set. The contribution of Pichard (2018a) to logical filter brings a formalism to the definition of logical constraints which enable him formal verification for logical filter consistency. Work on solving systems of Boolean equations [START_REF] Roussel | Design of Logic Controllers Thanks to Symbolic Computation of Simultaneously Asserted Boolean Equations[END_REF] is used to check the consistency of the set of constraints. In Pichard's work he distinguishes two types of constraints, simple constraints and combined constraints. These constraints are made of unknown (actuator) and known variables (input PLC variables). Simple constraints have only one unknown variable, while combined constraints have several.

As a simple example, let us consider i 1 a known variable and O 1 and O 2 2 unknown variables. For instance equation 1 is a simple constraint and equation 2 is a combined constraint.

CSs 1 = i 1 .O 1 (1) CSc 1 = O 1 .O 2 (2)
A constraint is considered satisfied if it is equal to 0. The objective being to define a control logic filter, the violation of one or more constraints must lead to a modification of the output vector. While solving simple constraints is straightforward, solving combined constraints requires additional information. Indeed, equation 2 can be solved in 3 different ways:

(1)

O 1 = 1 and O 2 = 0 (2) O 1 = 0 and O 2 = 1 (3) O 1 = 0 and O 2 = 0
The choice of the variable to be set to 1 in priority will then be indicated between brackets when defining the constraint. If both are to be set to 0, no further indication is given. The constraint Cc 1 is then defined as follows if the priority is given to O 1 :

Cc 1 = O 1 .O 2 [O 1 ] (3)
This problem has been identified as a boolean satisfiability problem which is abbreviated as SAT (Vizel et al., 2015).

A SAT solver has therefore been implemented to solve this problem (Pichard et al., 2018a). This solver will provide an output vector conforming to the safety constraints at each PLC cycle. This vector is chosen using the Hamming distance. This distance measures the deviation from the output vector proposed by the control law. The vector provided at the end of the resolution algorithm is therefore the one minimizing this Hamming distance.

However the implementation of this solver is also the weak point of the method. Indeed, the implementation of an online solving algorithm has a major drawback. The convergence time of the algorithm being variable, it can lead to uncontrolled cycle times. In particular if the cycle time of the automaton reaches the characteristic time of evolution of the system. This is why we decided to turn to another tool to synthesize a control logic filter.

Algebraic synthesis

The use of algebraic synthesis as a solving tool has been retained for the implementation of control logic filters. Algebraic synthesis is a method for solving systems of Boolean equations.

Initially algebraic synthesis was developed at LURPA by [START_REF] Hietter | Algebraic synthesis of dependable logic controllers[END_REF]. The original idea was to use the results of [START_REF] Brown | Boolean Reasoning[END_REF] to generate the control law by solving a Boolean equations system. Hietter's work has focused on formalizing mathematical tools for solving systems of Boolean equations. These tools allow to obtain a parametric solution to a problem formed by a set of Boolean equations. The existence of a solution is guaranteed by the verification of a consistency condition.

The latest theoretical results on the domain come from Hélène [START_REF] Leroux | Algebraic synthesis of logical controllers with optimization criteria[END_REF]. This paper brings optimisation criteria. These criteria allow to orient the choice of a solution.

There are 2 types of criterion, the maximisation and the minimisation. These criteria are defined by a logical expression that will be maximised or minimised. The set formed by the constraint system and the optimization criteria is the problem to solve. This resolution takes place in 4 steps:

(1) Computation of parametric solutions by solving the constraint system without applying criteria (2) Computation of an optimization criterion by replacing the unknown variables by the parametric solutions computed in step 1 (3) Addition of the expression of the criterion in the set of equations and resolution of this new system to obtain a new parametric solution (4) Repeat steps 2 and 3 to apply a new criterion

The criteria being applied one after the other, their order of definition has an impact on the solution.

The use of these criteria to guide the choice of a solution is presented bellow.

For instance, consider O 1 and O 2 2 unknown variables and i 1 a known variable. The following constraint is defined:

O 1 .O 2 = 0 (4)
At the end of the first step, as defined in Theorem 11 [START_REF] Roussel | Design of Logic Controllers Thanks to Symbolic Computation of Simultaneously Asserted Boolean Equations[END_REF] the following parametric expressions is obtained:

O 1 = p 1 O 2 = p 1 .p 2 (5)
With p 1 and p 2 arbitrary parameters.

Then the objective is to get rid of the parameters by applying the following preferences:

• when i 1 is true, we want O 1 to be true

• O 1 must be true as less as possible

• O 2 must be true as much as possible Therefore the following criteria are defined:

M ax(i 1 .O 1 ) (6) M in(O 1 ) (7) M ax(O 2 ) (8)
The resolution of the first criterion (equation 6) is presented bellow:

M ax(i 1 .O 1 ) = i1 (9)
The new equation to solve is:

i 1 .O 1 = M ax(i 1 .O 1 ) ⇔ i 1 .p 1 = i 1 ⇔ i 1 .p 1 .i 1 + i 1 .p 1 .i 1 = 0 ⇔ i 1 .p 1 = 0 (10)
This new equation is solved considering p 1 the unknown variable. The following parametric solution is obtained by injecting the value of p 1 obtained in the first solution:

O 1 = i 1 + p 1 O 2 = p 2 .p 1 .i 1 (11)
With p 1 an arbitrary parameter. The application of the second criterion (equation 7) provides the following parametric solution:

O 1 = i 1 O 2 = p 2 .i 1 (12)
Finally the application of the last criterion (equation 8) gives:

O 1 = i 1 O 2 = i 1 (13)
Therefore, a unique solution is obtained after applying 3 optimization criteria. However we can observe that the last two criteria removed 1 parameter while the first one only provided a new parametric solution. As we want to reach a unique solution in order to implement it in a PLC we need to know under which conditions a criterion effectively removes a parameter. We have therefore defined a sufficiency condition to make a parameter disappear from a parametric solution.

Theorem 1. (Parameter reduction condition theorem). For an optimization criterion to remove the parameter associated with an unknown variable x, it is sufficient that it is of the form:

M in(ax + bx) (14)
or M ax(ax + bx) (15) where a, b ∈ B such as a = b Proof. To prove the theorem we will show that the sufficiency condition implies the removal of the parameter for both forms of criteria.

We will start with the maximization criterion. Let us consider the following equation with one unknown f (x) = 0. According to Theorem 10 of [START_REF] Roussel | Design of Logic Controllers Thanks to Symbolic Computation of Simultaneously Asserted Boolean Equations[END_REF] this equation can be put in the following canonical form: f (0).x + f (1).x = 0 (16) as presented in [START_REF] Leroux | Algebraic synthesis of logical controllers with optimization criteria[END_REF] the result of the solution of this equation to which we apply the criterion:

M ax(ax + bx) (17) is: x = f (0) + a.b.f (1) +p.(a.f (1) + b.f (1)) ( 18
)
in this case if a = b:

x = f (0) + a.a.f (1) + p.(a.f (1) + a.f (1)) = f (0) + a.f (1) + p.a.f (1) = f (0) + a.f (1) (19)
For the minimization criterion the solution is :

x = f (0) + a.b.f (1) +p.(a.f (1) + b.f (1)) (20)
And in the same way we obtain:

x = f (0) + a.f (1) (21) In both cases the result of the application of the criterion gives a solution without parameters.

In order to obtain a unique solution for a system of equations with n unknowns, it is sufficient to apply 1 criterion respecting the reduction condition to each of these variables. It is important to note that the criteria being applied one after the other the criteria not respecting this condition must be defined first in order to have an impact on the solution.

SETTING UP A SAFETY FILTER

Our goal is to apply a safety filter using algebraic synthesis for any control law. In existing works on logic filters the set of constraints was always considered as well constructed. In this section we will propose a method to obtain this set by performing a system analysis.

System analysis

The first step for the implementation of a safety filter goes through a system analysis. This analysis is used to identify potential sources of risks for the system. The first step is to identify all the risk areas in the system. Then for each of this area every situation that can lead to a safety issue must be defined. Finally a set of constraints is drafted to prevent the occurrence of these situations.

In order to identify these situations the following questions must be asked for each area identified:

• Is there any risk of collision if some actuators are operated simultaneously? • Is there any risk of cluttering the system if some actuators are not activated together? • Can the actuators be controlled in a way that damages them?

Problem formalization

Now that the safety constraints are written we will show how to define problem that will be solved by algebraic synthesis.

The definition of the constraints is different from the one used by Pichard (2018a). Indeed, even if they were defined as logical equations, additional indications were provided for the combined constraints. Moreover, the definition of an algebraic synthesis problem requires more than the constraints redaction. It is also necessary to ensure that a unique solution is obtained. For simple constraints, they are defined in the same way as in Pichard's work. The difference appears for the combined constraints, in particular for the choice of the solution. Additional variables are also used to define the problem. These are known variables representing the request of the execution of an actuator by the control law. If the actuator variables are of the form O i these execution requests are of the form R O i .

The choice of the solution to be prioritized in the case of combined constraints is made using the optimization criteria. Let us go back to the combined constraint example presented earlier:

Cc 1 = O 1 .O 2 [O 1 ] ( 22
)
The formalization of this constraint in the framework of the algebraic synthesis is carried out in two steps.

Writing a Boolean constraint equation:

O 1 .O 2 = 0 (23) The definition of an optimization criterion: M in(R O 1 .R O 2 .O 1 ) (24)
This criterion is interpreted as follows, in the case where O 1 and O 2 are requested simultaneously O 1 must be minimize. This has the effect of favouring the solution O 1 = 1 and O 2 = 0.

In the same way that R. Pichard used a solver minimizing the Hamming distance, we want the value of the actuator variables to be as close as possible to the demands of the control law. We therefore define similarity variables between the actuator execution requests and the final values of these actuators. Optimization criteria are then defined to maximize these similarity variables.

For our example the similarity variables will be expressed as follows: Box at the end of the turntable C 7

Sim O 1 = R O 1 .O 1 + R O 1 .O 1 Sim O 2 = R O 2 .O 2 + R O 2 .O 2 (25)
Box at the beginning of the right exit conveyor C 8

Box at the beginning of the left exit conveyor C 9

Box at the end of the right exit conveyor C 10

Box at the end of the left exit conveyor

And the criteria will be defined as follows:

M ax(Sim O 1 ) M ax(Sim O 2 ) (26)
For these criteria if we take a = R O 1 and b = R O 1 the condition a = b is well verified. These criteria ensure the uniqueness of the solution.

APPLICATION OF THE METHOD TO AN ACADEMIC BENCHMARK

In order to illustrate the application of control logic filters by algebraic synthesis, we use the example presented in [START_REF] Pichard | Csp solver for safe plc controller: Application to manufacturing systems[END_REF].

Notations

The following notations is used:

• X -1 : Variable X at the previous cycle of the PLC ;

• ↑ X = X -1 .X: Rising edge of variable X ;

• ↓ X = X -1 .X: Falling edge of variable X.

Benchmark presentation

This system is represented in figure 2 and his inputs and outputs are detailed in tables 1 and 2.

In addition to these inputs we use 2 observers named P 01 and P 36 which indicates the presence of a box respectively between the sensors C 0 /C 1 and C 3 /C 6 Right exit conveyor

Filter definition and implementation

In the box sorting system we can identify 5 risk areas :

(1) Connection between the two supply conveyors;

(2) Connection between the second supply conveyor and the turntable;

(3) Connection between the turntable and the right exit conveyor; (4) Connection between the turntable and the left exit conveyor;

(5) The turntable.

The situations to be avoided are now defined for each of these risk areas as well as the safety constraints to avoid them. The list of these situations and their associated constraints are presented in the table 3.

We can notice that a single constraint can be used to avoid several situations. Now this set of constraints needs to be into an algebraic synthesis problem. The constraints 27 and the optimization criteria 28 and 29 have to be defined.

                                                                     P 01 .A 0 = 0 C 0 .A 0 .A 1 = 0 C 3 .C 4 .A1 = 0 C 3 .(C 6 + P 36 ).A1 = 0 C 3 .C 4 .A 1 .A 2 = 0 ↑ A 4 .(A 2 + A 3 ) = 0 C 4 .↑ C 6 . ↓ A 2 = 0 ↓ A 4 .(A 2 + A 3 ) = 0 C5.↓ C 8 . ↓ A 2 = 0 C5.↓ C 7 . ↓ A 3 = 0 C 5 .C 6 .A 3 = 0 C 5 .C 6 .A 2 = 0 A 2 .A 3 = 0 (27)
C 3 .C 4 .A 1 .A 2 [A 2 ]
The turntable cannot be turned towards the exit if its conveyors are used (2)

↑ A 4 .(A 2 + A 3 ) [A 2 + A 3 ] A loading cannot be stopped until it is completed (2) C 4 .↑ C 6 . ↓ A 2 An unloading by A 3 cannot be stopped until it is completed (3) C5.↓ C 7 . ↓ A 3
The turntable cannot be turned towards the supply if its conveyors are used (3)

↓ A 4 .(A 2 + A 3 ) [A 2 + A 3 ]
The turntable cannot be turned towards the supply if its conveyors are used (4) An unloading by A 2 cannot be stopped until it is completed (4)

C5.↓ C 8 . ↓ A 2
The turntable cannot be unloaded by A 3 if it is not aligned with the exit conveyors (5)

C 5 .C 6 .A 3
The turntable cannot be unloaded by A 2 if it is not aligned with the exit conveyors (5)

C 5 .C 6 .A 2
The turntable conveyors cannot be operated in both directions simultaneously (5)

A 2 .A 3                        M in(R A 0 .R A 1 .C 0 .A 1 ) M in(C 3 .C 4 .R A 1 .R A 2 .A 2 ) M in(A -1 4 .R A 4 .(R A 2 + R A 3 ).(A 2 + A 3 )) M in(A -1 4 .R A 4 .(R A 2 + R A 3 ).(A 2 + A 3 )) M in(R A 2 .R A 3 .(A 2 + A 3 )) (28)                                  M ax(Sim A0) M ax(Sim A1) M ax(Sim A2) M ax(Sim A3) M ax(Sim A4) M ax(Sim A5) M ax(Sim A6) (29)
The solution of this problem provides the solutions presented in 30. As the filter only consists of logical relations, it can be directly implemented in ladder or ST code in a PLC in order to be IEC 61131-3 compliant.

                                                 A 0 = R A 0 .P 01 .(C 0 + A 1 ) A 1 = R A 1 .(C 3 C4.C 6 .P 36 .(A -1 2 + R A 2 .R A 3 )) A 2 = A -1 2 .(C 4 .C 6 + C 5 .↓ C 8 ) + R A 2 .R A 3
.(C 6 .(C 4 + C 5 ) + C 5 .(A -1 2 + A -1 3 + ↓ C 7 ))

A 3 = A -1 3 .C 5 .↓ C 7 + R A 3 .R A 2 .(C 5 .(A -1 2 + ↓ C 8 ) +C 6 .(A -1 2 + C 4 .C 5 ) + C 4 . ↓ C 6 ) A 4 = A -1 4 .(A 2 + A 3 ) + R A 4 .(A -1 4 + C 4 .C 6 + A 2 .A 3 ) A 5 = R A 5 A 6 = R A 6 (30)
Compared to the filter proposed by Pichard (2018a) we obtain a similar functional behavior using the control law proposed in his paper. Moreover the Hamming distance has been computed online and in both cases the maximum observed distance is 3. The filter obtained using algebraic synthesis thus has a behavior similar to that using an SAT solver without the need to implement an online solver.

CONCLUSION

In this paper we have presented a method for defining a corrective logic filter to ensure compliance with security constraints. This filter is implemented using algebraic synthesis as a tool to solve the set of security constraints. This allows for an easily implementable solution that does not require the use of an online resolution algorithm. Since this filter only takes into account the security aspects, it does not guarantee that the expected functional behavior is respected. Indeed, in the case of a poorly designed control law, the application of a safety filter can lead to a system block. In this case the filter can be used to identify the defects of the control law to correct them. We also plan to develop a filter to ensure the liveliness of the system in our future work.

Fig. 1 .

 1 Fig. 1. Principle of implementation of the logic filter in a PLC

Fig. 2 .

 2 Fig. 2. Box sorting system

Table 1 .

 1 System Inputs Box at the end of the second supply conveyor C 4 Turntable aligned with supply conveyors C 5 Turntable aligned with exit conveyors C 6

	Inputs	Description
	C 0	Box between the two supply conveyors
	C 1	Box at the case detection
	C 2	Box detected
	C 3

Table 2 .

 2 System Outputs

	Outputs	Description
	A 0	First supply conveyor
	A 1	Second supply conveyor
	A 2	Turntable conveyor direction 1
	A 3	Turntable conveyor direction 2
	A 4	Rotation of the turntable
	A 5	Left exit conveyor
	A 6

Table 3 .

 3 Situations to avoid and associated safety constraints

	Situation to avoid	Safety constraints
	Pallets should not touch each	P 01 .A 0
	other (1)
	We cannot load a part on the	C 0 .A 0 .A 1 [A 1 ]
	A 1 if it is stopped (1)
	A part cannot be loaded on the	C 3 .C 4 .A1
	turntable if it is not aligned
	with the supply conveyors (2)
	It is not possible to load a	C 3 .(C 6 + P 36 ).A1
	part on the turntable if one is
	already on it (2)
	It is not possible to load a
	part on the turntable if the
	conveyor A2 is stopped (2)

ACKNOWLEDGEMENTS

This paper is carried out in the context of the HUMANISM ANR-17-CE10-0009 research program, funded by the ANR "Agence Nationale de la Recherche". This project involves three laboratories in Automatics Sciences and in Human Factors, CReSTIC (Reims), Lab-STICC (Lorient), and LAMIH (Valenciennes).

The authors gratefully acknowledge these institutions.