JP2024501588A - Computer-implemented method to check correctness of PLC program - Google Patents

Abstract

The present invention relates to a method for checking the correctness of a PLC program described by a functional specification, usually shown as a timing chart. This method consists of converting a PLC program into a model, converting a timing chart and integrating this timing chart into the model, and calculating the abstract semantics to finally solve the missing information in the timing chart. In order to satisfy the timing chart verification, the characteristics to be verified from the model and default PLC formalization instructions are predicated and deduced, and it is clarified whether the above characteristics are always verified. checking or providing a counterexample; converting the counterexample into a PLC model error event initial configuration; simulating execution; assembling state variable values and event execution variable values; and converting it back into a program.

Description

The present invention relates to programmable logic controllers.

A programmable logic controller (hereinafter referred to as "PLC") is an industrial digital computer used in manufacturing processes such as assembly lines or as an automation controller for robotic devices.

PLCs replace hard-wired relays, timers and sequencers and can be simulated by software that represents the calculation of outputs from inputs and internal memory values.

Typically, the IEC61131-3 standard defines several programming languages that can be used to develop PLC software, such as ladder logic, function blocks, structured text, among others. Ladder logic represents a PLC program in a graphical diagram using, for example, a relay logic hardware circuit diagram, whereas structured text is a textual programming language.

In traditional software development, most of the development time is spent on debugging. Particularly in the case of factory automation (FA), program debugging is very important because if a bug occurs in a factory, it costs a lot of money in terms of human and property damage, as well as plant shutdown time. In particular, debugging PLC programs is difficult and requires a lot of time and cost. A bug can be thought of as a violation of certain properties of the program regarding its input/output and local memory values at some point in the program.

