% $Id: modelcheck.tex 16638 2009-01-29 19:00:10Z gokhale $

\subsection{Validating QoS Configuration Options using Model-Checking}
\label{modelcheck}

After the model-transformation portion of the QUICKER toolchain
generates a CQML model comprising the QoS configuration options, the
correctness of these options must be validated before the application
assembly is deployed.  We validate these options using the Bogor
model-checking framework, which is a customizable explicit-state model
checker implemented as an Eclipse plugin.

Validating 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, therefore, we need to specify
the application model and the QoS configuration options that the
application is expected to
%\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}
\caption{QUICKER BIR Extension}
\label{extn:qosextensions}
%\label{extn:qosextensions}
%\end{singlespace}
%\end{BIRExtensions}
satisfy.  To express this specification in the BIR input language, we
leveraged Bogor's customization features to define new types and
primitives that allow manipulation of the newly defined types.  The
remainder of this section describes QUICKER's model-checking
capabilities and shows how our BIR extensions help resolve the
challenges described in Section~\ref{sec:challenges} related to
validation, option dependency tracking, and providing input to dynamic
QoS adaptation frameworks.

\textbf{$\bullet$ BIR input extensions.}  Bogor provides the BIR
language to specify input to its model-checker.  It is cumbersome,
however, to describe middleware QoS configuration options using the
default capabilities of BIR since (1) this representation is at a much
lower level of abstraction compared to domain-level concepts, such as
components and QoS options, that we want to model-check, and (2)
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 state that may be irrelevant to the
properties being model-checked~\cite{Bogor:03}.  To specify and
model-check properties more closely to the domain of component
middleware QoS configuration options, therefore, we used BIR's input
extension feature to define composite constructs that represent
concepts (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 BIR
extensions to represent QoS configuration options in middleware.  The
extensions shown in the listing 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}.  Each
\texttt{Component} maintains a single \texttt{QoSOptions} instance
internally.  Depending on a component's role (\emph{i.e.},
\texttt{client} or \texttt{server}), various individual QoS options
may need to be set. Since these BIR extensions allow representation of
middleware QoS options, we refer to them as \emph{QoS extensions}.

\textbf{$\bullet$ BIR primitives.}  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.  Since
a \emph{property} can be denoted by multiple QoS options, we define
\emph{rules} to capture valid option values.  BIR primitives are used to
express these rules in the input specification of MMS mission prototype, as
shown in Listing~\ref{extn:birspecification}.
\begin{BIRExtensions}[htb]
  %\begin{singlespace}%
   % \vspace{-0.4in}
    \begin{Verbatim}[frame=single,fontsize=\relsize{-2}]
// Declaration of the extensions
// Declare all data-type variables to be used in this
// file
loc loc0: live {} //
  do
  {
    // Instantiate the components with QoSPolicies;
    // Register policies with components; Register
    // components as per assembly structure in CQML 
    // model
    ...
  } goto loc1;
loc loc1: live {pm}
  when ! Quicker.hasQoSOptions (Comm)
  do
  {
    pm := Quicker.getPriorityModelPolicy (Comm);
  } goto loc2;
loc loc2: live {pm}
  do
  {
    when (pm == pmodel.SERVER_DECLARED) do {} 
       goto loc3;
    when !(pm == pmodel.SERVER_DECLARED) do {} 
       goto loc12;
  } goto loc30;
loc loc3: live {lr1}
  do
  {
    lr1 := QosOptions.getLowerBound (Analysis_1);
  } goto loc4;
    ...
loc loc8: live {hr3}
  do
  {
    lr1 := QosOptions.getUpperBound (Analysis_3);
  } goto loc9;
  ...
\end{Verbatim}
\caption{Application-specific BIR Primitives}
\label{extn:birspecification}
%\end{singlespace}
\end{BIRExtensions}

Primitives are the language constructs we defined to access and
manipulate data types for Real-time CCM. For example, instances of
\texttt{QoSOptions} can be created and manipulated using various
primitives defined in Listing~\ref{extn:birspecification}.  The rule
defined in this listing first determines the \emph{Priority Model} of
a particular component using the \texttt{getPriorityModelPolicy}
primitive.  If the \emph{Priority Model} policy of a component is
\textsc{server\_declared}, the rule calculates the range of connected
component's \emph{PriorityBand} values using \texttt{getLowerBound}
and \texttt{getUpperBound} primitives.  Finally, this rule also checks
if the range calculated above matches the priority associated with
\emph{Comm} component's thread pool (not shown in the listing).

Primitives are also used to capture component interconnections in BIR
format.  These interconnections are needed to construct the dependency
structure for the specified input application, such as the MMS mission
prototype.  They are also used later during validation of options for
connected components.

\textbf{$\bullet$ Generative capabilities.}  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.}, spacecraft engineers) since configuring application QoS
policies is typically done iteratively.  Depending on the number of
components and the number of 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 CQML model.
This generative process is done in GME using a model interpreter that
traverses the CQML model and generates a BIR file that capture the
application structure and its QoS properties.  The QUICKER 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.

