## 3 Formal Passive Testing Approach
### Semantics and Algorithm  
The semantics used in our work is related to the traditional Apt-Van Emden-Kowalsky semantics for logic programs [32], from which an extended version has been provided in order to deal with messages and trace temporal quantifiers. **Definition 6**. : _A substitution \(\theta\) is a finite set of bindings \(\theta=\{x_{1}/term_{1},...,x_{k}/term_{k}\}\), where each \(term_{i}\) is a term and \(x_{i}\) is a variable, such that \(x_{i}\
eq term_{i}\) and \(x_{i}\
eq x_{j}\) if \(i\
eq j\)._  
Given a formula \(\phi\) defined by using a set of clauses \(K\) as we mentioned above, a satisfaction result '\(\top\)' ('pass'), '\(\bot\)' ('fail') or '?' ('inconclusive') will be given for a particular trace \(\rho\). Using substitution \(\theta\), we recursively evaluate the formula \(\phi\) (_i.e._, protocol property) on the real protocol execution trace \(\rho\), coupled with a modification of SLD (selective linear definite-clause) resolution algorithm [33] for the evaluation of Horn clauses. The evaluation process is described as follows:  
\[eval(A_{1}\wedge...\wedge A_{k},\theta,\rho)= \begin{cases}\top&\text{if }A_{1} \wedge...\wedge A_{k}\theta\\ &\text{has a result}\\ \bot&\text{otherwise}\end{cases} \]  
For every possible value \(x\) in the trace, the following formula is used:  
\[eval(\forall_{x}\phi,\theta,\rho)=\{eval(\phi,\theta\cup x/m,\rho)|\forall_{ m}\in\rho\}\]  
If the formula \(\forall_{x}\phi\) is included in another formula, the result of evaluation is provided by:  
\[eval(\forall_{x}\phi,\theta,\rho)= \begin{cases}&\text{if }\exists_{m}\in\rho \text{ where}\\ \bot&\text{$eval(\phi,\alpha,\rho)=\bot$ \ with}\\ &\alpha=\theta\cup x/m\\?&\text{otherwise}\end{cases} \]  
The result \"\(\bot\)\" represents any violation that has been found. The evaluation of \(\exists_{x}\) is quite similar to the \(\forall_{x}\), but it is looking for a \"\(\top\)\" result. \[eval(\exists_{x}\phi,\theta,\rho)= \begin{cases}\top&\text{if }\exists_{m}\in\rho \text{ where}\\ \top&\text{$eval(\phi,\alpha,\rho)=\top$ with}\\ &\alpha=\theta\cup x/m\\?&\text{otherwise}\end{cases} \]  
The evaluation processes for \(\forall_{y>x}\), \(\exists_{y>x}\) and \(\phi\rightarrow\varphi\) are the same as described before; we will not repeat them here. The interested readers can have a look at our previous work [20,34]. We also provide the evaluation algorithm in the following. ```
Input: Formalized requirement \(\phi\), substitution \(\theta\) with initial bindings and finite trace \(\rho\) Output: Pass if the formula has a solution, _Fail_ if exist a violation of the requirements, '?' if no definite response can be provided if\(\rho\) is not empty, \(\phi\) is not emptythen \(verdict\leftarrow\top\); for(\(m_{0}\wedge...\wedge m_{m}\)) \(\in\rho\)do \(\theta^{\prime}\leftarrow\theta m_{i}\); for(\(A_{0}\wedge...\wedge A_{n}\)) \(\in\)\(\phi\) where \(verdict\
eq\perp\)do if\(\theta^{\prime}A_{0}\wedge...\wedge\theta^{\prime}A_{n}=\top\)then \(verdict\leftarrow\top\), return \(verdict\);  end if else \(verdict\leftarrow\perp\), return \(verdict\);  end if  end for if\(verdict=\top\)then  next \(m_{i}\), \(final\gets pass\), return \(final\);  end if else  next \(m_{i}\), check_end_of_file(\(m_{i}\)); if\(check\_end\_of\_file(m_{i})=\top\)then \(final\gets inconclusive\), return \(final\);  end if else \(final\gets fail\), return \(final\);  end if  end if  end for
```  
**Algorithm 1**Algorithm for eval (\(\phi\), \(\theta\), \(\rho\)). The algorithm starts by checking the existence of a trace \(\rho\) and a requirement \(\phi\). Then, if \(\phi\) contains subformulas, they will be sequentially tested by using recursive calls. For testing a formula \(\phi\) on a finite trace \(\rho\), the algorithm will firstly assign the values to substitution \(\theta\) from each message \(m\) in the trace. Then, the obtained \(\theta^{\prime}\) will be used to compare with each atom in the formula \(\phi\).