# Verification of Control System Runtime Using an Executable Semantic Model +
## 1 Introduction
This creates a Harvard architecture, and the entire runtime environment will be referred to as a virtual machine [8; 9] (meaning an application virtual machine, not related to hardware virtualization). Virtual machines have become prominent in IT due to platforms like the Java Runtime Environment [10] and the.NET Framework [11]. However, the architecture of the virtual machine (VM) presented here is specifically tailored for the hardware architecture of control devices and adapted for embedded systems with limited resources and performance. The implementation must take into account the programming language available for the platform and hardware features such as the type of central processing unit, access to RAM and ROM (flash) memories, clock for time measurement, random number generation, etc. Thus, these implementations vary from platform to platform [12; 13]. A high degree of universality is achieved by implementing a large part of the virtual machine in C/C++ languages available for numerous hardware platforms and processors [14]. Another solution, emphasizing performance, is to implement it in the languages for FPGA circuits [15; 16; 17]. The correctness of such an implementation must correspond to the specification of the virtual machine. So far, this has been verified using tests. This article presents a different solution based on a formal model of the virtual machine, which takes the form of denotational semantics equations encompassing the architecture, intermediate code processing, and individual instructions. Denotational equations are then written in the form of appropriate constructions of the \(\mathrm{F}^{\sharp}\) functional language, creating a direct representation of the denotational model in programmatic form. Such a form of the model is executable, leading to the possibility of verifying the implementation of the machine for a specific hardware platform. Specifically, the implemented runtime and model with the same input data (intermediate code) are executed side by side. During this execution, the verification mechanism compares the state of the model and the virtual machine, particularly the contents of memory, registers, and stacks. In the event of discrepancies, an error in the machine implementation is reported. This allows for the preparation of the machine in a form that precisely matches the specification. Since the machine supervises program execution, runtime errors are detected and signaled, and the runtime does not propagate their effects to other parts of the system. However, the programmability of control devices means that during execution, instructions with critical errors may occur, such as writing to a forbidden memory address or accessingan array with an illegal index. In such cases, the control system becomes inoperative and should transition to a safe state to prevent negative consequences for the controlled object. This type of behavior can be defined by the programmer as a response to runtime errors. Programming environments (e.g., Java, C5[11; 18]) provide a mechanism for handling exceptions, which allows to implement specific behavior in response to an error during the program execution. The previous conference paper [19] introduces a formal model of the exception mechanism tailored for an IEC 61131-3 oriented virtual machine, accompanied by a sample implementation. This paper extends the model into an executable form to conduct model-based checks on the virtual machine implementation. The expansion, coupled with the runtime exception handling, offers a chance to develop automation systems that are more robust and dependable.