# Verification of Control System Runtime Using an Executable Semantic Model +
## 2 Operation of the Runtime  
Usually, programmers who work with IEC 61131-3 focus on software projects intended for deployment on various controllers. In this context, it is assumed that such a project is executed by a runtime component referred to as an execution unit. A project consists of one or more tasks composed of Program Organization Units (POUs), such as program or function blocks. Consequently, a smaller device typically provides a single execution unit capable of running one project, while a controller with more powerful hardware can accommodate multiple execution units, allowing many projects to run simultaneously as shown in Figure 1a. In this context, an execution unit maintains an instance of the virtual machine, which establishes an isolated environment for executing control programs stored as binary intermediate code, shown as eXecutable Control Program (XCP). In such a solution, a control project is compiled into the binary format and subsequently transferred to the execution unit, where it is executed through the virtual machine. The execution units also interface with platform resources for the virtual machine. An example of leveraging dual-core CPUs for creating a controller with two execution units is outlined in [20]. The virtual machine discussed here has been specifically designed to comply with the IEC 61131-3 standard [14]. It is a part of the Control Program Developer (CPDev) programming environment, which facilitates the development of control software for diverse platforms, such as ARM, FPGA, and others [21]. A programmer uses CPDev IDE to prepare POUs using textual languages such as ST or IL, and graphical ones such as FBD, LD and SFC. Then, the compiler generates the intermediate binary code for the virtual machine [21]. The architecture of the CPDev virtual machine is depicted in Figure 1b. The program code is stored in the code memory, from where individual instructions for the virtual machine and their operands are retrieved based on the indications of the CodeReg register (also known as the program counter). In the Instruction Processing module, the instruction is decoded and executed. In the case of reading and writing variables, the data memory is  
Figure 1: Architecture of the runtime. (**a**) Project execution units. (**b**) Elements of the virtual machine. used. The DataReg register indicates the base address of the Program Organizational Unit (POU) for which the operation is performed. This enables working with multiple instances of POUs, such as function blocks or programs. Two stacks are used for entering and exiting subprograms: the data stack and the code stack. The data stack stores pointers to recently used database addresses (i.e., DataReg contents), while the code stack keeps track of return addresses (for CodeReg). Upon entering a subprogram, the current values of CodeReg and DataReg are pushed onto the code stack and data stack, respectively. Upon return, the contents of these registers are popped from the stacks. This stack mechanism facilitates nested function blocks. The virtual machine does not have a special register for storing operation results like an accumulator. Therefore, executing instructions typically involves fetching operands from memory, i.e., data memory for variables and code memory for constants, and storing the result in data memory. The machine incorporates the Flags register, containing status flags signaling errors or unusual situations like an array index beyond the valid range, an unknown instruction code, or a cold start. The instruction block for the virtual machine comprises three parts as illustrated in Figure 2. Each machine instruction is identified by the vmcode, which consists of two components: the group identifier ig, and the specific instruction type it. This design facilitates the selection of type-specific instructions from a set of similar ones aimed at a specific functionality. Furthermore, for certain instructions that accept a variable number of operands, the it component indicates the number of operands.