%**************************************************************************
%*
%*  Paper: ``INSTRUCTIONS FOR AUTHORS OF LATEX (Poster) ABSTRACTS''
%*
%*  Publication: 2011 Winter Simulation Conference Author Kit
%*
%*  Filename: wsc11poster.tex
%*
%*      DATE: Feb 08, 2011 to become the primary WSC'11 LaTeX file
%*
%*  Word Processing System: TeXnicCenter and MiKTeX
%*
%*
%*  All files need the following
\input{wsc13style.tex}     % download from author kit.  Style files for wsc formatting

\documentclass{wscposterproc}
\usepackage{latexsym}
%\usepackage{caption}
\usepackage{graphicx}
\usepackage{mathptmx}

%
%****************************************************************************
% AUTHOR: You may want to use some of these packages. (Optional)
\usepackage{amsmath}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{amsbsy}
\usepackage{amsthm}
%****************************************************************************


%
%****************************************************************************
% AUTHOR: If you do not wish to use hyperlinks, then just comment
% out the hyperref usepackage commands below.

%% This version of the command is used if you use pdflatex. In this case you
%% cannot use ps or eps files for graphics, but pdf, jpeg, png etc are fine.

\usepackage[pdftex,colorlinks=true,urlcolor=blue,citecolor=black,anchorcolor=black,linkcolor=black]{hyperref}

%% The next versions of the hyperref command are used if you adopt the
%% traditional latex-dvips-ps2pdf route in generating your pdf file. In
%% this case you can use ps or eps files for graphics, but not pdf, jpeg, png etc.
%% If you are using WinEdt or PCTeX, then use the following. If you are using
%% Y&Y TeX then replace "dvips" with "dvipsone"

%%\usepackage[dvips,colorlinks=true,urlcolor=blue,citecolor=black,%
%% anchorcolor=black,linkcolor=black]{hyperref}
%****************************************************************************



%****************************************************************************
% AUTHOR: You may need to use the following command to adjust the space on the title page
% to properly list all authors.
% Please use: 2.5in for 1 row of authors, 3.75in [default] for 2 rows of authors
%\setlength{\titlevboxsize}{2.5in}  % 2.5in for 1 row of authors, 3.75in for 2 rows of authors
%****************************************************************************


%
%****************************************************************************
%*
%* AUTHOR: YOUR CALL!  Document-specific macros can come here.
%*
%****************************************************************************


%#########################################################
%*
%*  The Document.
%*
\begin{document}

%***************************************************************************
% AUTHOR: AUTHOR NAMES GO HERE
% FORMAT AUTHORS NAMES Like: Author1, Author2 and Author3 (last names)
%
%       You need to change the author listing below!
%               Please list ALL authors using last name only, separate by a comma except
%               for the last author, separate with "and"
%
% These names will be used from the 2nd page on - thus for one page abstracts this can stay as it is.
% DON'T REMOVE THIS LINE!
%
\WSCpagesetup{Antonenko, Chemeritsky, Glonina, Konnov, Pashkov,
Podymov, Savenkov, Smeliansky, Volkanov, Zakharov, and Zorin}

% AUTHOR: Enter the title, all letters in upper case
\title{DYANA: HLA-BASED DISTRIBUTED REAL-TIME EMBEDDED SYSTEMS SIMULATION TOOL}


\author{\itshape
Vitaly A. Antonenko$^\star$, Evgeny V. Chemeritskiy$^\star$,
Alevtina B. Glonina$^\star$, Igor V. Konnov$^{\star\star}$,
Vasily N. Pashkov$^\star$, \\
Vladislav V. Podymov$^\star$, Konstantin O. Savenkov$^\star$, Ruslan
L. Smeliansky$^\star$,
Dmitry Yu. Volkanov$^\star$, \\
Vladimir A. Zakharov$^\star$,
Daniil A. Zorin$^\star$\\[12pt]
\itshape$^\star$Lomonosov Moscow State University, Moscow, Russia \\
\itshape$^{\star\star}$Technische Universität Wien, Wien, Austria }

