\documentclass[a4paper,twoside]{report} %11pt,
\usepackage{fullpage} 
%+%\usepackage{a4pasc}
\usepackage[english]{babel} %\usepackage[french]{babel}
\usepackage[T1]{fontenc}   %
\usepackage{amsmath}
\usepackage{amssymb}
\usepackage{epsfig}
\usepackage{xspace}
\usepackage[usenames]{color}
\usepackage{url}
\usepackage{listings}
\usepackage{times}
%\usepackage{ae}
\usepackage{boxedminipage}
%\usepackage{pifont}
\usepackage{multicol}

\usepackage{fancyhdr}
\pagestyle{fancy}
\headheight 14pt \headsep 25pt
%\topmargin -47pt 
%\addtolength{\headheight{\marginparsep}
%\addtolength{\headheight}{\marginparheight}
\lhead[\small\thepage]{\small\rightmark}
\rhead[\small ECONET Workshop 2007]{\small\thepage}
\cfoot{}
%\lhead[\small\thepage]{\small\rightmark}
%\rhead[\small\leftmark]{\small\thepage}
%\lfoot[\small ECONET Project]{\small Workshop at Prague}
%\rfoot[\small Workshop at Prague]{\small ECONET Project}

\definecolor{darkRed}{rgb}{0.65,0,0}
\definecolor{lightGray}{rgb}{.75,.75,.75}
\definecolor{darkBlue}{rgb}{0,.22,.41}
\definecolor{darkGray}{rgb}{.40,.40,.40}
\definecolor{orange}{rgb}{0.97,0.53,0.38}
\RequirePackage[ps2pdf,bookmarks,%
                urlcolor=orange,citecolor=darkRed,linkcolor=darkBlue,%
                breaklinks=true,%pagecolor=darkRed,
                colorlinks,hyperfigures,pdfpagescrop={0 0 595 890}]{hyperref}

\def\repHOME{.}
\def\repFIGURES{\repHOME/FIGURES}

\def\og{"} %not in french
\def\fg{"}
\newcommand{\todecide}[1]{\texttt{+++to decide: #1 +++ \\}}
\def\towrite{\texttt{+++ to write +++ \\}}
\newcommand{\todo}[1]{\texttt{+++ TODO: \textit{#1}  +++ \\}}
\def\kmelia{\textsf{Kmelia}\xspace}
\def\lotos{\textsc{Lotos}\xspace}
\def\kadl{\textsc{Kadl}\xspace}
\def\sofa{\textsc{Sofa}\xspace}

\title{\textcolor{BrickRed}{ECONET Project}~\\
{\sc Prague 2007 - Workshop Report}\\[2ex]
}

\author{\underline{Pascal ANDRE}\thanks{LINA - FRE CNRS 2729- 2, rue de la
Houssini{\`e}re, B.P.92208, F-44322 Nantes Cedex 3, France} \and
Dan CHIOREAN\thanks{Computer Science Research Laboratory,
  Universitatea BABES-BOLYAI
Mihail Kogalniceanu nr. 1 RO- 400084 Cluj-Napoca, Romania} \and
Frantisek PLASIL\thanks{Distributed Systems Research Group,
Charles University, Malostranske nam.25, 11800 Prague 1, Czech
Republic} \and Jean-Claude ROYER\thanks{OBASCO - EMN/INRIA LINA
FRE CNRS 2729, 4, rue Alfred Kastler F - 44307 Nantes cedex 3
France}}

\date{\textcolor{Blue}{2007, 3-7 september}\\[4ex]
{\small \textcolor{Orange}{supported by}}\\[2ex]
{\includegraphics[width=0.22\textwidth]{\repFIGURES/logoEgide.eps}}
}

%Laboratorul de Cercetare Stiintifica In Informatica
%Praha Ceská Republika

\begin{document}
\maketitle

\section*{Executive Summary}

An Egide-sponsored workshop was held at the Department of Software Engineering of Charles University in Prague.
This workshop was the first one of the ECONET Project Nr \texttt{16293RG}
entitled, "\textcolor{BrickRed}{Behaviour Abstraction from Code, 
{\small Filling the Gap between Component Specification and Implementation}}".

The workshop was convened in response to the objectives of the first year of the project plan which are remind here
  \begin{itemize}
  \item Determination the field of application (boundaries of Java concepts and idioms).
  \item Settings of the major principles to abstract behaviours for software components (into \kmelia, SOFA and STS) from Java code.
  \item Experimentations on existing code.
  \item Studying and proposing a pattern for annotating EJB components in order to better support RE (behavior abstraction from code).
  \item Integration of the verification of guards using OCL (and OCLE).
  \item Documentation, research report and workshop
preparation.
  \end{itemize}
More precisely, the aims of the workshop were (1) to improve the knowledge of the participants on each other activity and background, and (2) to take concerted decisions on the project issues (concrete objectives, tasks, organisation, responsabilities, deliveries, planning...).

On these points the workshop was a satisfactory step in the project, thanks to the participant motivation. 
The following issues have been discussed: detailed competences of each participant on the project topics, comparison of component models and development approaches, concrete objectives of the project, selection of the kind of code to be abstracted, shared techniques and tools, common benchmark, etc.
The working sessions enabled (1) to establish a common and shared concrete vision of the project, (2) to delimit the project objectives and context (nature of the Java code, benchmark, subset of the abstract models),
(3) to divide the project into parts, which are easier to handle,
(4) the definition and repartition of individual tasks.

A project architecture was drawn after fruitful exchanges accompanied with the definition of tasks, with balanced responsabilities and partnerships.
This projects includes three distinct but complementary parts:
  \begin{itemize}
  \item Structural Abstraction from Java Code.
  \item Behavioural Abstraction from Java Code.
  \item Metamodel Definition and Consistency Verification.
  \end{itemize}
Each part (subproject) constitute a challenge since there are ongoing research on it. 
Interfaces between the parts have been roughly defined.
A common benchmark has been proposed to avoid support mismatch.

A key recommendation from the workshop is that the participants should tackle the objectives in a limited (but extensible) context in order the produce results in a 2-year project. Nevertheless a contribution on the fields is expected.
A secondary recommendation from the workshop is to pursue a cross fertilisation on the abstract component models and metamodels.

The workshop concluded by some guidelines to the next workshop that should hold in Nantes in the beginning of 2008.
~\\

This report relates what happened in the workshop.

~\\[2ex]

\paragraph{Acknowledgements}
The participants would like to thank Egide for its
financial support of this workshop.

%\begin{abstract}
%This report summarises the 
%\end{abstract}

\tableofcontents

\chapter{Introduction}
\label{introduction}
\input{introduction}


\chapter{Workshop Sessions}
\label{sessions}
%\input{sessions}

This chapter collects the main events and informations of the workshop sessions.
We first begin by the presentation sessions where the participants present themselves, their team and technical contributions (section \ref{presentation_sessions}).
Then we summarise in section \ref{working_sessions} the contributions of the working sessions where the  participants discussed on the project (issues, structure, tasks, technical aspects, tools...).

The detailed program is given on the wiki at:

\small
\textcolor{BrickRed}{\url{http://www.lina.sciences.univ-nantes.fr/coloss/wiki/doku.php?id=econet:}\\
\indent\url{pragues2007:program07}}
\normalsize

The slides, pictures and discussions are stored on the wiki at:

\small
\textcolor{BrickRed}{\url{http://www.lina.sciences.univ-nantes.fr/coloss/wiki/doku.php?id=econet:}\\
\indent\url{pragues2007:materials}}
\normalsize

\section{Team and Technical Presentation Sessions}
\label{presentation_sessions}
\input{psessions}

\section{Working Session}
\label{working_sessions}
\input{wsessions}

\chapter{Project Architecture}
\label{architecture}

The contents of this chapter has been defined individually after the workshop.
It presents a detailed vision of the three subprojects, defined in the workshop.
There remain some coordination to process on the common parts (especially on the interface formats and model tools) and also to share the experience on tools.

\section{Structural Abstraction Subproject}
\label{structural}
\input{structural}

\section{Behavioural Abstraction Subproject}
\label{behavioural}
\input{behavioural}

\section{Metamodel Abstraction Subproject}
\label{metamodel}
\input{metamodel}

\section{Common Tools}

Several tools will be used in more than one subproject.

\begin{enumerate}
%\begin{thebibliography}{99}
 \bibitem{JavaCC}JavaCC, \url{https://javacc.dev.java.net/}
 \bibitem{JavaC}Java Development Kit, \url{http://java.sun.com/}
 \bibitem{ANTLR}ANTLR, \url{http://www.antlr.org/}
 \bibitem{JavaCUP}Java CUP, \url{http://www2.cs.tum.edu/projects/cup/}
 \bibitem{SableCC}SableCC, \url{http://sablecc.org/}
%\end{thebibliography}
\end{enumerate}

\chapter{Conclusion}
\label{conclusion}
\input{conclusion}

\appendix 

\chapter{More informations on...}

\textit{see the Project Wiki.} 

\section{Workshop Material}

Most of the elements are on the project and workshop Wiki.

\section{Collaborative Tools}

Some collaborative tools have been installed to exchange documents.

\begin{itemize}
    \item Wiki \\
\url{http://www.lina.sciences.univ-nantes.fr/coloss/wiki/doku.php?id=econet:start}\\
For storing documents, discussions...
    \item CVS \\
\url{http://www.ksi.mff.cuni.cz/??cvs??/}\\
    \item CoCoME \\
\url{http://agrausch.informatik.uni-kl.de/CoCoME}\\
\url{http://www.cocome.org/}\\
%   \item Wiki \url{}\\
\end{itemize}


\section{Annotated Bibliography}
\label{annotedBib}
\input{annotedBib}

%see the Project Wiki.

\nocite{dsrg:PP06aa,general:CCG+04,bandera00,general:CGJ+00,general:Eis05,general:CKS+04,general:BR02,general:BCM+06}
%\bibitem[CDH+00]{general:CDH+00}
%= bandera00

\bibliographystyle{alpha}
\bibliography{econet_reverse}

\begin{enumerate}

\bibitem[PP06a]{dsrg:PP06aa}
Pavel Parizek and Frantisek Plasil.
\newblock {Modeling Environment for Component Model Checking from Hierarchical Architecture}. In
\newblock {\em Proceedings of Formal Aspects of Component Software (FACS'06)}, Prague, Czech Republic, September 20-22, 2006, ENTCS, Sep 2006.


\bibitem[CCG+04]{general:CCG+04}
Sagar Chaki, Edmund M. Clarke, Alex Groce, Somesh Jha, and Helmut Veith.
\newblock {Modular Verification of Software Components in C}. In
\newblock {\em IEEE Transactions on Software Engineering}, 30(6), June 2004.

\bibitem[CGJ+00]{general:CGJ+00}
Edmund M. Clarke, Orna Grumberg, Somesh Jha, Yuan Lu, and Helmut Veith.
\newblock {Counterexample-guided abstraction refinement}. In
\newblock {\em Computer Aided Verification}, pages 154--169, 2000.

\bibitem[Eis05]{general:Eis05}
Cindy Eisner.
\newblock {Formal verification of software source code through semi-automatic modeling}. In
\newblock {\em Software and System Modeling}, 4(1): 14--31, 2005.

\end{enumerate}


\listoffigures
\end{document}

\appendix 
\chapter{Workshop Material}
\section{Team and Technical Presentations}
\section{Working Sessions}
\section{Collaborative Tools}
\chapter{Annotated Bibliography}

\bibitem[CKS+04]{general:CKS+04}
Edmund M. Clarke, Dalien Kroening, Natasha Sharygina, and Karen Yorav.
\newblock {Predicate Abstraction of ANSI--C Programs using SAT}. In
\newblock {\em Formal Methods in System Design (FMSD)}, pages 105--127, vol. 25, 2004.

\bibitem[BR02]{general:BR02}
Thomas Ball and Sriram K. Rajamani.
\newblock {The SLAM Project: Debugging System Software via Static Analysis}. In
\newblock {\em POPL 2002}, ACM, Jan 2002.

\bibitem[BCM+06]{general:BCM+06}
Tomas Barros, Ludovic Henrio and Eric Madelaine.
\newblock {Model-Checking Distributed Components: The Vercors Platform}. In
\newblock {\em Proceedings of Formal Aspects of Component Software (FACS'06)}, Prague, Czech Republic, September 20-22, 2006, ENTCS, Sep 2006.

