# Verification of Control System Runtime Using an Executable Semantic Model +
## 1 Introduction  
The predictable and reliable operation of control systems is an essential requirement in industrial practice. Programmable automation controllers (PACs) and programmable logic controllers (PLCs) provide flexibility in constructing control programs, which can lead to significant negative consequences if they are improperly prepared. To avoid this, various approaches exist. Some of them, which can be classified as software engineering, emphasize the proper execution of the software development process, reducing the likelihood of errors by the programmer [1]. In the case of control systems, this can also be achieved by using specially designed programming languages tailored for such applications. A typical example is the set of languages ST, FBD, LD, IL, and SFC, which are part of the industrial standard IEC 61131-3 [2]. It also defines the appropriate architecture for control software. Other concepts focus on preparing suitable testing procedures for such applications, aimed at detecting errors in control software before it is deployed in industrial conditions [3]. One solution considered in this work is the development of a specialized runtime environment designed to prevent the propagation of errors made by the programmer to the entire system. The occurrence of a critical runtime error in the program should be detected and prohibited. Such an isolated environment is often called a sandbox and can be implemented using hardware security mechanisms, such as memory protection [4]. However, these solutions require hardware expansion with additional circuits or the use of advanced processors with such capabilities [5]. In embedded systems, which may involve various hardware platforms, such extension is often unavailable and impractical. Hence, there is a need for software solutions that allow the isolation of the program execution environment from the rest of the system. One option involves the supervised execution of the program by a software interpreter instead of directly by the hardware processor. The interpreter fetches individual instructionsfrom the program, translates them into processor code, and executes them. During these activities, the interpreter can check whether the execution of instructions will cause errors and react accordingly if it does. The prerequisite is to include a programming language interpreter library in the controller's firmware, allowing the textual source code to be interpreted and executed [6]. This solution may be disadvantageous in control systems due to the additional memory and time required for analyzing the textual code by the appropriate parser and preparing native code for the target processor. Another option is to prepare a language and tools for the automatic and semi-automatic model analysis of software [7]. However, this approach can be time-consuming and error-prone due to the necessity of developing an additional compiler and an environment for theorem proving. The solution considered in this article, although based on the concept of an interpreter, does not use textual code but binary code containing encoded instructions along with operands. Therefore, lexical analysis using a parser is not needed at the controller side. Instructions in binary code are defined for a virtual processor with specified characteristics. However, their implementation by the hardware processor is still necessary; hence, the binary code is called intermediate or portable code. In return, we achieve platform independence because the interpreter can translate the instructions of the virtual processor into specific instructions of a real processor, provided that support for the latter is included in the process. In distributed control systems where multiple control devices with varying hardware platforms are interconnected via a network, the software portability enabled by the intermediate code proves particularly advantageous. To execute the intermediate code, the interpreter uses specially allocated code and data memory areas as well as stacks defined programmatically.