Corresponding author: Mikhail A. Belonosov (mbelonosov@vniia.ru)

Academic editor: Georgy Tikhomirov

The article describes an automated verification method used for application software of control safety systems based on the TPTS-SB equipment. Verification is performed by comparing two mathematical models (oriented graphs): one obtained by processing the original design data, i.e., graphical functional diagrams, and the other formed by reversing the program code loaded from the controller. The vertices in both graphs are functional blocks of mathematical and logical operations; the edges are connections between them. The constructed mathematical models undergo a comparison, covering the vertices and edges of the graphs as well as the memory cells and values of constants. The equivalence of mathematical models proves the correspondence between the program code and the initial set of design functional diagrams.

The proposed automated verification method makes it possible to prove that no distortion is introduced into the program during the process of converting graphical functional diagrams into the program code with its subsequent translation and loading into the controller. It is postulated that any distortions will be detected during the verification procedure, which is performed every time after loading the code into the controller.

The solution provides an acceptable speed when large volumes of vector graphics stored in a relational database are processed, and makes it possible to visualize the verification results. The proposed method is implemented in the GET-R1 instrumentation tools for TPTS-SB and is used in designing and verifying the application software of the safety systems at the Belarusian NPP.

Specialists of the FSUE VNIIA have developed a technological software/hardware complex (TPTS-SB) for digi1tal control safety systems (CSS) of NPP instrumentation and control (I&C) systems. These systems are assigned the most important task of ensuring nuclear safety at power units during beyond-design-basis accidents; therefore, they are subject to the most stringent requirements for software diversity, reliability and correctness. The TPTS-SB software/hardware products were developed to meet all modern requirements for such systems.

