@@ -86,7 +86,7 @@ The remainder of this section defines the properties we formalized and verified.

\item\textit{functional properties}, which are extracted from the SHOULD's and the MUST's of the RFC specifications. They may have a security impact.

\end{enumerate}

A key point to note is that properties are checked not on the actual concrete model of the {\dsut}, but on an abstract model, which represents an over-approximation of the {\dsut} induced by the {\dmapper}. This is unlike in~\cite{TCP2016}, where properties where checked on a concretization of the learned model obtained by application of a reverse mapping. Building a reverse mapper is far from trivial given the {\dmapper}'s complexity. Performing model checking on an abstract model means we cannot fully translate model checking results to the concrete (unknown) model of the implementation. In particular, properties which hold for the abstract model do not necessarily hold for the implementation. Properties that don't hold however, also don't hold for the {\dsut}.

A key point to note is that properties are checked not on the actual concrete model of the {\dsut}, but on an abstraction of the {\dsut} that is induced by the {\dmapper}. This is unlike in~\cite{TCP2016}, where properties where checked on a concretization of the learned model obtained by application of a reverse mapping. Building a reverse mapper is far from trivial given the {\dmapper}'s complexity. Thus we need to be careful when we interpret model checking results for the learned model. Also, we must be aware that when some property does not hold for the abstract model, and the model checker provides a counterexample, we still need to check whether this counterexample is an actual run of the abstraction of the {\dsut} induced by the mapper. If this is not the case then the counterexample demonstrates that the learned model is incorrect.