%% $Id: casestudy.tex,v 1.42 2004/12/31 19:38:42 schmidt Exp $

\section{Demonstrating Integrated CoSMIC$\leftrightarrow$Cadena
Capabilities via a Robot Assembly Case Study} 
\label{casestudy}

This section describes a case study of a robot assembly application we
developed in conjunction with colleagues at Lockheed Martin.  This
application is representative of DRE systems in the process control
domain, {\em i.e.}, it defines an {\em assembly line} with robots
creating various types of {\em goods}, which in our case study are
wrist watches assembled by robots.  We describe the robot assembly
application below to illustrate the benefits of integrating and
applying the CoSMIC and Cadena MDD toolsuites, as described in
Sections~\ref{overview} and~\ref{approach}.  In particular, this case
study illustrates how developers of the robot assembly application
required multiple MDD tools, each providing different capabilities,
such as configuration, deployment, schedulability analysis, and model
checking.  The source code and integrated MDD tools for this example
are available in the CIAO release from
\url{www.dre.vanderbilt.edu/CIAO}.

\subsection{Structure and Functionality of the Robot Assembly Application}
\label{sfraa}

Figure~\ref{fig:robot_model} illustrates the five core components in
the robot assembly application: {\tt Management\-Work\-Instruction},
{\tt Watch\-Setting\-Manager}, {\tt Human\-Mach\-ine\-Interface}, {\tt
Pallet\-Conveyor\-Manager}, and {\tt Ro\-bot\-Manager},
\begin{figure}[htb]
\vspace{-.5in}
\center{\includegraphics[width=4.5in]{eps/robot_assembly_arch.eps}}
\vspace{-.4in}
\bfcaption{Robot Assembly Model} 
\label{fig:robot_model}
\vspace{0.1in}
\end{figure}
each of which are implemented as CCM components using CIAO.  These
individual CCM components can be interconnected together to form {\em
CCM component assemblies} and ultimately deployed using DAnCE to
create complete applications.

\begin{figure}[htb]
\vspace{-.4in}
\center{\includegraphics[width=4.5in]{eps/robot_prod_seq.eps}}
\vspace{-.5in}
\bfcaption{Robot Assembly Production Sequence} 
\label{fig:robot_prod_seq}
\vspace{0.1in}
\end{figure}
Figure~\ref{fig:robot_prod_seq} depicts a sequence diagram for the
robot assembly production process.  The {\tt
Management\-Work\-Instruction} and {\tt Human\-Machine\-Interface}
components interact with humans, whereas the {\tt
Pallet\-Conveyor\-Manager} and {\tt Rob\-ot\-Manager} components
interact with the pallet moving and assembling tools hardware devices,
respectively.  The normal operation of the robot assembly application
involves the following steps:
%\sqztiny
\begin{enumerate}%\crunchlist
\item The {\tt Management\-Work\-Instruction} asks for a watch to be
produced by sending an event to the {\tt Watch\-Setting\-Manager}.

\item The {\tt Watch\-Setting\-Manager} emits an event to the {\tt
Human\-Machine\-Inter\-face} asking to validate the order.  The {\tt
Human\-Machine\-Interface} accepts the order by invoking an operation
on a CCM facet belonging to the {\tt Watch\-Setting\-Manager}.

\item The {\tt Watch\-Setting\-Manager} uses a different event to
notify the {\tt Manage\-ment\-Work\-Instruction} that the order was
accepted and then displays the work on the {\tt
Human\-Machine\-Interface}.

\item The {\tt Watch\-Setting\-Manager} emits an event to the {\tt
Pallet\-Conveyor\-Manager} to move the pallet into position.  The {\tt
Pallet\-Conveyor\-Manager} then responds with another event
acknowledging the status of good positioning on the pallet. This event
includes an enumerated type indicating status, such as acceptance,
rejection, completion, failure, and/or cancellation.

\item The {\tt Watch\-Setting\-Manager} again emits an event to the
{\tt Human\-Machine\-Interface} asking for confirmation to perform a
production step.  The {\tt Human\-Machine\-Interf\-ace} accepts by
invoking an operation on a facet.

\item The {\tt Watch\-Setting\-Manager} emits an event to the {\tt
Robot\-Manager} asking it to process the pallet.  The {\tt
Robot\-Manager} performs the job and then responds via an event
acknowledging the success (or failure) of the assembling operation.

\item The {\tt Watch\-Setting\-Manager} displays the completed work to
{\tt Human\-Mac\-hine\-Interface} via an event.  The {\tt
Human\-Machine\-Interface} validates the work via a facet operation
call (same as in bullet 1).

