% $Id: mcheck.tex 16662 2009-02-02 04:43:57Z gokhale $

\subsection{Verifying the Generated QoS Configurations}
\label{sec:modelcheck}

QUICKER uses a novel approach to check the correctness of the generated
configurations.  QUICKER achieves this capability by reducing the
problem to a model checking problem.  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
middleware component such as in our CIAO middleware, 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}
\bfcaption{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,
a property simply means whether or not the QoS configurations are
verified correct.  Thus, since we need to verify the values of various
QoS options as a means to check whether the 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.   We demonstrate this capability in the context of a
representative system in Section~\ref{sec:mcheck-basicsp}. 

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. 


\subsection{Validating BasicSP QoS Configuration Dependencies via Model-checking}
\label{sec:mcheck-basicsp}

The QoS extensions to the BIR format described in
Section~\ref{sec:modelcheck} are used 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=\columnwidth,keepaspectratio]{dependency}
  \bfcaption{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.}
  \label{fig:dependency}
\end{figure}

A similar approach can be carried out if the DRE system has multiple
different modes of operation, which in turn define multiple different
regions of operation.  Each such operating region may then have a set of
configuration options.  The Bogor-based model checking approach can now
verify the dependencies among options for connected components for
multiple modes of operation.  The verified sets of configurations can
then be used by the middleware to seamlessly adapt from one set to
another depending on the mode.


