% $Id: verify.tex 16661 2009-02-02 04:13:30Z gokhale $
\subsection{Verifying the Correctness of the Transformations and
  Generated Artifacts}
\label{sec:corresp}

The difficulty in verifying the correctness of model transformations
is akin to the difficulty in verifying compilers for high-level
languages.  This difficulty can be alleviated to some extent if we
restrict the verification of the transformation process to the
verification of instances of the transformations.  In other workds, a
transformation may be said to have executed correctly if a certain
instance of its execution produces an output model that preserves
certain properties of interest.  We designate such an instance as
certified correct.
 
In our approach, we have used a transformation verification technique
based on structural
correspondence~\cite{Karsai_ENTCS:08,Karsai_ECEASST:08}.
The intuition behind this approach is as follows:  Specific structural
configurations in the source model (such as the QoS policies in PICML)
produce specific structural configurations in the target model (such
as CIAO/RTCORBA-specific QoS configurations in CQML).  The rules to 
accomplish the structural transformations may be simple or
complicated.  However, it is fairly straightforward to compare and
verify that the correct structural transformation was made if we
already know which parts of the source structure map to which parts of
the target structure. 

In our technique to verify a transformation by structural
correspondence, we first define a set of structural correspondence
rules specific to a certain transformation, which are effectively a
relation between elements of the source model and that of the target
model.  We then use cross-links to trace source elements with the
corresponding target elements, and finally use these cross-links to
check whether the structural correspondence rules hold.  In essence,
we expect that the correspondence conditions are independently
specified for a model transformation, and an independent tool checks
if these conditions are satisfied by the instance models, after the
model transformation has been executed. 

\iffalse
In other words, the correspondence conditions depend purely on the
source and target model structures and not on the rewriting rules
necessary to effect the transformation.  Since the correspondence
conditions are specified in terms of simple queries on the model
around previously chosen context nodes, we expect that they will be
easier to specify, and thus more reliable than the transformation
itself.  We also assume that the model transformation builds up a
structure for bookkeeping the mapping between the source and target
models. 
\fi

Figure~\ref{fig:verify} illustrates the verification
technique.  The source and target portions of the transformation are
treated as typed, attributed graphs, called the source and target
metamodels.  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
metamodels and specifying what constitutes a correct transformation
for these nodes. The existing transformation rules written in the
GReAT visual language are extended to generate annotations along with
the instance models.  Once this setup has been completed, every
execution of the  transformation is followed by an automatic
correctness checker, which uses the generated annotations to check if
the correctness conditions were satisfied for the generated output
model.  Recall from Section~\ref{sec:algo} that the GR-Engine in GReAT
is responsible for executing the transformations and hence also the
correctness checking.  If this check is satisfied, we can say that the
output model instance is `certified' correct.  

\begin{figure}[htb]
  \centering
  %\vspace{-0.4in}
  \includegraphics[width=\columnwidth,keepaspectratio]{verify}
  \bfcaption{Verifying model transformations}  
  \label{fig:verify}
\end{figure}

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.  This is the responsibility of
the transformation developer to specify these rules.  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.

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.   In the figure we
show the composite metamodel that relates an element from PICML (in
this case the QoS policies for a request/response scenario) with an
element from CQML (in this case the request handling priority model
supported in RTCORBA).

\begin{figure}[htb]
  \centering
  %\vspace{-0.4in}
  \includegraphics[width=\columnwidth,keepaspectratio]{cross-link}
  \bfcaption{Structural correspondence using cross-links}  
  \label{fig:cross-link}
\end{figure}

\texttt{RTPolicy} is an input language object that denotes
real-time policy specification for a component.  It has a
correspondence relation with \texttt{RealTimeConfiguration} output
language object indicated by the 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{RTPolicy} is set to \textsc{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
\textsc{server\_declared} in the output model.  Otherwise
\texttt{pri\-or\-ity\_mo\-del} should be set to
\textsc{client\_propagated}.  

Moreover, if \texttt{pri\-or\-ity\_mo\-del} is set to
\textsc{se\-rv\-er\_de\-cl\-ar\-ed} for a component, \texttt{Lane}
values at that component and \texttt{Bande\-dConn\-ection} 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 \textsc{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.

Note that the transformation verification does not imply the correctness
of the QoS mapping rules themselves -- rather it provides an assurance
that the model transformation specification and implementation correctly
mapped the QoS specifications that were formulated before.  