\item The {\tt Watch\-Setting\-Manager} sends an event asking the {\tt
Pallet\-Conveyor\-Manager} to move the pallet out of the working area
and into a finishing area.

The {\tt Pallet\-Conveyor\-Manager} notifies the status of the
operation back to the {\tt Watch\-Setting\-Manager} with the
acknowledgment event already discussed. Steps 2-7 can be repeated if
there are additional pallets to process.

\item The {\tt Watch\-Setting\-Manager} sends an event to the {\tt
Management\-Work\-Instruction} notifying it that the requested job has
been completed.
\end{enumerate}

\subsection{Key Capabilities Provided by CoSMIC and Cadena Integration for the Robot Assembly Application}
\label{sec:capabilities} 

Section~\ref{sfraa} described the structure and functionality of the
robot assembly application.  We now illustrate the key challenges
encountered when integrating the CoSMIC and Cadena MDD toolsuites and
applying them to the robot assembly case study.

\paragraph{Capability 1: Choosing appropriate communication mechanisms.}
\sqztiny Developers of large-scale component-based DRE systems must
determine which communication mechanisms their components should use
to interact.  A key design decision is whether to use CCM {\em facets
and receptacles}, which can perform point-to-point synchronous
operation invocations between components, or {\em event sources and
sinks}, which can exchange typed messages asynchronously with one or
more components.  Applying an MDD tool like PICML
(Section~\ref{cosmic}) can help developers reason more effectively
about which communication mechanism to select.  Below, we demonstrate
how our MDD tools help developers make better design choices.

\begin{figure}[htbp]
\vspace{-.1in}
\center{\includegraphics[width=3.8in]{eps/robot_picml.eps}}
\vspace{0in}
\bfcaption{Robot Assembly CCM Component Assembly Visio Drawing}
\label{fig:robot_picml}
\vspace{0.1in}
\end{figure}
Figure~\ref{fig:robot_picml} shows a Visio drawing of the robot
assembly component interaction.  We used this informal drawing to
guide our subsequent formal modeling and analysis of the robot
assembly application.  In particular, we created a model of the CCM
component assembly in PICML and then used Cadena to analye, validate,
and refine this model.  After validation by Cadena, we used the CoSMIC
toolsuite to deploy, configure and run the robot assembly application.
Figure~\ref{fig:robot_picml_error} (without the connection pointed by
the arrow) represents the PICML model that captures the application
represented by the Visio drawing in Figure~\ref{fig:robot_picml}.
\begin{figure}[htbp]
\vspace{0in}
\center{\includegraphics[width=3.8in]{eps/robot_picml_error.eps}}
\vspace{0in}
\bfcaption{Erroneous Robot Assembly PICML Model}
\label{fig:robot_picml_error}
\vspace{0.1in}
\end{figure}

Unlike the informal Visio drawing, the PICML model is semantically
navigable, down to the data types and events exchanged by every
operation and event communication.  By inspecting the PICML model, we
can quickly spot design fallacies and/or vulnerabilities, {\em e.g.},
the return value of the facet invocation for the response of {\tt
Human\-Machine\-Interface} to {\tt Watch\-Setting\-Manager}
(Section~\ref{sfraa}) is {\tt void} and there are no out or inout
parameters, yet the operation is not defined as a CORBA {\tt oneway}.

Further analysis indicates that a more appropriate choice for this
communication would be an asynchronous connection (event) rather than
a facet/\-receptacle.  This analysis thus reveals a design mistake
made by the developers at the components (IDL) modeling stage.  Such
mistakes are less common when working with visual modeling
environments due to the visual feedback developers receive
continuously.  There is still a possibility of errors due to the fact
that at component (IDL) modeling stage the view of the CCM component
assembly providing the ``big picture'' is not yet available.  At the
time the component assembly is also modeled, however, the presence of
a navigable visual model significantly helps developers spot such
problems, compared with reading hundreds of lines of CORBA IDL code.
In addition, refinement cycles for correcting such errors in the IDL
and then adjusting the component assembly accordingly are much faster
to perform with a visual modeler than when dealing with low-level
source code.

\paragraph{Capability 2: Detecting type mismatches at design-time vs. run-time.}
\label{sec:mismatch}
\sqztiny As mentioned in Section~\ref{intro}, a key goal of MDD is
achieving ``correct by construction'' programs.  In particular, MDD
tools should allow only correct choices and/or detect maximum number
of errors at design-time rather than run-time.  Constraining a correct
choice or performing an early detection of mistakes significantly
reduces the time needed for fixes.

