# Verification of Control System Runtime Using an Executable Semantic Model +
## 3 Runtime Formal Model
### Semantic Domains  
The semantic domains represent abstract data types, modeling values used by the virtual machine. These domains arise from the architecture of the virtual machine and are expressed using formulas. The following domains related to memory are defined in (1):  
* _Address_: depends on the implementation, but here, 4 bytes are assumed (32-bit).
* _Memory_: a function that, for a given address, returns a byte value.
* _CodeMemory_: represents the _Memory_ (alias) with the program code.
* _DataMemory_: represents the _Memory_ with variable values. \[\begin{split} Address&=Four\_Bytes\\ Memory&=Address\to OneByte\\ CodeMemory&=Memory\\ DataMemory&=Memory\\ \end{split}\] (1) The stacks of the virtual machine are defined in Formula (2). They are as follows:
* _Stack_: represents the stack using a Kleene closure (i.e., a sequence indicated by \({}^{*}\)). It is handled using helper functions Push and Pop, which will be discussed in Section 3.4.
* _CodeStack_: represents the _Stack_ of return addresses (subroutines).
* _DataStack_: represents the _Stack_ of database addresses. \[\begin{split} Stack&=Address^{*}\\ CodeStack&=Stack\\ DataStack&=Stack\\ \end{split}\] (2) The following registers are defined in the model (3):
* _CodeReg_: the _Address_ of the current instruction in the _CodeMemory_.
* _DataReg_: the base _Address_ for operations in the _DataMemory_.
* _Flags_: each bit of this 16-bit value signals errors or unusual situations (array index exceeded, cold start, time overrun, etc.). \[\begin{split} CodeReg&=Address\\ DataReg&=Address\\ Flags&=TwoBytes\\ \end{split}\] (3) The exception-handling mechanism involves nested protected code portions with one or more catch blocks. The stack \(ProtStack\) used for this purpose is represented as a Kleene closure of \(ProtEntry\) tuples, each consisting of four addresses. _ExcObj_ is an _Address_ indicating where the exception object has been stored. Consequently, the exception state \(ExcState\) is represented by the \(ProtStack\) and \(ExcObj\): \[\begin{split} ProtEntry&=Address\times Address \times Address\\ ProtStack&=ProtEntry^{*}\\ ExCObj&=Address\\ ExState&=ProtStack\times ExcObj\\ \end{split}\] (4) In a broad sense, the objective of executing a program is to transform the current state of the machine into a new one. The state is depicted as a combination of various aspects such as memory, stacks, registers, and flags. With the specific domains outlined in the model, the state of the virtual machine is encapsulated within the _State_ domain as defined by Formula (5): \[\begin{split} State=&CodeMemory\times DataMemory \times CodeStack\times DataStack\times\\ &\times CodeReg\times DataReg\times ExcState\times Flags\\ \end{split}\] (5)As seen, the \(State\) domain is formed through the amalgamation of code memory, data memory, code stack, data stack, code register, data register, and processor flags. These components collectively influence the outcome during the execution of each instruction, stemming from the underlying architecture of the machine and its instruction processing methodology. They can be succinctly represented by a set of tuples:  
\[(cm,dm,cs,ds,cr,dr,ex,flg) \tag{6}\]  
where each tuple element corresponds to a value within its respective domain.