# Verification of Control System Runtime Using an Executable Semantic Model +
## 3 Runtime Formal Model
### Memory and Stack Operations  
One of the helper functions handling data and code memories is the memory read function. The task is to retrieve data from the given address and sometimes from subsequent addresses, forming a value of the specified size. The models of these functions are presented using Formula (7). The function \(Get1 BMem\) retrieves a single byte from the specified address. The function \(Get2 BMem\) retrieves two data bytes, one from the given address and the other from an address incremented by one, and then combines them into a \(TwoBytes\) value. The functions \(Get4 BMem\) and \(Get8 BMem\) retrieve 4 and 8 bytes, respectively, combining them into \(FourBytes\) and \(EightBytes\) values. The function \(GetAddress\) retrieves the value stored at the specified \(Address\) in \(Memory\), where \(Memory\) itself is represented by another \(Address\). Since the virtual machine lacks an accumulator and directly operates on addresses, the function \(GetAddress\) plays a crucial role in the model:  
\[Get1 BMem =(Address\times Memory)\rightarrow\mathit{Byte} \tag{7}\] \[Get2 BMem =(Address\times Memory)\rightarrow\mathit{TwoBytes}\] \[Get4 BMem =(Address\times Memory)\rightarrow\mathit{FourBytes}\] \[Get8 BMem =(Address\times Memory)\rightarrow\mathit{EightBytes}\] \[GetAddress =(Address\times Memory)\rightarrow\mathit{Address}\]  
The task of the memory update functions is to change the contents of memory at a given address with the provided value. As a result, a new memory is returned, which is a copy of the old one with the introduced change. These functions come in several variants, similar to the read functions. They respectively modify one, two, four, or eight bytes in memory. The variants of the update functions have been defined using Formula (8). Additionally, the function \(MemMove\) moves a portion of memory from the source \(Address\) to the target \(Address\). The size of the portion is specified as \(OneByte\) (0 to 255):  
\[Upd1 BMem =(Address\times Memory\times OneByte)\rightarrow\mathit{Memory} \tag{8}\] \[Upd2 BMem =(Address\times Memory\times TwoBytes)\rightarrow\mathit{Memory}\] \[Upd4 BMem =(Address\times Memory\times FourBytes)\rightarrow\mathit{Memory}\] \[Upd8 BMem =(Address\times Memory\times EightBytes)\rightarrow\mathit{Memory}\] \[MemMove =(Address\times Memory\times Address\times Memory\times OneByte) \rightarrow\mathit{Memory}\]  
The helper functions \(Push\) and \(Pop\), whose models are presented using Formula (9), perform operations on the code stack and data stack. The \(Push\) function pushes the given address onto the stack, returning a new stack, while the \(Pop\) function returns the last pushed address on the stack along with the new stack without the retrieved value. They are used during the invocation of user functions, functional blocks, and programs:  
\[Push =(Stack\times Address)\rightarrow\mathit{Stack} \tag{9}\] \[Pop =Stack\rightarrow(Address\times Stack)\]  
To manage the \(ProtStack\) for exception handling, the following functions are introduced: \(PushProt\), \(PopProt\), and \(PeekProt\). \(PushProt\) adds an item to the stack, \(PopProt\)removes an item from the stack, and \(PeeRProt\) returns a copy of the topmost item without altering the stack:  
\[\begin{split} PushProt&=(ProtStack\times ProtEntry) \to ProtStack\\ PopProt&=ProtStack\rightarrow(ProtEntry\times ProtStack)\\ PeeRProt&=ProtStack\to ProtEntry\\ \end{split} \tag{10}\]  
The last group of helper functions comprises the processor flag control functions. The \(SetFlag\) function sets the status bits, while the \(ClearFlag\) clears the status bits. The flags are used for signaling cold start, invalid instruction, or array out-of-bounds conditions. The models of these functions are presented using Formula (11). The successive \(TwoBytes\) denote the actual value of \(Flags\), bits to be set or reset, and new \(Flags\):  
\[\begin{split} SetFlag&=(TwoBytes\times TwoBytes) \to TwoBytes\\ ClearFlag&=(TwoBytes\times TwoBytes) \to TwoBytes\\ \end{split} \tag{11}\]