To evaluate how effectively our integrated CoSMIC and Cadena tools
described in Section~\ref{approach} work in the context of our robot
assembly application, we deliberately tried to introduce a mistake in
our component assembly by connecting an additional port to a
destination port of the wrong type.  This mistake is detected by
PICML's constraint checker because the two ends are not of the same
type, and thus disallowed by the PICML paradigm.  It would not be
desirable, however, to have trivial human mistakes detected by only
one tool ({\em e.g.}, PICML), as this would defer the detection
significantly when users work for long period of time on other tool(s)
({\em e.g.}, Cadena) before going back to PICML.

Cadena (described in Section~\ref{cadena}) also immediately detects a
set of potential human mistakes, including connections with mismatched
endpoints and mismatched type for properties on components.  These
checks are performed both at modeling time and model-import time and
can be verified, {\em e.g.}, by importing into Cadena an erroneous
model produced by a tool that has weaker validation support.  In our
case, PICML is (currently) the only other tool, so testing this
feature required manually disabling PICML's constraint checker, manual
creation of an invalid connection, and then exporting the result to
Cadena.

For this example, we chose to connect the {\tt analysis} receptacle of
the {\tt Watch\-Setting\-Manager} to the {\tt controller} facet of
{\tt Pallet\-Conveyor\-Manager}, as shown in
Figure~\ref{fig:robot_picml_error} with a block arrow.
Figure~\ref{fig:robot_picml_error_detect} shows how Cadena detected
the wrong connection, and printed an error message.  Early (possibly
immediate) detection of user mistakes, even when limited to simple
ones, is important since it reduces the work that must be undone to
roll back to a valid project state when a mistake is detected.
\begin{figure}[htb]
\vspace{0in}
\center{\includegraphics[width=3.7in]{eps/robot_cadena_error_detect.eps}}
\vspace{0in}
\bfcaption{Error Detected by Robot Assembly Cadena Model} 
\label{fig:robot_picml_error_detect}
\vspace{0.1in}
\end{figure}

\paragraph{Capability 3: Advanced model checking of component assemblies.}
\label{sec:model-check}
\sqztiny Another important capability provided by MDD tools is
advanced model checking, such as Cadena's feature that detects cyclic
call chains and event feedbacks and can be used to reason about the
possible deadlocks that may occur in a concurrent system.  Since all
robot assembly components only interact with the {\tt
Watch\-Setting\-Manager}, any possible cycle must pass through that
component.  Right clicking the {\tt Watch\-Setting\-Manager} component
in the graphical scenario view of Cadena and selecting the ``cycle
check'' feature highlights two components of the assembly -- the {\tt
Human\-Machine\-Interface} and the {\tt Watch\-Setting\-Manager} --
which form a cycle, as shown in
Figure~\ref{fig:modeless_cycle_detect}.
\begin{figure}[htb]
\vspace{-.1in}
\center{\includegraphics[width=3in]{eps/modeless_cycle_detect.eps}}
\vspace{0in}
\bfcaption{Robot Assembly Modeless Cycle Detection in Cadena} 
\label{fig:modeless_cycle_detect}
\vspace{0.1in}
\end{figure}
The cycle detection stops after the first detection, which is why only
two components are highlighted (darker colors) in the figure.  If we
disconnect those two components and repeat the cycle check, however,
other components will be highlighted.  The {\tt
Watch\-Setting\-Manager} affects and is affected by every other
component, so eventually every component is in the downstream path of
every other component in the component assembly.

Since we have at least one cycle we cannot be certain that deadlocks
do not occur.  Deadlocks for such a model are thus ``implementation
defined,'' which means that they might or might not be avoided with a
more sophisticated implementation, {\em e.g.}, one that handles
assumptions that cannot be (or are not) modeled.  The system therefore
cannot be validated from a modeling perspective.  Examining the
production sequence diagram in Figure~\ref{fig:robot_prod_seq} above,
however, clearly shows that no deadlock can occur, at least during the
normal production use case.  This information clashes with the
analysis from Cadena, due to the fact that we have not yet specified
modal information in our components, {\em i.e.}, component operational
modes specifying interactions between input and output ports of the
same component (intra-component interactions).  Specifying modal
information allows a more precise detection of cycles and potential
deadlocks.