\noindent{\bf Resolving Challenge 2: Ensuring validity of QoS
configuration options.}  A priority-banded connection between {\em
Analysis} and \emph{Comm} components must have matching policies and
values, as discussed in Section~\ref{sec:challenges}.  QUICKER uses
BIR primitives to ensure the validity of QoS configuration options for
MMS mission components.  To show how the primitives (and rules defined
using those primitives) can ensure valid QoS configuration options, we
deliberately introduced a QoS misconfiguration by specifying the
concurrency model of \emph{Comm} component to use \emph{Thread Pool}
without \emph{Lanes} in the PICML model of MMS mission prototype.  The
same configuration is contained in the (transformation-generated) CQML
model of the application, which is used to generate the BIR
specification.

One of the rules specified in Listing~\ref{extn:birspecification} uses
BIR primitives to validate that the banded connection between {\em
Comm} and \emph{Analysis} components have matching priority values.
The change to QoS option (of \emph{Comm} component) outlined above
therefore causes a misconfiguration, which is detected by the rule in
Listing~\ref{extn:birspecification}.  Rules defined using BIR
primitives are thus used in QUICKER to provide an automated tool
support for ensuring the validity of QoS configuration options.

\noindent{\bf Resolving Challenge 3: Resolving dependencies between QoS
  configuration options.} There is a dependency between \emph{Gizmo}
components and \emph{Comm} component in the MMS mission prototype, as
explained in Section~\ref{sec:challenges}, \emph{i.e.}, the \emph{Gizmo}
component invocation priority values should match the thread pool lane
priority values. The dependency structure of the MMS mission prototype is
\begin{figure}[htb]
  \centering
  \includegraphics[width=\columnwidth,keepaspectratio]{dependency}
\vspace{-2.2in}
  \caption{Dependency structure of MMS Mission}
  \label{fig:dependency}
\end{figure}
maintained in QoS extensions to track such dependencies between QoS
options.  Figure~\ref{fig:dependency} represents the dependency
structure generated using QoS extensions for the MMS mission. When a 
change occurs to either of the dependent QoS options (\emph{ i.e.}, the 
thread pool lanes of \emph{Comm} component and the invocation priority 
of the \emph{Gizmo} component), the QoS extensions detect mismatches 
between the priority values.

Even with a thorough understanding of middleware QoS configuration options,
it is tedious and error-prone to track these dependencies and detect
mis-configurations.  As the number of components and component
interconnections increases, this problem is exacerbated.  QUICKER helps
developers automatically track these dependencies throughout the evolution
of an application.

\noindent {\bf Resolving Challenge 4: Ensuring validity of QoS
  configuration options with changes in QoS policies.}  A dynamic
reconfiguration that triggers changes in QoS options of \emph{Gizmo}
components necessitates reconfiguration of components dependent on {\em
  Gizmo} and revalidation of the configuration, as discussed in
Section~\ref{sec:challenges}.  Our QoS extensions explore the possible
states of an application and generate a set of valid application states.
Since we are only concerned with the QoS configuration options, we use the
term ``application states'' to represent just the set of QoS configuration
option values for all the components in an application.

\begin{figure}[htb]
  \centering
  \includegraphics[width=\columnwidth,keepaspectratio]{states}
  \caption{Snapshot of QoS Configuration States}
  \label{fig:states}
\end{figure}

Figure~\ref{fig:states} shows the generated states for the MMS mission
prototype.  For simplicity, this figure only shows the generated states for
\emph{Analysis} and \emph{Comm} components.
% ; further, only states corresponding to the server-side QoS options of
% \emph{Analysis} components and the client-side QoS options of the
% \emph{Comm} component are shown.
For our explanation purposes, it is assumed that the rest of the
application state is valid and does not change.  The server QoS options in
Figure~\ref{fig:states} are denoted by an $n$-tuple consisting of: (1)
\texttt{Priority Model} (\textsc{server\_declared}, or \textsc{
  client\_propagated}), (2) \texttt{Priority Value} (RTCORBA::Priority),
(3) set of \emph{l} \texttt{Lane} configurations (4) \texttt{ThreadPool}
configuration.  Similarly, client QoS options are denoted as $m$-tuple
consisting of all the priority \texttt{Band} configurations for a client.

In the MMS mission prototype specification, if new mission goals require
changes in QoS options of the \emph{Comm} and \emph{Analysis\_3} components
the application state could change from initial state G1 to G2.  Likewise,
the state could change to G3, when new mission goals dictate that priority
\texttt{band} configuration for \emph{Analysis\_1} and \emph{Analysis\_2}
components should change.  From each of these states, the system could
enter a number of possible states depending on further changes in QoS
configuration.  Each of G1, G2, and G3 (along with other generated states)
are valid application states.  By exploring all the possible application
states, QoS extensions generate validated states of an application at
design-time, which can be used to select runtime QoS configurations by the
RACE QoS adaptation framework.

By exploring all the possible states of an application, QoS extensions
identify both the set of valid and invalid application states.  We can then
construct an automaton using the chain of configuration modifications
(generated by the model-checker) from the application state corresponding
to the initial QoS configuration that lead to the invalid state.  This
automaton can guide the behavior of the RACE controller that adapts
configuration options dynamically, to ensure that reconfiguration will not
yield an invalid application state.
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "QoSMapping"
%%% End:
