# Verification of Control System Runtime Using an Executable Semantic Model +
## 4 Denotations of Instructions
### Machine Instructions
These retrieved values are then compared with the model pattern, and any disparities prompt a message to the user to rectify the implementation. ### Tools

The runtime checking methodology utilizing the F\({}^{\sharp}\) executable model seamlessly integrates with the CPDev IDE, designed around the.NET framework. By augmenting the programming environment with the reference runtime, developers can execute a control program on the target device (controller) using the implementation in question alongside the model. Before executing each program cycle, the controller may receive data of the external signals via its inputs, such as sensors. These acquired values are then transferred to the CPDev IDE using online communication capabilities such as Modbus or TCP, and provided to the model, effectively stored in the data memory. This ensures that both the model and the runtime operate on the same input data, leading to consistent results. Figure 3 illustrates a test session in the CPDev environment, verifying the implementation of the ADD and DIV functions for REAL variables. The simple test program is prepared in the FBD language, utilizing four global variables I, J, K, and L of type REAL. Additionally, local variables OUT1 and OUT2, and a constant 10.0 are introduced. In the lower part, a portion of the virtual machine code is displayed in binary format (on the left) and textual format (assembler notation). The program is executed cycle by cycle on the target device. The verification of the virtual machine state against the model is performed after each cycle with the results reported at the bottom. As illustrated in Figure 3, the verification passed successfully for all program cycles. In case of any disparities between the outcomes of the model and the runtime, an alert would be raised to the user, providing specific details for error correction. The debugging capabilities of the CPDev environment facilitate checking results not only after the completion of all operations in the program cycle but also within the cycle itself. In this scenario, the device operation is paused after each instruction performed by

Figure 3: Verifying the ADD and DIV implementation in the CPDev environment. the virtual machine, allowing for an immediate comparison between the state of the model and the implemented runtime. This approach helps detect erroneous implementations of the last executed instruction promptly. For example, the presented methodology identified issues in one of the runtime implementations, such as a missing exception raise in the DIV instruction and an extra byte being modified by the CEAC instruction, apart from the intended array element. ## 7 Final Remarks

The denotational equations forming the semantic model of the runtime appear to be a favorable choice, despite being primarily used for programming languages. As demonstrated, these equations can be naturally translated into executable F\({}^{\sharp}\) code. This format enables the examination of whether the virtual machine implementation will execute the portable control program code consistently across different target platforms, regardless of the implementation techniques. The presented methodology holds promise for industrial applications, providing an automated method for verifying the correctness of the runtime, which may be particularly interesting in the field of distributed control systems consisting of heterogeneous hardware platforms. Consequently, it facilitates the development of predictable, consistent, and error-free control devices. Conceptualization, J.S. ; methodology, J.S. and B.T. ; software, J.S. and B.T. ; validation, J.S. ; formal analysis, J.S. ; investigation, B.T. ; resources, J.S. and B.T. ; data curation, J.S. and B.T. ; writing--original draft preparation, B.T. ; writing--review and editing, B.T. and J.S. ; visualization, B.T. ; supervision, B.T. All authors have read and agreed to the published version of the manuscript. This research received no external funding. The authors declare no conflicts of interest.