For the semantics shown in Figure~\ref{fig:robot_prod_seq}'s
production sequence diagram, most components can remain stateless.  At
least two components require state, however, the {\tt
Watch\-Setting\-Manager} and the {\tt Human\-Machine\-Interface}.  For
the {\tt Watch\-Setting\-Manager}, the sequence diagram in
Figure~\ref{fig:robot_prod_seq} implicitly defines the following seven
states: (1) {\em WaitingWorkOrder}, (2) {\em WaitingAcceptWorkOrder},
(3) {\em WaitingPalletReady}, (4) {\em WaitingProceed}, (5) {\em
WaitingPalletComplete}, (6) {\em WaitingPalletMoved}, and (7) {\em
WaitingProcessingAccepted}.  In each state, no more than one input
port affects an output port, and not all the output ports are affected
(in facts, no more than three are affected for each mode).  The other
input and output ports behave as if they were disconnected.

For the {\tt Human\-Machine\-Interface}, we need to specify that a
{\em DisplayWorkUpdate} cannot trigger an {\em AcceptWorkOrder}.
Otherwise, a feedback cycle with the {\tt Watch\-Setting\-Manager}
will arise.  At least two states are needed, though it is better to
specify all four semantically detectable states: (1) {\em
WaitingNewWorkOrder}, (2) {\em WaitingDisplayWorkUpdate}, (3) {\em
WaitingReadyToProduce}, and (4) {\em
WaitingDisplayProcessingComplete}.

The behaviors of the {\tt Watch\-Setting\-Manager} and the {\tt
Human\-Machine\-Interface} components outlined above can be captured
in the Cadena property specification ({\tt *.cps}) file shown below:

{\footnotesize
\ls{0.8}
\begin{verbatim}
module RobotAssembly {
  component WatchSettingManager {
    mode status of { 
       WaitingWorkOrder,
       WaitingAcceptWorkOrder,
       WaitingPalletReady,
       WaitingProceed,
       WaitingPalletComplete,
       WaitingPalletMoved,
       WaitingProcessingAccepted 
    }
    init status.WaitingWorkOrder;

    dependencydefault: none;
    dependencies {
      case status of {
        WaitingWorkOrder:
          WorkOrder -> Display;
        WaitingAcceptWorkOrder:
          DisplayResponse.WorkOrderResponse -> 
            MovePallet, Display,
            ProductionReport;
        WaitingPalletReady:
          PalletStatus -> ProductionReport;
        WaitingProceed:
          DisplayResponse.ProductionReport ->
            MovePallet;
        WaitingPalletComplete:
          ProcessingStatus -> MovePallet;
        WaitingPalletMoved:
          PalletStatus -> Display;
        WaitingProcessingAccepted:
          DisplayResponse.ProductionReadyResponse -> 
            ProductionReport, MovePallet;
      }
    }
  }
  component HumanMachineInterface
  {
    mode status of
    {
      WaitingNewWorkOrder, 
      WaitingDisplayWorkUpdate, 
      WaitingReadyToProduce, 
      WaitingDisplayProcessingComplete
    }
    init status.WaitingNewWorkOrder;
    dependencydefault: none;
    dependencies {
      case status of {
        WaitingNewWorkOrder:
          WorkDisplayUpdate -> 
            HumanResponse.WorkOrderResponse;
        WaitingDisplayWorkUpdate:
          WorkDisplayUpdate -> ;
        WaitingReadyToProduce:
          WorkDisplayUpdate -> 
            HumanResponse.ProductionReadyResponse;
        WaitingDisplayProcessingComplete:
          WorkDisplayUpdate -> 
            HumanResponse.PalletInspectionResponse;
      }
    }
  }
}
\end{verbatim}}

The Cadena {\tt *.cps} file shown above sets our modal specifications
for the robot assembly project.  The remainder of this section refers
to the modal view of the scenario illustrated in
Figure~\ref{fig:modal_view}.
\begin{figure}[htb]
\vspace{-.1in}
\center{\includegraphics[width=3.4in]{eps/modal_view.eps}}
\vspace{0in}
\bfcaption{Robot Assembly: Modal View in Cadena} 
\label{fig:modal_view}
\vspace{0.1in}
\end{figure}
The two components for which we have defined the states must be set to
a globally consistent state, {\em i.e.}, we cannot set the {\tt
Watch\-Setting\-Manager} in the {\em WaitingPalletComplete} state
while the {\tt Human\-Machine\-Interface} is in the {\em
WaitingNewWorkOrder} state.  We therefore set the {\tt
Watch\-Setting\-Manager} in the {\tt WaitingAcceptWorkOrder} state and
the {\tt Human\-Machine\-Interface} in the {\tt
WaitingDisplayWorkUpdate} state.  As a result, only the connections
that belong to the current mode will be shown (see
Figure~\ref{fig:modal_view}).  Since the cycle analysis will detect
any cycles in any of the modes, the current model can be analyzed to
detect deadlocks.