The purpose of debugging is to detect property violations during code creation before executing it, that is, to find initial values of inputs and internal memory that result in property violations when the program is executed. Since it is nearly impossible (and too expensive) to check every executable behavior of a program, the usual practice is to develop and run a few tests (i.e. (run the program against the configuration and check its behavior).

However, tests are not exhaustive in nature and their development is very costly and time consuming.

A solution to circumvent these limitations is to perform formal deductive verification.

Deductive verification is based on checking that a program yields the intended behavior and results for all possible executions, given some assumptions. The principle of using deductive verification to check that a PLC program is free of runtime errors is disclosed in the document US Pat. .

In the case of high-level characteristics, the intended behavior of a PLC program is usually described as a timing chart, ie, a change in output value over time according to a change in some input value. As an example, timing chart specifications are shown in FIG. Changes in the X variable reflect hypotheses about the input values, while changes in the Y variable represent expected output values.

A change in input value (or expiration of a timer) is referred to herein as an "event." Such an event corresponds to one execution of the PLC program. Verifying the specifications means verifying that the output value changes (or does not change) at each event according to the timing chart and that the output value does not change between two events. The intervals between these events are referred to herein as "states" and correspond to an indefinite number of consecutive executions of the PLC program.

Two known methods can be mentioned as methods for verifying that a PLC program satisfies timing chart specifications.

"Test" is the first and most common. The test is to run the program from an initial configuration with different scenarios for different changes (only the number of runs in a state can change, the order of input changes given by the timing chart does not change). The problem with testing is that it is not efficient enough. Running many different configurations is costly in terms of human and computer processing (CPU) time, and the number of differently timed input evolutions is infinite, so it is not recommended to test every run. is not possible, and testing cannot be exhaustive. That is, even if the test does not find an error, this does not mean that the error can never exist. Also, when an error is detected in a test, the only information available to the developer is the initial configuration of the input and internal memory that led to the error. Therefore, after running the program several times, it is often difficult to understand the underlying reason for the error and why the initial configuration under consideration results in errors elsewhere in the program.

The state-of-the-art method for verifying timing chart specifications is model checking (for example, as disclosed in Non-Patent Document 1 and Reference [2] shown at the end of this specification). Model checking is the definition of a model of a program in the form of an automaton with states and transitions between those states. Model checking then simulates different executions of the program using different paths between states in the automaton. Errors are modeled by certain states that should not be reached. Model checking verifies that those states are unreachable.

Limitations include that model checking is costly and time consuming (CPU time) and may not be exhaustive.

Model checking can consider successive executions of the same program, but the complexity is often exponential, and as a result simulating the execution of a program quickly requires a lot of CPU time. shall be. Therefore, this method cannot be exhaustive for most typical industrial scale PLC programs.

In short, to address the verification of timing chart specifications of PLC programs, testing is a possible method, but not exhaustive, generally inefficient, and does not provide traceability of detected errors. Model checking is slightly more efficient in part because it can consider consecutive executions of the same program and can provide an execution trace when validation fails. However, model checking remains relatively expensive for large industrial programs and remains non-exhaustive.

Although deductive verification provides coverage guarantees, it is not suitable for temporal property verification. In fact, deductive verification requires complete knowledge of the evolution of the program's variables, whereas timing charts require that the evolution of some other program variable is missing, the elapsed time between two state changes. It is poorly specified in that the time is not always known. Moreover, the timing chart includes events of fixed duration (3 seconds in the example of FIG. 1 discussed above) that constitute meta-properties of the program that are not directly accessible to deductive verification.

European Patent No. 3715975

Clarke, Edmund & Grumberg, Orna & Peled, Doron. (2001). Model Checking.

The present invention uses abstract semantic computations to enable deductive verification of timing chart specifications and provide coverage guarantees.

The present invention aims to improve the above situation.

To that end, the present invention proposes a computer-implemented method for checking the correctness of a PLC program (i.e. a program written in any PLC programming language, e.g. one of those defined by the IEC 61131-3 standard). do. More particularly, this PLC program corresponds to a programmable logic controller type computer program described by time function specification data (such as timing chart data as shown above with reference to FIG. 1). This method is
Converting a PLC program into a model (S1);
converting the time function specification data and integrating the converted time function specification data into the model (S2);
calculating abstract semantics to infer information missing in the temporal functional specification data (S3);
performing a predicate transformation (S4) to deduce from the model and predetermined PLC formalization instructions the properties to be verified such that the PLC program satisfies the temporal functional specification data;
elucidating and checking whether the above property is always verified or providing a counterexample (S5);
including.

Implementation of this method subsequently makes it possible to detect the first point in the PLC program when a characteristic is not verified and allow the programmer to make appropriate corrections.

Computation of abstract semantics according to S3 followed by deductive verification in S4 has been found to be particularly effective for PLC programs described by time function specifications such as timing charts. .

In certain embodiments, the method includes, after S5:
Converting the above counterexample into a PLC model error event initial configuration (S6);
assembling at least state variable values and event initial variable values (S8);
converting it back into a PLC program (S9);
may further include.

For example, in S6, the transformation of the above counterexample is
an output value that is not satisfied after a specific event described by the above time function specification data;
at least one variable value that results in a specification violation;
At least one of these can be given.

Finally, this series of steps S1-S9 allows the programmer to clearly know the bugs that may occur as a result of model specification violation scenarios after S9.

For example, in one embodiment, at S9, the conversion back to the PLC program includes intermediate values, including values of inputs, internal memories, and outputs, for each event and for each execution state of the PLC program, up to the last unsatisfied event. Information and model specification violation scenario data can be provided.

Such intermediate values may be, for example, after S6 and before S8 in certain embodiments.
simulating the execution (S7) to obtain intermediate values of the event execution in addition to the initial configuration;
can be earned by carrying out
Thus, in S8, state variable values and event initial variable values as well as further intermediate variable values can be assembled.

For example, intermediate values for event execution can typically be obtained from the initial configuration described above.

Indeed, in S6, the aforementioned counterexample can be transformed into information comprising, for example, an output value that is not satisfied after a certain event of the timing chart (or more generally by the aforementioned time function specification data). These information thereby provide the values of the variables that result in the corresponding specification violation.

These values of variables can describe in more detail the event initial configuration of the PLC program model and correspond to the values of inputs and internal memory at the beginning of the event of the timing chart and up to the last unsatisfied event. Can be done. Once the bug corresponding to such an unsatisfied event is fixed, the method can be started again at S1 until a new last unsatisfied event is encountered. Finally, the method makes it possible to detect violations at any point in the timing chart specification and to check the overall consistency of consecutive points in the timing chart.

Moreover, to implement S7, in S7, the model event execution intermediate value can be calculated from the PLC model error event initial configuration obtained from S6 and the predefined PLC formalization instructions. This therefore makes it possible to simulate the execution of a PLC program and to recalculate intermediate values of internal memory and outputs during event execution, from the event initial configuration given in S6 to the last unsatisfied event.

Furthermore, in S8, from S7 to obtain the complete error scenario that defines the range of values that the aforementioned variables can take during states and event executions, from the start of the PLC program until the last unsatisfied event. The event execution value of and the state variable value range from S3 are assembled.

An example embodiment of the first steps S1-S5 shown above is shown below.

For example, for the implementation of S1, the model obtained from S1 refers to a default model of PLC primitives and can be represented in a first-order logic logical framework.

Generally, at least integer type references and boolean type references can be used to model the inputs, internal memories, and outputs of a PLC program.

Further, the time function specification data input as an argument in S2 can be given in the data format of a timing chart expressed in a PlantUML type language (for example, as described in the cited document [5] shown below). ).

