% $Id: verify.tex 16638 2009-01-29 19:00:10Z gokhale $
\sqzlarge
\sqztiny
\subsubsection{Assuring the correctness of model transformation algorithms}
\label{sec:corresp}
\sqztiny
To provide an assurance that the QoS requirements 
specifications were correctly mapped into the QoS 
configuration model, we have used the transformation 
verification technique described in~\cite{Karsai_TR:07}. The 
source and target portions of the transformation are 
treated as typed, attributed graphs, and the 
correctness of the transformation is specified as a 
relation between these graphs. Such a relation, 
called a structural correspondence, is specified by 
identifying pivot nodes in the metamodel and 
specifying what constitutes a correct transformation 
for these nodes. 

Using structural correspondence, the verification consists 
of two phases: the specification of the correctness 
conditions, and the evaluation of the correctness. In the first 
phase, we identify important points in the transformation, and 
specify the structural correspondence rules for these points. From these 
rules, a model traverser is automatically generated, which will 
traverse and evaluate the correspondence rules on the instance models. This 
step needs to be performed only once. The second phase involves invoking 
the model traverser after each execution of the model transformation. In 
this phase, the model instance being transformed is traversed, and the 
structural correspondence rules are evaluated at each relevant node. If 
any of the rules are not satisfied, it indicates that the model has not 
been transformed satisfactorily. 
\begin{figure}[htb]
  \centering
  %\vspace{-0.4in}
  \includegraphics[width=0.7\columnwidth,keepaspectratio]{cross-link}
  \caption{Structural correspondence using cross-links}  
  \label{fig:cross-link}
\end{figure}

Structural correspondence rules are described using (1) specification of 
the correspondence condition itself, and (2) the rule path expressions, which are
similar to XPath queries.  
Figure~\ref{fig:cross-link} shows how we have used 
cross-links in GReAT as means of specifying the correspondence
condition between input and output language objects such that
their equivalence can later be established. 
\texttt{RTRequirements} is an input language object that denotes
real-time requirement specification for a component. It has a 
correspondence relation with \texttt{RealTimeConfiguration}
output language object, indicated by presence of a 
cross-link between them in Figure~\ref{fig:cross-link}. 

Additionally, one of the transformation rules in our
QoS mapping algorithms states that if the Boolean 
attribute \texttt{fixed\_priority\_service\_execution} of
\texttt{RT\-Re\-qu\-ir\-em\-ents} is set to {\sc true} in the input 
model, then \texttt{pri\-or\-ity\_mo\-del} attribute of 
\texttt{Pri\-or\-it\-yM\-od\-el\-Po\-li\-cy} object be set to 
{\sc server\_declared} in the output model. Otherwise 
\texttt{pri\-or\-ity\_mo\-del} should be set to 
{\sc client\_propagated}. Additionally, if 
\texttt{pri\-or\-ity\_mo\-del} is set to 
{\sc se\-rv\-er\_de\-cl\-ar\-ed} for a component, \texttt{Lane} values 
at that component and \texttt{BandedConnection} values at 
its clients must match. In order to complete the correspondence rule
specification, the above is encoded as a rule path expression
as follows:

{\footnotesize{
\noindent\verb+(RTRequirement.+ \\
\verb+fixed_priority_service_execution =+
  \verb+true+ 
  $\wedge$ \\
   \verb+(+ $\forall$ \verb+b+ $\in$ 
      \verb+RTConfiguration.+ 
      \verb+BandedConnection+ \\
      \verb++$\exists$ \verb+l+ $\in$ \verb+RTConfiguration.+
          \verb+Lanes :+\\
          \verb+    (b.low_range+ 
          $\leq$ \verb+l.priority+ 
            $\leq$ 
            \verb+b.high_range))+ $\wedge$ \\
\verb+RealTimeConfiguration.PriorityModelPolicy.+ \\
    \verb+priority_model = "SERVER_DECLARED")+ $\vee$ \\
    \verb+(RTRequirement.+ \\
    \verb+fixed_priority_service_execution = false+ $\wedge$ \\
\verb+RealTimeConfiguration.PriorityModelPolicy.+ \\
\verb+priority_model = "CLIENT_PROPOGATED")+ 
}}

If this expression evaluates to {\sc true} on an instance model, then 
it implies that the QoS configuration for this particular property has 
been mapped correctly. This applies to the \texttt{RTRequirements} and 
\texttt{RealTimeConfiguration} classes, and correspondence condition is added 
as a link between these classes in the metamodel. Similar to correspondence
condition between \texttt{RTRequirements} and \texttt{RealTimeConfiguration}
we described, other conditions for each of the QoS mapping rules have been
specified ensuring that the transformation is verified correct if all these 
conditions are satisfied.