% Andy please put screenshot of Cadena in Modal view here:
% CadenaModalView_WaitingAcceptWorkOrder_WaitingDisplayWorkUpdate.png

% Dr.Schmidt, Andy: have a look if you want to introduce 
% the following part, which I commented out by default
% It might be interesting, but the readers might ask: 
% how comes that the new cycles are not detected by default but 
% instead I have to introduce a section in the .cps by hand in order to make 
% Cadena detect these....? (and the answer is that there was 
% another way to do the things but it was too long and tedious
% to be put in a bookchapter: e.g. the CPS file would have been 
% at least 3 times longer and there would have been 
% lots of boring details in it, without interesting improvements
% on explaining the concepts of model checking.)

For contrast, we also show a variation of the robot assembly CCM
component assembly that is in fact not deadlock-proof and hence cannot
be validated.  This variation consists of adding the connection from
the {\tt Watch\-Setting\-Manger}/\-{\tt Analysis} receptacle to the
{\tt Robot\-Manager}/{\tt Analysis}
facet.\footnote{Figure~\ref{fig:robot_picml} shows that the following
two CCM ports were already connected: (1) {\tt Robot\-Manager}/{\tt
Circle\-Analysis} receptacle to {\tt Pallet\-Conveyor\-Manager}/{\tt
Circle\-Analysis} facet and (2) {\tt Pallet\-Conveyor\-Manager}/{\tt
Analysis\-Two} receptacle to {\tt Watch\-Setting\-Manager}/{\tt
Analysis\-Two} facet.}  We do not have any semantic or behavioral
specifications for these analysis ports.  We must therefore assume
that (1) operation calls on the facets can affect any analysis
receptacle on the same component and (2) this behavior can happen in
any mode of the three components.  To reflect this scenario we add the
following lines for the {\tt Watch\-Setting\-Manager} into the {\tt
*.cps} file shown below:

{\footnotesize
\ls{0.8}
\begin{verbatim}
    ...
    dependencies {
      AnalysisOne.CallingBackTwo 
                 -> Analysis.CicrleCallOne,
                    Analysis.CallingBackOne;
      AnalysisTwo.CircleCallThree 
                 -> Analysis.CicrleCallOne,
                    Analysis.CallingBackOne;
      case status of 
        ...
     }
\end{verbatim}
} 

The resulting scenario shows a cycle (illustrated in
Figure~\ref{fig:cadena_circle_analysis}) in at least one mode (and in
this particular case, in all the modes).
\begin{figure}[htb]
\vspace{-.1in}
\center{\includegraphics[width=3.4in]{eps/circle_analysis.eps}}
\vspace{0in}
\bfcaption{Robot Assembly: Cadena Model After Circle Analysis} 
\label{fig:cadena_circle_analysis}
\vspace{0.1in}
\end{figure}
Armed with this knowledge, therefore, any deadlock avoidance must be
at the implementation level, {\em i.e.}, this model cannot be
validated against deadlocks without further knowledge of the semantics
at the modal level.

\subsection{Summary of the Robot Assembly Case Study}
This section used a robot assembly application case study we developed
with our colleagues at Lockheed Martin to showcase our integration of
CoSMIC and Cadena.  The case study shows how semantic validation of
models can help detect problems earlier in the software lifecycle,
{\em e.g.}, immediately after the planning of the interfaces, but
before implementing the business logic.  In our experience, early
detection of defects yielded fewer code revisions, lower development
costs, and shorter time to market.  This ``correct by construction''
paradigm and the ongoing checking for human mistakes made by CoSMIC
and Cadena helped ensure proper execution in mission-critical
contexts, where run-time error-detection and debugging alone was
insufficient.

In particular, the CoSMIC PICML MDD tool helped developers formally
define CCM component assemblies, while allowing better visualization
and easier navigation that can be useful to improve design, spot
errors more easily, and in general work at a higher level of
abstraction and be more productive.  The Cadena environment, likewise,
provided powerful analysis and validation features, which were
synergistic with those of PICML.  In Cadena, a relatively
straightforward declarative language was used to define high-level
behavioral specifications for components.  These specifications were
then used for analysis and validation purposes, such as
component-dependencies traversal and ensuring the robot assembly
application was free of deadlocks.