The implementation of S2 can provide specification assertions expressed in a logical framework of predicate logic. Thus, multiple successive copies of the model, possibly incorporated into a loop, can be used to represent the successive states and events given by the timing chart.

At S3, the range of variable values taken during the execution state of the PLC program can be inferred for at least some of these variables not specified in the time function specification data.

In one embodiment, in S4, Dijkstra's weakest precondition calculation method is used to ensure that the PLC program always satisfies the corresponding functional specification if the generated properties are satisfied. can.

In one embodiment, at S5, the automated solver:
Proving the above properties generated in S4, or
finding a counterexample of the above property represented by the input and internal memory values in the model in which the above property is not satisfied;
can be used to do.

The invention is also directed to a computer program comprising instructions for causing a computing device to perform the method described above when the program is executed by the computing device. The invention is also directed to non-transitory computer readable media for storing instruction data of such computer programs.

The invention is also directed to a computing device comprising processing circuitry for carrying out the method described above (an example of such processing circuitry is shown in FIG. 3, described below).

More details and examples of embodiments of the invention will be described below with reference to the accompanying drawings.

It is a figure which shows an example of the timing chart of a PLC program. 1 is a diagram illustrating an example of a sequence of steps of a method according to the invention in a particular embodiment; FIG. 1 schematically depicts an example of a computing device according to the invention in a particular embodiment; FIG.

As indicated above, programmable logic controllers (PLCs) can control assembly lines and electronic robots, among others. It is difficult to debug PLCs, especially regarding functional specifications described as timing charts. Bugs are costly in factory automation systems in terms of downtime and sometimes human and hardware damage. Current techniques for checking the correctness of PLC programs according to timing chart specifications are not exhaustive, time consuming, and generally not efficient in understanding problems when bugs are detected.

In the following, we propose a comprehensive, efficient and automated solution to check the correctness of PLC programs according to timing charts. This solution uses both abstract semantic computations to infer missing information from timing charts and deductive verification to ensure that all bugs are detected. This solution detects violations anywhere in the timing chart specification and checks the overall consistency of consecutive parts of the timing chart. When a violation is detected, this solution can display the scenario to the programmer as an execution sequence from the initial configuration of the timing chart to the defective location. This solution provides an efficient tool that safely reduces deployment time while increasing the reliability of PLC programs in the factory automation industry.

abstract semantic computation (according to step S3 shown below), and deductive verification (according to step S4 below),
The combination shows high efficiency when especially applied to PLC programs described by timing chart specifications.

In fact, deductive verification guarantees exhaustiveness with respect to the property being verified, but if the number of executions between two events is arbitrarily large, it is therefore unknown whether the values that internal memory variables can take during two events are unknown. It is not suitable for time characteristic verification. On the other hand, abstract semantic calculations can give an over-approximation of the values that variables can take during any number of consecutive executions of the program. Abstract semantic computation also guarantees exhaustiveness, but is not as scalable as deductive verification. Therefore, deductive verification cannot operate on a typical industrial scale complete PLC program. The solution proposed here is to infer the variable value information needed to perform a deductive verification that guarantees exhaustiveness and thus also provides verification that is scalable to real-world industrial PLC programs. It uses abstract semantic calculations at specific points in the PLC program.

FIG. 2 shows the overall architecture of a possible implementation of this solution for automated deductive verification of PLC time specifications. This implementation is divided into nine different process steps.

Step S1 relates to automatically converting the PLC program into a model. This process automatically converts a PLC program into a model that references predefined PLC primitives: logic checkers (contacts), actuators (coils), logic circuits, and instructions. This model can be expressed in a first-order logic logical framework.