\maketitle

\section*{ABSTRACT}
In this paper we present DYANA, an HLA-based hardware-in-the-loop
simulation tool. This tool is used for distributed Real-Time and
Embedded Systems (RTES) simulation. RTES models are described by
Unified Modeling Language (UML) statechart diagrams. The statechart
diagram is transformed into a Network of Timed Automata (NTA). After
translation into NTA we use UPPAAL for RTES model verification. The
statechart diagram is also transformed into HLA-based Simulation
Model (HSM). After translation into HSM we use CERTI as the
simulation runtime.


%\begin{center}
\section{DYANA OVERVIEW}
%\end{center}

Development of embedded devices and of the RTES itself is a
distributed process performed by several teams located in different
organizations. The tool which support this process is needed. In
this paper we present DYANA, a tool for simulation and verification
of RTES. This tool is a new revision of DYANA simulation
environment~\cite{num1}. The key features of DYANA are UML
statecharts as the modeling language for RTES, using one notation
for simulation and verification, checking the Worst Case Execution
Time (WCET) by invoking the analysis tool Metamoc, using of OTF
trace format for execution traces of models run in CERTI.

Figure~\ref{fig:blocks2} shows the main components of DYANA:

\begin{figure}[htb]
{
\centering
\includegraphics[width=280pt]{blocks2.pdf}
\caption{DYANA components \label{fig:blocks2}}
}
\end{figure}

DYANA provides a specialized model development environment with a
number of integrated services. Rectangles without background mark
the tools that were integrated into DYANA as-is, rectangles with
light background are modified tools and rectangles with dark
background represent the tools developed specifically for DYANA.

ArgoUML is the UML editor used to create the models of real-time
systems. Models are defined as UML statecharts. The models are saved
to XMI format, so technically any UML editor that supports XMI can
be used instead of ArgoUML.

UPPAAL is a verification tool. UML statecharts can be converted to
UPPAAL format automatically in IDE. Correctness of this conversion
showed in ~\cite{num2}. During the conversion, WCET can be computed
using Metamoc tool.

CERTI is the runtime for the real-time models. DYANA uses the
modified multi-thread version of CERTI, different from the version
on the trunk in the repository. UML models are automatically translated
to HLA federates via the IDE. Execution traces of models run in
CERTI can be visualized in Vis4.

RAP tool is a tool for solving Realibility Allocation Problem for
RTES~\cite{num4}. Our RAP tool supports such methods as Evolutionary
Algorithm, Simulation Annealing and Greedy Algorithm.

\section{DYANA WORKFLOW}

The way DYANA can be used for design of RTES can be illustrated by
the following example. Suppose a flight controller
system~\cite{num5} is under development, the whole code is not
available yet, but the subsystem responsible for interprocessor
communication and fault tolerance is ready. Then the general model
can be simplified to include only the part relevant to the analysed
subsystem. The resulting UML diagram is loaded in DYANA and
converted to a net of UPPAAL timed automata. Then the safety and
liveness properties of the system can be verified with UPPAAL
checker.

If the checker finds a counterexample, the corresponding UPPAAL
trace can be converted to a trace showing transitions in the
original UML statechart. Using this trace, it is possible to modify
the model to make it reproduce this trace every time. Then the model
is converted to a set of federates in C++ and simulated in CERTI.
The trace can be visualized in Vis4 to help the developers
understand the problem discovered by the model checker.

\section{FUTURE WORK}

Directions for future research include :

\begin{itemize}
  \item More thorough exploration of the proposed tool on data from real
avionics systems.
  \item More strong cooperation between simulation and verification inside
  DYANA.
  \item Support HLA-based Hardware-In-The-Loop Simulation(HILS)
  \item Creation of tool for automate scaling of models for preparation for using of verification.
  \item Creation of tool for automate processing of simulation
experiments  results.
\end{itemize}


% Please don't exchange the bibliographystyle style
\bibliographystyle{wsc}
% AUTHOR: Include your bib file here
\bibliography{wsc13bib}

\end{document}
