# Verification of Control System Runtime Using an Executable Semantic Model +
## 4 Denotations of Instructions
### Machine Instructions
```
letDIV(state:State,getBytes:(Address*Storage)->'a,updBytes:(Address*Storage*'a)->Storage,typeOf:'a->ValueType,fromType:ValueType-> 'a)= let(cm,dm,cs,ds,cr,dr,ex,flg)=state...//gettingvaluesofraddr,dividend,divisor matchdivisorwith |SINT0y|INT0s|DINT0|LINTOL|BYTEOuy|WORDOus|DWORDOu|LWORDOUL|REAL0.0f|LEAL0.0-> let(ps,eo)=ex leteol=(cr3,DIV_BY_ZERO_EXC) letexl=(ps,eo1) letdvflg=SetFlag(flg,DIV_BY_ZERO_FLG) RAISE(cm,dm,cs,ds,cr3,dr,exl,dvflg) |SINT_|INT_|DINT_|LINT_|BYTE_|WORD_|DWORD_|LWORD_|REAL_|LREAL_|letvalue=matchdividend,divisorwith |SINTa,SINTb->SINT(a/b) |INTa,INTb->INT(a/b) |DINTa,DINTb->DINT(a/b) |LINTa,LINTb->LINT(a/b) |BYTEa,BYTEb->BYTE(a/b) |WORDa,WORDb->WORD(a/b) |DWORDa,DWORDb->DWORD(a/b) |LWORDa,LAWORDb->LWORD(a/b) |REALa,REALb->REAL(a/b) |LREALa,LAREALb->LREAL(a/b) |_->failwith\"Wrongdata\" printfn\"Operand1:%AOperand2:%A\
DIVresult:%A\" dividend divisorvalue letmodBytes=updBytes(raddr,dm,fromType(value)) (cm,modBytes,cs,ds,cr3,dr,ex,flg) |_->failwith\"Wrongdata\"
```
The CEAC instruction from Listing 8, which verifies the correctness of an index value in an array, also utilizes exceptions. If the provided idxval falls between lobaseval and hilevelval, the flag register remains unchanged. However, if the index is out of bounds, the exception object signals OUT_OF_BOUNDS_EXC using the RAISE function. Additionally, the OUT_OF_BOUNDS_FLG flag is set. ```
letCEAC(state:State):State= let(cm,dm,cs,ds,cr,dr,ex,flg)=state.... //gettingvaluesoftidxval,lobaseval,hilevelval lettmp=matchidxval,lobasevalwith |INTa,INTb->INT(a-b) |_->failwith\"Wrongata\" letum=Upd2 BMem(idxaddr,dm,FromInt(tmp)) letnewflag=matchtmp,hilevelvalwith |INTa,INTb-> if(a>=Os&&a<=b) thenflg else let(ps,eo)=ex leteo1=(cr3,OUT_OF_BOUNDS_EXC) letex1=(ps,eo1) letbadIdxFlg=SetFlag(flg,OUT_OF_BOUNDS_FLG) RAISE(cm,dm,cs,ds,cr3,dr,ex1,badIdxFlg) |_->failwith\"Wrongata\" (cm,um,cs,ds,cr3,dr,ex,newflag)
```

Listing 8: Array index checking with CEAC in F\({}^{\sharp}\). ## 6 Checking the Implementation against the Model

### Procedure

Implementing the CPDev virtual machine for diverse target platforms involves various programming techniques, depending on platform specifics, available languages, and tools. The CPDev virtual machine has been ported to ARM, x86, RISC-V, and various other microprocessors and microcontrollers, with an FPGA-based machine also developed. Additionally, several applications for control devices have been created [14]. Typically, the runtime for a device is developed by industrial users based on the provided VM specification. Previously, each implementation required a manual series of tests to ensure compliance with the specification. These tests encompassed several dozen programs utilizing the full set of runtime features. Each change in the runtime necessitated the repetition of these tests. However, with the executable model in F\({}^{\sharp}\), automated verification becomes feasible, streamlining the process and reducing the manual effort required. To verify the accuracy of the machine implementation on a particular platform, a series of control projects utilizing the VM functions and procedures are employed. These projects are compiled into intermediate binary code, which is utilized by both the executable model and the implemented runtime. The process involves the following steps:

* Creating a control project using IEC 61131-3 languages like ST, FBD, LD, or SFC within the CPDev environment. * Compiling the program into the intermediate binary code for the virtual machine (XCP file, see Section 2). * Running the program on the target platform and by the F\({}^{\sharp}\) model side by side. * Comparing the state of the virtual machine on the platform with the state of the model. The comparison occurs after the predefined cycle time of control devices, typical for PLCs. At this point, data memory, stack contents, and registers are retrieved from the device using a communication protocol.