The application programs of TPTS-SB-based control safety systems are created as graphical functional diagrams by means of the GET-R1 tool environment (

The article describes a standard procedure for verification of an application program after it is loaded into the controller, including reading from the controller and reverse engineering from the byte-code into a graphical representation of the algorithm.

It is postulated that, in the process of converting graphical algorithms into the program code, translating and loading the code into the controller, there are no hidden distortions in the program: any distortion will be detected by means of the proposed verification procedure.

TPTS-SB is a software/hardware system with built-in hardware/software variety designed to build NPP digital control safety systems. The built-in variety is achieved due to division by two independent different implementations: Diversities A and B, which duplicate each other, are functionally equivalent, but differ in hardware and software. The arrangement and architecture of TPTS-SB-based software/hardware systems are described in detail in (

Fig.

Logical processing in Diversities A/B is performed by programmable automation processor modules (APM). These controller modules read cyclically the data from input modules, execute a user program using a special interpreter, and supply signals to output modules and priority control modules.

Integrated TPTS-SB-based CSS: EP – emergency protection; MCR – main control room; BCP – backup control panel; ULCS – upper level control system; CSS – control safety system; EPA – emergency protection automatics; IM – interface module; CM – communication module.

To program the APMs, the STEP-S programming language is used, which includes logical and arithmetic instructions as well as complex technological ones, such as integration, signal limiting, voting, etc. A program written in the STEP-S programming language is a strictly linear sequence of instructions that does not contain cycles and transitions. Each instruction contains a strictly defined set of arguments and presents an operator of the form

CMD opd1 ... opdN … value1 … valueN

where CMD is the alphanumeric sequence indicating the instruction; opd (operand or marker) is the symbolic address of the APM memory cell; value is the numeric or symbolic constant.

To be loaded to the APM, a STEP-S program is translated into a binary representation (byte-code) while the program structure remains unchanged.

STEP-S programs are the result of processing a large number of control algorithms that are developed graphically in the language of functional diagrams (

As an example, Fig.

Fragment of the STEP-S application program.

No. | STEP-S instruction |
---|---|

1 | NOT M,133 M,141 |

2 | 2/4-FS ET,4,9 ET,2,10 ET,5,11 M,140 M,145 M,146 |

3 | NOT M,133 M,142 |

4 | AND-3 M,150 M,141 M,135 M,152 |

5 | 2/4-FS2 M,138 ET,4,9 ET,2,10 ET,5,11 M,153 M,154 |

6 | NOT M,135 M,143 |

7 | AND-3 M,133 M,153 M,143 M,155 |

8 | 2/4 M,138 ET,4,9 ET,2,10 ET,5,11 M,147 |

9 | B-DFLT M,147 M,148 M,149 1 1 |

10 | NOT M,135 M,144 |

11 | AND-3 M,142 M,156 M,144 M,158 |

12 | B-LADK M,143 0 |

13 | 2/4-FS M,138 ET,4,9 ET,2,10 ET,5,11 M,156 M,157 |

14 | OR-4 M,158 M,155 M,152 M,146 M,159 |

15 | B-DFLT M,147 M,150 M,151 1 1 |

Functional diagram of processing signals from seismic sensors.

Each functional block shown in the diagram is converted into a sequence of one or more instructions. The code is generated in four stages.

APM memory cells (markers) necessary for calculations and storing the results are estimated and assigned.

The order of calculations is determined. The place where the instructions corresponding to a specific functional block enter the resulting program is determined by this block sequence number which is automatically calculated by topological sorting of an acyclic oriented graph – a mathematical model corresponding to the APM functional diagrams (

The design data integrity and correctness as well as compliance with the formal design rules for the TPTS-SB platform are automatically checked. In case of errors, generation is terminated.

The sequence of functional blocks is processed as determined at Stage 2. Template instructions corresponding to each functional block are inserted into the resulting program, and previously calculated memory cells and values are entered.

Mathematical model graph corresponding to the functional diagram in Fig.

All the generation stages are performed automatically. The resulting program undergoes the translation stage, and then is loaded into the APM of TPTS-SB in the form of byte-code.

When designing NPP control safety systems, it is necessary to prove the correctness of all stages of code generation, translation and loading as well as the absence of distortions in the resulting program as compared to the graphics algorithm. To do this directly is extremely difficult for the following reasons:

rigorous proof of the correctness of all programs operating at different code generation stages is a labor-intensive process;

there is no guarantee that the generation process will not fail, which will affect the data integrity. A failure can also be caused by external factors, such as data transmission errors, and internal factors, such as hidden program errors, data read/write errors, etc.

Therefore, the only acceptable way to prove the correctness of the program is to develop a procedure for reverse engineering of the generated and loaded program into a graphical or tabular representation and to compare the restored data with the original project. At the same time, a graphical representation is a general functional diagram, which includes all functional blocks from which the APM program is generated and connections between them; a tabular representation is a list of all functional blocks and their parameters in a tabulated form. However, this proof is also associated with certain difficulties. The program generated in the STEP-S language does not have the following data:

information on whether the STEP-S instructions belong to a specific control algorithm;

graphic information necessary for dividing the graphics into diagrams and determining the coordinates of functional blocks;

designations of algorithms, inscriptions and decoding necessary for users to understand the algorithm;

information about the graphic implementation of functional blocks (several icons can correspond to the same functional unit).

Therefore, it is impossible to completely restore the original graphical representation of the control algorithms using the program code without involving the project information.

However, to prove the correctness of the code generation and loading procedures, it is not required to completely restore the graphics. Moreover, with large project volumes, these procedures will take an unreasonably long time. Instead of full restoration, it is proposed to construct mathematical models of the project in the form of graphs oriented to different source data: one graph is constructed according to the project; the other is constructed according to the program code. The vertices in both graphs are functional blocks of mathematical and logical operations, while the edges are connections between them. The constructed mathematical models undergo a comparison, covering the vertices and edges of the graphs as well as the memory cells and values of constants. The equivalence of mathematical models is the proof of the correspondence between the program code and the initial set of project functional diagrams. Fig.

The reverse engineering procedure is implemented independently of the code loading, translation, and generation programs. Restoration is performed in six stages.

The byte-code is read from the APM and back-translated into a string representation in the STEP-S language.

A list of STEP-S instructions is created for the functional blocks from the library and this list is sorted by the number of instructions in each block.

A search is carried out for template sequences of the functional blocks in the program code and the program is split into corresponding fragments. Each fragment of the STEP-S instructions is replaced by the corresponding functional block.

The memory cells (markers) and constants from the code are inserted into the inputs and outputs of the functional blocks.

The connections between the functional blocks are determined by the correspondence of the memory cells (if the same marker is assigned to the input of one block and the output of the other, then these input and output are connected). At the end of this stage, there is already a full-fledged oriented graph constructed by the program code.

An identical oriented graph is constructed (

The result of the comparison of these two oriented graphs can be visualized in a tabular form or in the form of a general functional diagram, which includes all the APM algorithms. When the comparison results are visualized in the form of a general functional diagram, it is considered that different graphical representations of the same function, for example, the vertical and horizontal image of the AND2 function (conjunction of two boolean values), are invariant with each other. Therefore, in comparison, it is reasonable to use a graphical version of the blocks, which is the most suitable from a visual point of view. The functional diagrams generated by the code and the project of the same versions will be identical.

There is a known procedure for verifying the code generator of the SPACE tools (

The solution applied to TELEPERM XS does not verify the code translation and loading stages where errors may occur. Verification of the generated C code proves only the correctness of the generation process, but cannot serve as proof of the identity of the project and the compiled program loaded into the controller.

The solution proposed for the TPTS-SB equipment is more complete, since the entire processing chain is verified (including generation, translation, and loading). In this case, the project mathematical model is restored completely independently without any project information involved. In addition, the use of graph models makes it possible to clearly visualize the comparison results using the hierarchical embedding algorithm of graphs (

The authors propose a method for complete verification of controller programs through reverse engineering. The method can be used for verifying application programs of any controller programmed by means of graphical languages of the IEC 61131-3 standard.

The GET-R1 tools for TPTS include a software component that implements this method. Within these tools, the proposed verification method is used in developing the application software for the TPTS-SB-based control safety systems of the Belarusian NPP-2.

To completely guarantee the code correctness, the TPTS-SB equipment allows for the code loading with a delayed start, which makes it possible to first load the program, then perform the reverse conversion procedure and only after that start a new program.

The main design solutions for I&C systems of modern Russian NPPs are presented in (

✩ Russian text published: Izvestiya vuzov. Yadernaya Energetika (ISSN 0204-3327), 2018, n. 2, pp. 146–156.