% $Id: mcheck.tex 16638 2009-01-29 19:00:10Z gokhale $
\sqzlarge
\subsubsection{Verifying the generated QoS configurations}
\label{modelcheck}
\sqztiny
This section illustrates how the correctness of QoS configuration mappings
is verified using the
Bogor model-checking framework, which is a customizable explicit-state model
checker implemented  as an Eclipse plugin.  Verifying a system using Bogor
involves defining  (1) a model of the system using the \emph{Bogor Input 
Representation} (BIR) language and (2) the \emph{property} (\emph{i.e.},
specification) that the model is expected to satisfy.  Bogor then traverses the
system model and checks whether or not the property holds.  To validate QoS
configuration options of an application using Bogor, we need to
specify the application model and its QoS configurations.
We use Bogor's extension features to customize the
model-checker for resolving the QoS configuration challenges 
for component-based applications.

It is cumbersome to describe middleware QoS configuration options using the
default input specification capabilities of BIR.  This is because such
a representation is at a much lower level of abstraction compared to
domain-level concepts, such as components and QoS options, which we want to
model-check.  Additionally, specifying middleware QoS configuration options
using BIR's low-level constructs can yield an unmanageably large state space
since representing domain-level concepts with a low-level BIR specification
requires additional auxiliary states that may be irrelevant to the
properties being model-checked~\cite{Bogor:03}.  Therefore we have
defined composite language constructs that represent functional sub-systems
(such as components) and QoS options (such as thread pools) as though they were
native BIR constructs. 

Listing~\ref{extn:qosextensions} shows an example of our QoS extensions in Bogor
to represent QoS configuration options in middleware, which define two new data
types: \texttt{Component}, which corresponds to a CCM component, and
\texttt{QoSOptions}, which captures QoS configuration options, such as
\texttt{lane}, \texttt{band}, and \texttt{threadpool}.

\begin{BIRExtensions}[htb]
  %\begin{singlespace}%
   % \vspace{-0.4in}
    \begin{Verbatim}[frame=single,fontsize=\relsize{-2}]
extension QoSOptions for
edu.ksu.cis.bogor.module.QoSOptions.QoSOptionsModule
{
  // Defines the new type to be used for
  typedef lane;
  typedef band;
  typedef threadpool;
  typedef prioritymodel;
  typedef policy;
  // Lane constructor.
  expdef QoSOptions.lane createLane (
   int static, int priority, int dynamic);
  // ThreadPool constructor.
  expdef QoSOptions.threadpool
  createThreadPool (boolean allowreqbuffering,
   int maxbufferedrequests, int stacksize, int
   maxbuffersize, boolean allowborrowing);
  // Set the band(s) for QoS policy.
  actiondef registerBands (QoSOptions.policy
   policy, QoSOptions.band ...);
  // Set the lane(s) for QoS policy.
  actiondef registerLanes (QoSOptions.policy
   policy, QoSOptions.lane ...);
  ...
}
extension Quicker for
edu.ksu.cis.bogor.module.Quicker
{
  // Defines the new type.
  typedef Component;
  // Component Constructor.
  expdef Quicker.Component
  createComponent (string component);
  // Set the QoS policy for the component.
  actiondef registerQoSOptions (Quicker.Component
    component,QoSOptions.policy policy);
  // Make connections between components.
  actiondef connectComponents (Quicker.Component
    server,Quicker.Component client);
  ...
}
\end{Verbatim}
\vspace{-0.25in}
\caption{QUICKER BIR extension}
\label{extn:qosextensions}
\end{BIRExtensions}
In addition to defining constructs that represent domain concepts, such as
components and QoS options, we also need to specify the \emph{property} that the
application should satisfy. In our case, property simply means whether or
not the QoS configurations are verified correct. Thus, since we need to
verify values of various QoS options as means to check whether application property is
satisfied, we define \emph{rules} that capture values of these QoS 
options. BIR primitives are used to express these rules in the input specification of DRE
system.  Primitives are also used to capture component interconnections in BIR
format which are required for populating the dependency structure for the
specified input application.  They are also used later during verification of
options for connected components. 

QoS extensions are also helpful in maintaining and resolving
dependencies between application components. For example, consider
a real-time configuration of BasicSP scenario in which each of the 
\emph{GPS}, \emph{AirFrame}, and \emph{NavDisplay} components are
configured to have \texttt{priority bands} for separate service
invocation priorities and the \emph{Timer} component is configured
to support multiple priority levels during generation of pulse events.
Given such a configuration, we have that \texttt{priority 
band} values at \emph{GPS} (client) component must match 
\texttt{ThreadPoolLanes} at \emph{Timer} (server) component \emph{i.e.}, 
a direct configuration dependency exists between these two components. 

Further, since the pulse events are subsequently reported to \emph{AirFrame} and
\emph{NavDisplay} components there is a similar indirect dependency between
\texttt{band} values at these components and \texttt{lanes} at 
\emph{Timer} component. The dependency structure of BasicSP scenario is
maintained in QoS extensions to track such dependencies between QoS
options.  Figure~\ref{fig:dependency} represents the dependency
structure generated using QoS extensions with the given
configurations for our BasicSP scenario. Occurrences of change in configurations 
of either of the
dependent components are followed by detection of potential mismatches such that
all dependencies are exposed and resolved during application QoS design
iterations.

\begin{figure}[htb]
  \centering
  \includegraphics[width=0.5\columnwidth,keepaspectratio]{dependency}
%\vspace{-1.7in}
  \caption{Dependency structure of BasicSP. $L_{c}$ denotes threadpool lane and
   $B_{c}$ denotes priority bands at component $c$. {\sc sd} and {\sc cp} indicate
   the {\sc server\_declared} and {\sc client\_propagated} priority models, respectively.}
   \vspace{-0.10in}
  \label{fig:dependency}
\end{figure}
Applications that need to be model-checked by Bogor must be represented in BIR
format.  Writing and maintaining BIR manually can be tedious and error-prone for
domain experts (\emph{e.g.}, avionics engineers) since configuring application
QoS policies is typically done iteratively.  Depending on the number of
components and available configuration options, manual processes do not scale
well.

To automate the process of creating BIR specification of applications, we
therefore used the generative capabilities in GME to automatically generate BIR
specification of an application from its QoS configurations model.  This
generative process is done in GME using a model interpreter that traverses the
QoS configurations model and generates a BIR file that captures the application
structure and its QoS properties. Our toolchain therefore automates the
entire process of mapping application QoS policies to middleware QoS options, as
well as converting these QoS options into BIR.  A second model interpreter is
used to generate the Real-time CCM-specific descriptors required to configure
functional and QoS properties of an application and deploy it in its target
environment. In the next section we empirically validate these generated QoS 
configurations.

\noindent\textbf{Resolving Challenge 3 \& 4:} QUICKER transformation rules
contain information about the semantics of the QoS options, their
inter-dependencies, and how they affect the high-level QoS
requirements of a DRE system and therefore are used to assign values
to the subset of options chosen earlier.  Further, QoS options
semantics are known precisely during transformations, and thus QUICKER
ensures preservation of target typed graph semantics.  Component
interactions defined in input typed graph instance (\emph{i.e.},
source model), along with the user-specified QoS requirements captured
in that instance are used to completely generate an instance of the
output graph. Finally, the model-checking extensions ensure that the
application QoS configuration is valid at the local- and global-level.
The entire process is automated in QUICKER and thus, can be repeated 
when changes in QoS policies of an application occur. 
