% $Id: correctness.tex 16663 2009-02-02 04:55:42Z gokhale $
\section{Correctness of the Model Transformation Process and Generated
Configurations}
\label{sec:correctness}

In any approach that provides automation, two key assurances must be
provided: (1) that the automation process itself is correct, and (2)
that the artifacts produced as a result of the automation are correct.
In our approach, it is therefore necessary to provide an assurance
that the process of mapping the QoS policy specifications into
middleware-specific QoS configurations is correct, and that the
generated mappings themselves are correct including all the
dependencies between the mappings.   

This task entails ensuring the correctness of the QoS mapping
process, \emph{i.e.}, providing assurance that the QoS configurations
generated are equivalent to the QoS policies from which these
options are mapped.  In our case, this translates to verification of
the QoS transformations used, and (2) correctness of the generated QoS
options themselves, \emph{i.e.}, whether the configuration parameters
themselves are correct and whether the individual values of these
options are appropriate locally (\emph{e.g.}, for a component) as well
as globally (\emph{e.g.}, for all dependent components).  

\input{verify}

\input{mcheck}

\subsection{Resolution of Challenges 2 and 3} 
\label{sec:resolve2_3_4}

Challenge 2 from Section~\ref{sec:issues} is resolved by the assurance
of correctness provided by structural correspondence as follows.  Pre-
and post-conditions can be satisfied by assuring that the generated
configurations are indeed the expected artifacts.  Since the
transformations are automated, developers need not worry about the
plethora of configuration options and their interactions.  Not all
invariants may be satisfied by the transformation process alone. 
For example, whether the ORB can eliminate or minimize priority
inversions depends solely on the quality of the middleware
implementation and the OS platform on which it runs.  To address this
shortcoming, a potential solution may require that the transformation
algorithms be enhanced to incorporate features of the available 
platform-specific support, such as the real-time features provided by
the OS.   We do not provide this capability in this paper.

Finally, the model-checking extensions ensure that the system QoS
configuration is valid at the local- and global-level including all the
dependencies.  The entire process is automated in QUICKER and thus,
can be repeated  when changes in QoS policies of an application occur.
For example, QUICKER helps DRE systems to evolve by automatically
(re-)calculating the dependencies between options, and can thus be
used repeatedly by DRE developers during the entire lifecycle thereby
addressing Challenge 3.

Note that QoS configuration challenges also arise during runtime.  We do
not expect model checking to be applied at runtime.  Rather, in the
context of DRE systems, system developers will formally define the
regions of operation of the system and the desird QoS policies as system
conditions vary.  Accordingly QUICKER can synthesize and verify the
configurations for all the operating regions.  The middleware is then
subsequently responsible for adapting to the new configurations as the
operating region of the system changes.  QUICKER guarantees \emph{a
  priori} availability of QoS configurations that are tailored to each
operating region. 



%%% Local Variables: 
%%% mode: latex
%%% TeX-master: "NFP_SoSym2009"
%%% End: 