Integer type references and Boolean type references can be used to model the inputs, internal memory, and outputs of a program. Manifolds can be used to factor out the number of model primitives. In this process, information can be added to the model element, such as code locations to link the model element to the original PLC element, or instructions to instrument tools used later in the process. .

Step S2 relates to converting the timing chart and integrating the timing chart into the program model. The conversion of timing charts into specification assertions in the program model can possibly be done from a given language such as PlantUML (cited document [5]). Those assertions can be expressed in the logical framework of predicate logic.

Several successive copies of the program model, possibly incorporated into loops, can be used to represent the successive states and events given by the timing chart.

Step S3 involves computing abstract semantics to infer necessary information missing in the timing chart. This process uses sound abstract semantic computations, such as abstract interpretation (reference [6]), to infer missing information that is then used for deductive verification. For example, this process applies to loop invariants, especially for internal variables whose values are not specified in the timing chart; The range of values that can be taken can be inferred. Without this evaluation information, deductive verification cannot handle properties that are to be verified after the state.

Step S4 deduces from this model and some predetermined PLC formalization the predicates to be transformed, and more specifically the properties to be verified. This process combines a model transformation of the PLC program and timing chart with a predefined model of the instructions to calculate characteristics that persist more at certain points in the execution sequence of the PLC program to satisfy timing chart verification. This process uses Dijkstra's weakest precondition calculation method [3] to ensure that such calculations minimize the size of the property being computed and are sound (i.e., if the property is satisfied) can ensure that the PLC program always meets the specifications.

Step S5 automatically resolves and checks whether the property is always verified or provides a counterexample. This process uses an automated solver (such as the SMT solver [4]) to formally prove the properties generated in step S4 or to find counterexamples to these properties. In the former case, this process ensures that the PLC program fully satisfies the timing chart specifications for any execution sequence, along with the soundness of the calculations in step S4. In the latter case, this process provides a counterexample of the property, ie, the input and internal memory values in the model for which the property is not satisfied.

Step S6 is to convert the characteristic counterexample into a PLC model error event initial configuration. If step S5 finds a counterexample to the characteristic generated in step S4, this step S6 converts this unsatisfied characteristic into information about which output values are unsatisfied after a particular event in the timing chart. As well as converting the associated counter-examples, the values of the variables that result in this specification violation, i.e. the event initial configuration of the model of the PLC program (i.e. up to the unsatisfied event, the input and internal memory at the start of the event of the timing chart) value of the corresponding model element).

Step S7 is for simulating execution. To that end, model event execution intermediate values are calculated from the PLC model error event initial configuration. This step S7 simulates the execution of the PLC program using another PLC formalization, and stores all internal memory and outputs during the event execution, from the event initial configuration given in step S6 to the unsatisfied events. The intermediate value of can be recalculated.

Step S8 is for assembling state variable values and event execution variable values. This process assembles the event execution values from step S7 and the state variable value ranges from step S3 to obtain the complete error scenario.

This step S8 combines the information from steps S3 and S7 to create a complete specification violation scenario, from the start of the PLC to the unsatisfied event, i.e. the values that variables can take during state and event execution. A range can be given.

Step S9 relates to reverse conversion to a PLC program. This process converts the model intermediate values back into a PLC program with intermediate value information, and can, for example, present a printed version of the results to the user. The process of step S9 finally converts the model specification violation scenario back to the original PLC program having input, internal memory and output values for each event and each state, up to the event where the specification is not satisfied. Can be done. This process can print those values as the original PLC program values decorated with colors representing binary values and labels representing integer values. This error scenario, along with the code location and information added to the model in step S1, gives a very complete overview of the violation found and how to fix this violation.

The invention is also directed to a computing device comprising processing circuitry for performing the method described above with reference to FIG.

Refer now to FIG. Such a processing circuit is
an input interface IN for receiving data of a PLC program, its timing chart and possibly predetermined PLC formatting instructions;
a memory MEM for storing the data of the instructions of the computer program according to the invention and possible temporary and/or non-transitory data necessary to carry out the execution of the computer program;
a processor PROC capable of cooperating with a memory MEM to read and execute instructions of a stored computer program;
an output interface OUT for providing corrected PLC program data and input, internal memory and output values for each event and each state up to the event where the specifications are not met;
can be provided.

(Cited documents)
Document 1: European Patent Publication: EP3715975.
Reference 2: Clarke, Edmund & Grumberg, Orna & Peled, Doron. (2001). Model Checking.
Reference 3: EW Dijkstra. Hierarchical ordering of sequential processes, Acta Informatica, vol. 1, No. 2, 1971, pp 115-138.
Reference 4: C Barrett, R Sebastiani, S Seshia, and C Tinelli, "Satisfiability Modulo Theories." In Handbook of Satisfiability, vol. 185 of Frontiers in Artificial Intelligence and Applications, (A Biere, MJH Heule, H van Maaren, and T Walsh, eds.), IOS Press, Feb. 2009, pp. 825-885.
Reference 5: Drawing UML with PlantUMLPlantUML Language Reference Guide. http://plantuml.com/guide
Reference 6: Cousot, Patrick; Cousot, Radhia (1977). "Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints". Conference Record of the Fourth ACM Symposium on Principles of Programming Languages, Los Angeles , California, USA, January 1977. ACM Press. pp. 238-252.

Claims (16)

A computer-implemented method of checking the correctness of a PLC program, said PLC program corresponding to a programmable logic controller type computer program described by time function specification data, said method comprising:
converting the PLC program into a model (S1);
converting the time function specification data and integrating the converted time function specification data into the model (S2);
calculating abstract semantics to infer information missing in the temporal function specification data (S3);
performing a predicate transformation (S4) to deduce from the model and predetermined PLC formalization instructions characteristics to be verified such that the PLC program satisfies the temporal functional specification data;
elucidating and checking whether the property is always verified or providing a counterexample (S5);
including methods. The method includes, after the S5,
converting the counterexample into a PLC model error event initial configuration (S6);
assembling at least state variable values and event initial variable values (S8);
converting it back into a PLC program (S9);
2. The method of claim 1, further comprising: In S6, the transformation of the counterexample is
an output value that is not satisfied after a specific event described by the time function specification data;
at least one variable value that results in a specification violation;
3. The method of claim 2, wherein at least one of the following is provided. The method includes, after the S6 and before the S8,
simulating the execution (S7) to obtain intermediate values of the event execution in addition to the initial configuration;
further including;
4. The method according to claim 2 or 3, wherein in said S8 state variable values and event initial variable values as well as further intermediate variable values are assembled. In said S7, a model event execution intermediate value is calculated from said PLC model error event initial configuration obtained from said S6 and said default PLC formatting instruction to simulate the execution of said PLC program, and said S6 5. The method of claim 4, wherein intermediate values of internal memory and output during event execution are recalculated from the event initial configuration given in to the last unsatisfied event. In said S8, from the start of said PLC program until the last unsatisfied event, a complete error scenario is defined that defines the range of values that said state variable values and said event initial variable values can take during state and event execution. 6. A method according to claim 4 or 5, comprising assembling the event execution value from the S7 and the state variable value range from the S3 to obtain. In S9, the reverse conversion to the PLC program includes intermediate value information including input, internal memory, and output values of each event and state of the execution of the PLC program until the last unsatisfied event, and model specification violation scenarios. The method according to any one of claims 2 to 6, wherein the method is provided together with the data. The method according to any one of claims 1 to 7, wherein the model obtained in S1 refers to a predefined model of PLC primitives and is represented in a logical framework of first-order logic. 9. The method of claim 8, wherein at least integer type references and Boolean type references are used to model inputs, internal memories and outputs of the PLC program. The method according to any one of claims 1 to 9, wherein the time function specification data input as an argument in S2 is given as a timing chart expressed in a PlantUML type language. The implementation of S2 provides specification assertions expressed in a logical framework of predicate logic, such that multiple successive copies of the model incorporated into a loop represent successive states and events given by the timing chart. 11. The method according to claim 10, wherein the method is used. Any one of claims 1 to 11, wherein in S3, the range of variable values taken during the execution state of the PLC program is inferred for at least some of the variables not specified in the time function specification data. The method described in section. Any one of claims 1 to 12, wherein in said S4, Dijkstra's weakest precondition calculation method is used so that said PLC program always satisfies a corresponding functional specification when a characteristic is satisfied. The method described in section. In S5, the automated solver
proving the property generated in S4; or
finding counterexamples of said property represented by inputs and internal memory values in said model for which said property is not satisfied;
14. The method according to any one of claims 1 to 13, wherein the method is used for carrying out. A computer program comprising instructions which, when executed by a computing device, cause the computing device to perform a method according to any one of claims 1 to 14. A computing device comprising a processing circuit for performing the method according to any one of claims 1 to 14.