% Project: ECONET 
% Document: Prague07 Workshop Report
% Last writer: Andre Pascal 
% creation: 14/09/07 
% modification PA 02/10/07 
% *********************************** 
%\chapter{Workshop Sessions}
%\label{sessions}
%\input{sessions}
%\section{Working Session}
%\label{working_sessions}
%\input{wsession}

\subsection{Introduction}

The goals of the working sessions are mainly to fix a battle plan for the project.
This means to clarify and delimit the detailed objectives in a feasible manner,
to define clearly the concrete and coordinated contribution of each partner,
to define task, products and results,
to organise tasks (responsabilities, contributors, schedule...).
One first issue was to check that each partner has a compatible (or even better the same) vision of the project.
Another one is to structure the work in several parts because a monolithic task cannot be realised by four geographically separated entities.

These sessions are highly dynamic so that a strict program was not established.
Thus the detailed program given in the following subsections are post-workshop programs.
Nevertheless the initial program covering included three aspects for the working session
\begin{itemize}
    \item 
decision on the source and target area boundaries
    \item 
discussions on the way to get reverse transformations
    \item 
find application examples
\end{itemize}
In the following we will summary the session contents day by day.

\subsection{Wednesday, September 5, 2007}

This is a half-day session.

\begin{center}
\begin{tabular}{||c|l|l||}
\hline
\textbf{Time} & \textbf{Activity} & \textbf{Speaker}\\
\hline
\hline
09:00 & Introduction to the working sessions & Pascal André\\
\cline{2-3}
$|$ & LCI Point of view & Dan Chiorean\\
\cline{2-3}
$|$ & DSRG Point of view & Frantisek Plasil\\
\cline{2-3}
12:00 & Round tables and discussions & all\\
\hline
\end{tabular}
\end{center}

\subsubsection{Introduction to the working sessions}
\label{ws:intro:pa}

The slides of this (first plan) introduction are provided on the Workshop Wiki at:\\
\small
\textcolor{BrickRed}{\url{http://www.lina.sciences.univ-nantes.fr/coloss/wiki/doku.php?id=econet:pragues2007:}\\ \url{program07}}
\normalsize

Pascal introduced the working session by giving its view of the current project situation and provided some tracks for the discussions.
Consequently the Working Session Roadmap was organised around four points
\begin{enumerate}
\item Convergence on the objectives
\item Convergence on the means
\item Definition of the tasks
\item Production
\end{enumerate}
The three first points define an initial objective for each day of the working session.

\paragraph{1- Convergence on the objectives}~\\

There is a clear agreement on the "abstract" context
\begin{enumerate}
\item We have abstract component models (\sofa, \kmelia, \kadl) and tools.
Some have elements for Java code generation (engineering).
\item We assume Java Code Specifications and Programs.
This code contains informations about structure and behaviours (even if it was not designed in a CBSE).
\item We want to practice Reverse Engineering = from code to abstract models.
There exist general techniques and tools such as code analysers, patterns, extractors...
\end{enumerate}

\begin{figure}[ht]
\centerline{\epsfig{figure=\repFIGURES/archiEco1.eps,width=12cm}}
\caption{ECONET Project: "abstract" context}%[archiEco1]
\label{archiEco1}
\end{figure}

There is a fuzzy vision of the "concrete" context.

\begin{itemize}
\item What sort of Java code nature do we want to process ?
\begin{itemize}
\item Bytecode - the one that exists at run-time.
\item Plain source - the one usable for an open source project.
\item Annoted Source - a Java program (source or compiled) that includes informations usable for connecting to an abstract model.
This is the case when the program is (aprtially) generated from a component abstract specification by some code generator.
\end{itemize}
\item Assuming we have a Java program, does its code be structured in some way ?
\begin{itemize}
\item plain Java: there are no special structure.
\item "componentised" Java (EJB, Corba, .NET, issued from a code generator - SOFA, Fractal...): the code has a component flavour.
\item "behavioural" Java (threads, communication primitives, issued from a code generator...): the code has a behaviour flavour.
\end{itemize}
\item What are the reengineering issues ? It means toward what objective do we look for abstractions ?
\begin{itemize}
\item legacy code recovery/discovery: the usual goal of reverse-engineering.
You have an existing code but it was not designed according to the same abstract concepts.
\item compare code and specifications (conformance): 
we want to check whether a concrete representation and an abstract representation (of the same system !) are consistent.
\item roundtrip: the code is generated from a model and complete that model.
The development process includes engineering and reverse-engineering activities.
This approach is frequent in MDA.
\item ...
\end{itemize}
\end{itemize}

\textcolor{red}{Goal of day 3 = Clear agreement on the "concrete" context}

\paragraph{2- Convergence on the means}~\\

Once we agree on the right objectives, the question is how can we reach them.

\begin{itemize}
\item Collaborative State of the Art Study.\\
The idea here is to share the individual experiences both on domains and tools in order to accelerate the collaborative work.
The state of the art covers works and tools related to:
reverse engineering (in general, for components), java reverse engineering, Java code manipulation (analysis, annotation, extraction...).
\item Re-engineering techniques.\\
The objective is to be up-to-date in techniques available in the open source community.
\begin{itemize}
\item Java Compilers and Analysers to handle the Java code.
\item Patterns, rule based systems for reverse-engineering issues.
\item Used notations and Intermediate layers (models) for a step-by-step process.
\item ...
\end{itemize}
\item Separate modules (e.g. structural / behavioural / metamodels).
Do we work on separate parts and levels with different applications or shall we use one program only ?
Do we propose a framework for general purpose or do we design a single purpose application ?
\item Benchmark example.\\
It is quite difficult to find Java code related to components.
A collaborative work imlies that we work together on the same Java program.
\end{itemize}
We also have experience on OCL and metamodels.

\textcolor{red}{(optimistic) Goal of day 4 = organise the means tracks and find the benchmark}

\paragraph{3- Definition of the tasks}~\\

Once we agree on the right objectives and we have a somewhat clear idea of the means we provide, the question is to organise the work \textit{i.e.} the project management.

\begin{itemize}
\item What to do ? \\
Define a list of tasks to do and the delivery.
\item Contributions ? \\
Define the actors and collaborations (who do what).
\item Synchronisation points \\
Point out the botlenecks of the process.
\item Planning \\
Define who do what and when.
\item ...
\end{itemize}

\textcolor{red}{(optimistic) Goal of day 5 = each participant has a somewhat clear idea of what he will do}

\paragraph{4- Production}~\\

Here are some guidelines for that part.

\begin{itemize}
\item Workshop Report
\begin{itemize}
\item Collect paper and slides 
\item Summary of the discussions
\end{itemize}
\item[+] Bibliographical Notes\\
\item[$\implies$] \textcolor{BrickRed}{project plan for year 2 and
 \textit{Evaluation}}\\
\item Fix the participants objectives
\item Documentation, research reports
\item Intermediate results $\implies$ Second Workshop
\item \textcolor{darkGray}{Publications (?)}
\end{itemize}

\textcolor{red}{These are also part of the initial 'Second year objectives'}

\subsubsection{LCI Point of view}

Dan talked about various aspects of reverse engineering and especially those related to models (MDA).
Reverse engineering is about finding the concepts of the models by analysing the code and inject the model.
There are several models: the programming language (Java) model, the component models.
He stressed three aspects:
\begin{enumerate}
    \item About reverse engineering (RE).\\
He expects a more clear defintion of the context and goals.
The domain is quite difficult and unexplored.
There are different programming languages (Eiffel, C++, Java...) and different tools.
There are some existing work on the subjet, we should have a look at them.
He worried about the practical result of Component RE (the value of RE, the mandatory results).
Do \sofa applications have non-\sofa parts.
    \item About Behaviour Checking.\\
Do we want to detect possible deadlocks in the code ?
What can we do if component instances relate to the same component type.
    \item About per/post conditions.\\
This information is rarely present with a clear format in programs (even for java assertions).
\end{enumerate}

Dan also noticed that most tools work with the architecture of the application.
He also remind that LCI had a previous experience with reverse-engineering UML from C++ programs.
 
\subsubsection{DSRG Point of view}

The slides of this intervention are provided on the Workshop Wiki at:\\
\small
\textcolor{BrickRed}{\url{http://www.lina.sciences.univ-nantes.fr/coloss/wiki/doku.php?id=econet:pragues2007:}\\ \url{program07}}
\normalsize

Frantisek recalls that the ECONET project is a small project (budget, duration).
He commented the initial project definition (see section \ref{econet:project}).
As a general remark he recalled that the pragmatic outputs of the project are a cross fertilization and joint publications. 

He distinguished four area of contribution by DSRG are:
\begin{enumerate}
    \item Providing \sofa.\\
\textcolor{lightGray}{This is one of the abstract models. Providing covers the language definition, the tool support, examples, the knowledge.}.
    \item Enhancing EBP by additional features from STS/eLTS (to enhance expressive power of EBP).
\textcolor{lightGray}{The idea is to take concepts from other abstract models.}.
    \item Extracting protocols (EBP) from code  (at least BP from code).
\textcolor{lightGray}{This is a part of the reverse engineering if we consider that there are two complementary aspects in a program: the structure and the behaviour.}.
    \item OCL: WFR (well-formed rules) for component diagrams, activity diagrams? WFR for \sofa components,
\textcolor{lightGray}{The idea is to improve the \sofa language definition using the LCI experience.}.
\end{enumerate}
Note that point 2 and 4 are indirectly related to reverse-engineering but can participate to define a more general framework.

Frantisek brings an answer to one of the \textit{means} issues: the benchmark.
He proposes to take an exemple from a previous work on a Dagstuhl Modelling Contest, the \textcolor{darkGray}{CoCoME (Common Component Modelling Example)}
\url{http://www.cocome.org/}
The advantage is to benefit from a Java program that implements a component application (this is rare enough to have both a specification and a program)
and two abstract models that have been manully built on it.
Two trivial examples are more fruitful.

\subsubsection{Discussions}

The discussions took place from the three above interventions.

%++ recup gilles ideas wiki ++*
Here are some Gilles's random ideas:
\begin{enumerate}
    \item We're interested in behavior models.
	\begin{enumerate}
    \item Getting them from plain java code without structural information about the component architecture is far beyond the scope of this project.
    \item We at least need some kind of "boundaries".
	\end{enumerate}
    \item There are two first steps :
	\begin{enumerate}
    \item Our benchmarks shouldn't be spagetthi code (while not sticking to a particular comp model, the application should have a something that look like a component architecture). A proposed task is finding fitting benchmarks.
    \item Then let's pretend we already got most of the structural info about the component architecture (Manually, Automatically from Specification or code...).
	\end{enumerate}
    \item We're about to target different abstract models.
	\begin{enumerate}
    \item We need meta information somehow common to the models : a minimal structural component model (component hierarchy, one or several interfaces by component). A proposed task is finding this minimal meta information.
We don't need a Unified Component Language -just the minimal stuff to work (remember the size of the project).
    \item Additional model-specific meta information (because we might want to do something beyond this project's scope some day).
	\end{enumerate}
\end{enumerate}
Annotations examples

\footnotesize
\begin{verbatim}
code source part (class, package, method, whatever..)  "is part of componet id #12344" 
code source part (class, package, method, whatever..)  "is part of interface id #12344" 
\end{verbatim} 
\normalsize

Here is a short summary.

\begin{itemize}
    \item \textcolor{BrickRed}{Benchmark}\\
The CoCoME benchmark is adopted.
It has many interest: existing informations on requirements, on component design, available Java program.
    \item \textcolor{BrickRed}{Input}\\
Of course the fine input would be a component program but it does not exist yet.
A better input is an object program with informations (commments, annotations) on components.
Again it does not exist yet.
We decidede that the input is a plain source Java with possible annotations or informations (comments, separate documentation files, UML models...).
Having a source code allow to use parsers, extraction techniques, comments and various informations that are not available for java bytecode.
These annotations and/or informations should inform on some component abstractions.
We are not sure to find such informations but we assume that as soon as component design will be applied (later), it will help to inject annotations in the plain Java code.\\
A practical question remains: which informations or annotations do we need ?
    \item \textcolor{BrickRed}{Input Model}\\
We do not want to have a instantiated model of the Java programs \textit{i.e.} we carry only some informations of the program not all of them (no model transformation for instance).
    \item \textcolor{BrickRed}{Reverse engineering goal}\\
The goal is to find abstractions than realise full reverse engineering.
The abstraction help to analyse some properties of the program, to get an abstract model, either to compare with an existing one (conformance) or to document the application.
%abstraction rather than full reverse engineering
%compare code and specifications (conformance)
    \item \textcolor{BrickRed}{Separation of concerns}\\
We discussed about two main problem issues: structure/behaviour, one or more target.
	\begin{itemize}
    \item We distingues the structural informations from the behavioural ones.
Both aspects are orthogonal and existing works mainly relate to one aspect only.
Moreover finding the behavioural abstractions depends on both the Java code and the structural model.
The structural part is at first a delimitation of what are the components in the Java code.
    \item We may want to target several abstract model. Shall we implement a tool for each of them or try to share both procedure and knowledge.
Note that some of these model can have only structural features.
One way to proceed is to use metamodels (pending issues to be studied on thursday).
	\end{itemize}
This separation of concerns also make it easy to split the project realisation.
    \item \textcolor{BrickRed}{Background}\\
Other contributions of the project are recalled: cross LTS extensions, WFR definitions.
\end{itemize}

\subsection{Thursday, September 6, 2007}

\begin{center}
\begin{tabular}{||c|l|l||}
\hline
\textbf{Time} & \textbf{Activity} & \textbf{Speaker}\\
\hline
\hline
09:00 & Welcome & Pascal André\\
\cline{2-3}
$|$ & CoCoME Contest & Jan Kofron\\
\cline{2-3}
$|$ & "ECONET tasks" proposal & Petr Hnetynka\\
\cline{2-3}
$|$ & CoCoME in \sofa 2.0 & Jan Kofron\\
\cline{2-3}
12:00 & Round tables and discussions & -\\
\hline
\hline
13:30 & Java Path Finder, Bandera & Jiri Adamek\\
\cline{2-3}
$|$ & Project modules and interfaces (discussions) & - \\
\cline{2-3}
17:00  & Toward an annotation language (discussions) & -\\
\hline
\end{tabular}
\end{center}

\subsubsection{Welcome}
 
Pascal introduced the second day working session by giving an abstract of the
discussions and the gainful decisions of the first day.
Since the goal of day 3 were roughly reached we can now fight the ones of day 4, which are convergence of the means (see section \ref{ws:intro:pa})
and especially try to advance on the input format, the benchmark and the available techniques.
To this end a presentation of the benchmark has been planned in the morning and another one on Java Path Finder (and Bandera) in the afternoon.
The rest of the day (morning and afternoon) is reserved for discussions.

The slides (second plan) are provided on the Workshop Wiki at:\\
\small
\textcolor{BrickRed}{\url{http://www.lina.sciences.univ-nantes.fr/coloss/wiki/doku.php?id=econet:pragues2007:}\\ \url{program07}}
\normalsize

\subsubsection{CoCoME Contest}

Jan Kofron presented Common Component Modeling Example contest.

CoCoME \url{http://agrausch.informatik.uni-kl.de/CoCoME} is an international contest aiming at comparison of different modeling approaches on a common assignment organized by Technische Universität Clausthal, Universität Karlsruhe, Politecnico di Milano, Charles University in Prague. Sharing a common close-to-real-life assignment should reveal strengths and weaknesses of the different modeling approaches and thoroughly test their applicability in practice. 

The assignment is a trading system, a Business application for managing chain of stores with about 200 stores and 8 cash desks per store.
Participants had as input a partial specification via UML, informal specifications as use-cases for the requirements, deployment diagrams for the distribution and a reference implementation (realised by a teacher and students).

The workshop held at Dagstuhl in Germany.
Eighteen teams were involved in that contest.
The objectives was to model the application on various aspects (structure, deployment, behaviour modelling extends behaviour protocols).
Note that Uml models were not fully consistent with the code and the components were given.

The slides of this intervention are provided on the Workshop Wiki at:\\
\small
\textcolor{BrickRed}{\url{http://www.lina.sciences.univ-nantes.fr/coloss/wiki/doku.php?id=econet:pragues2007:}\\ \url{program07}}
\normalsize

\subsubsection{"ECONET tasks" proposal}

Petr Hnetynka proposed some answers to pending questions on the objectives and the means.

To the question "What is an input?" his answer is "plain Java".

For obtaining a behavior specification we need also a model (i.e. architecture).
To the question "How to obtain model?" his answer is "it is already given or we extract it from the plain Java sources.

We need a single concrete meta-model (for specifying models).
The problem is that each component system has its own means for specifying models but most of component systems are similar (black-box component, provided/require services, nesting), thus we can use the core of the SOFA 2 meta-model as a concrete meta-model.

In advance to the objectives of the day he also proposed a first task assignment proposal: model extraction (-?) and behavior specification extraction (DSRG).

The slides of this intervention are provided on the Workshop Wiki at:\\
\small
\textcolor{BrickRed}{\url{http://www.lina.sciences.univ-nantes.fr/coloss/wiki/doku.php?id=econet:pragues2007:}\\ \url{program07}}
\normalsize

\subsubsection{CoCoME in \sofa 2.0}

Back to the CoCoME, Jan Kofron overviewed a \sofa solution for the Common Component Modeling Example. He skipped the \sofa 2.0 presentation to focus on the general design solution and the verification of a part of the system.

The following summarizes modeling of the CoCoME assignment using SOFA 2.0.
\begin{itemize}
    \item Architecture\\
First, the SOFA architecture of the TradingSystem (Fig. \ref{ecoSofaReconst}) was created,
forming basis for further work.
    \item Behavior modeling\\
All CoCoME components were specified using EBP.
Parts of the CoCoME assignment are ambiguous and even contradictory ;
the behavior specification is mainly based on the reference implementation. 
    \item Verification\\
Checking communication of components for errors (Bad-activity no-activity (deadlock) infinite-activity),
Compliance checking (Translation of EBP specification into Promela
using the SPIN model checker to search the state space),\\
Code checking (Via combining Java PathFinder with Behavior Protocol Checker).
    \item Performance
\end{itemize}

\begin{figure}[ht]
\centerline{\epsfig{figure=\repFIGURES/cocomeSofa.eps,width=12cm}}
\caption{CoCoME: Sofa static architecture}%[ecoSofaReconst]
\label{ecoSofaReconst}
\end{figure}

Benefits :
As SOFA 2.0 explicitly supports components throughout the entire software lifecomponent cycle, the architecture erosion is mitigated. Moreover automatic connector generation provides seamless component distribution. Behavioral modeling via EBP and subsequent verification allows for reasoning about correctness of the design even before actually having an implementation. Then with the implementation available, one  can use code checking to find out, whether the implementation obeys its EBP specification.

The solution involves (i) modeling architecture in SOFA meta-model, (ii) specification
of component behavior via extended behavior protocols, (iii) checking
behavior compliance of components, (iv) verification of correspondence between
selected component Java code and behavior specification, (v) deployment
to SOFA run-time environment (using connectors that support RMI and
JMS), and (vi) modeling of performance and resource usage via layered queuing
networks. We faced several issues during implementation of the CoCoME
assignment in SOFA 2.0. Most notably, the architecture was modified in order
to improve clarity of the design – in particular, the hierarchical bus was replaced
by two separate buses and the Inventory component was restructured.
Extended behavior protocols for all the components are based on the provided
plain-English use cases, the UML sequence diagrams, and the reference Java
implementation (the assignment does not include a complete UML behavior
specification e.g. via activity diagrams and state charts).

Jan showed the SOFA solution for CoCoME:
static view, behavior view (BP [sofa, fractal], EBP [Sofa 2.0]),
deployment view,
performance view (model performance),
comparison with UML,
flat / hierarchical models,
multiplicity,
evaluation.

The slides of this intervention are provided on the Workshop Wiki at:\\
\small
\textcolor{BrickRed}{\url{http://www.lina.sciences.univ-nantes.fr/coloss/wiki/doku.php?id=econet:pragues2007:}\\ \url{program07}}
\normalsize

\subsubsection{Morning Discussions}

Here is a short summary of thursday discussions and decisions.

Petr drew a quick picture of a Sofa metamodel (Fig. \ref{sofaMeta}) which should correspond to all our component models (with different names).

\begin{figure}[ht]
\centerline{\epsfig{figure=\repFIGURES/sofaMeta.eps,width=10cm}}
\caption{Sofa: short metamodel}%[sofaMeta]
\label{sofaMeta}
\end{figure}

\newpage
Then we discussed about the application design 
(Fig. \ref{archiEcoTaskV0}).
This figure shows a three parts architecture with a common metamodel and a dependency between structural and behavioural abstraction.
The contribution is an annotation definition, a first prototype (Java analyser, xDoclet) that must be incremental.
See also Spring anf Fractal.

\begin{figure}[ht]
\centerline{\epsfig{figure=\repFIGURES/archiEcoTaskV0.eps,width=12cm}}
\caption{Econet Architecture: draft 1}%[archiEcoTaskV0]
\label{archiEcoTaskV0}
\end{figure}

After, Tomas explained a short example of code generation from \sofa architecture.
He took the \texttt{LogDemo} example %(Fig. \ref{logdemo}) 
and illustrated different versions of the Java generator.

%\begin{figure}[ht]
%\centerline{\epsfig{figure=\repFIGURES/logdemo.eps,width=6cm}}
%\caption[logdemo]{Logdemo example in \sofa}
%\label{logdemo}
%\end{figure}
\begin{multicols}{2}
~\\
~\\
\epsfig{figure=\repFIGURES/logdemo.eps,width=7cm}
~\\
~\\
\footnotesize
\begin{verbatim}
    module logdemo {
      interface LogInterface {
        void log(in string number);
      };
      frame Caller {
        requires:
          LogInterface Log;
      };
      frame Logger {
        provides:
          LogInterface Log;
      };
    };
\end{verbatim}
\normalsize
%see also http://sofa.objectweb.org/sofa1/docs/docdemosrc/demodescr.html
\end{multicols}

There are two primitive components - \texttt{Caller} (or \texttt{Caller} in his example) and \texttt{Logger}. \texttt{Logger} provides the interface \texttt{LogInterface}, \texttt{Caller} requires this interface, in the component \texttt{logdemo} these two components are instantiated and their provision and requirement are bound together.

In the first translation, plain Java code is generated with a specific implementation of requirements (variable + methods).

%\begin{multicols}{2}
\footnotesize
\begin{verbatim}
 // LoggerImpl.java
package SOFA.demos.logdemo;

public class LoggerImpl implements LogInterface {
  public void log(java.lang.String msg) {
    System.out.println("**** LOG: "+msg);
  }
}
\end{verbatim}
\begin{verbatim}
// CallerImpl.java
package SOFA.demos.logdemo;

public class CallerImpl implements Runnable {
  SOFA.Component.DCUP.DCUPComponentManagerImpl cm;
  LogInterface LogRequirement;
  boolean end;
  boolean stopped;
  public CallerImpl(SOFA.Component.DCUP.DCUPComponentManagerImpl _cm) {
    ...
  }
  private void setRequirement() throws SOFA.Component.NamingException {
    LogRequirement = (LogInterface) cm.getRequirement("Log");
  }
  public void run() {
	...
  }
  public void setEnd() {
  }
  public boolean isStopped() {
  }
}
\end{verbatim}
\normalsize
%\end{multicols}

In a second translation, the provisions and requirements are specified as annotations in Java for a post processing.

\footnotesize
\begin{verbatim}
 // LoggerImpl.java
@provision(log)
public class LoggerImpl implements LogInterface {
  ...
}
\end{verbatim}
\begin{verbatim}
// CallerImpl.java
@requirements(log)
public class CallerImpl {
  boolean end;
  boolean stopped;
  public CallerImpl() {
    ...
  }
  public void run() {
	...
  }
  public void setEnd() {
  }
  public boolean isStopped() {
  }
}
\end{verbatim}
\normalsize

The architecture is generated or predefined.
There are templates for connectors.
~\\

Last, we discussed about flat component / hierarchical components and the composition operators.
AT first we cannot reengineer the composite components from scratch.
One can build hierarchies on performance criteria or distribution criteria.
But is is enough for instance to build the primitive components and then manually to build the structures.
Jiri proposed launching the code with introspection rather than parsing the code.


\subsubsection{Java Path Finder, Bandera}

The afternoon started with a short description of JPF (and Bandera) by Jiri Adamek.
The slides of this intervention are provided on the Workshop Wiki at:\\
\small
\textcolor{BrickRed}{\url{http://www.lina.sciences.univ-nantes.fr/coloss/wiki/doku.php?id=econet:pragues2007:}\\ \url{program07}}
\normalsize

\subsubsection{Bandera} %~\\

Jiri explained that Bandera was unstable at the time he studied it and the
second version was not really public on the web site\footnote{\url{http://bandera.projects.cis.ksu.edu/}}.
Bandera is a 6-years old source transformer.
Bandera allow to check in a semi-automatic way different properties for  different abstractions (Fig. \ref{bandera}).
Two years ago a model-checker for Java, called BOGOR\footnote{\url{http://bogor.projects.cis.ksu.edu/}}, has been developped ;
it can be a future source of information and tool.

\begin{figure}[ht]
\centerline{\epsfig{figure=\repFIGURES/bandera.eps,width=8cm}}
\caption{Bandera overview}%[bandera]
\label{bandera}
\end{figure}


\subsubsection{Java Path Finder}%~\\

%see slides of Pavel (26/06/07) JPF introduction
JPF is a Java model checker developped at NASA Ames Research Center\footnote{\url{http://javapathfinder.sourceforge.net/}}.

\begin{figure}[ht]
\centerline{\epsfig{figure=\repFIGURES/jpf1.eps,width=14cm}}
\caption{JPF model of operation}%[jpf1]
\label{jpf1}
\end{figure}

In general, JPF is capable of checking every Java program that does not depend on unsupported native methods. The JPF VM cannot execute platform specific, native code. This especially imposes a restriction on what standard libraries can be used from within the application under test. While it is possible to write these library versions (especially by using the Model Java Interface - MJI mechanism) there is currently no support for java.awt, java.net, and only limited support for java.io and Java's runtime reflection. Another restriction is given by JPF's state storage requirements, which effectively limits the size of checkable applications to ~10kloc (depending on their internal structure) if no application and property specific abstractions are used. Because of these library and size limitations, JPF so far has been mainly used for applications that are models, but require a full procedural programming language. JPF is especially useful to verify concurrent Java programs, due to its systematic exploration of scheduling sequences - an area which is particularly difficult for traditional testing.

One problem in a component view is that it accepts only closed java programs.
It explores the state space.
%Which defects can be found by JPF? 
Out of the box, JPF can search for deadlocks and unhandled exceptions (e.g. NullPointerExceptions and AssertionErrors), but the user can provide own property classes, or write listener-extensions to implement other property checks. A number of such extensions, like race condition and heap bounds checks are included in the JPF distribution.
One advantage of JPF is that it accepts \textbf{listeners} for custom search algorithms and an access to a Model-Java interface via its API (Fig. \ref{jpfapi}).

\begin{figure}[ht]
\centerline{\epsfig{figure=\repFIGURES/jpfapi.eps,width=10.5cm}}
\caption{JPF Java layers}%[jpfapi]
\label{jpfapi}
\end{figure}

%\begin{figure}[ht]
%\centerline{\epsfig{figure=\repFIGURES/jpfreport.eps,width=14cm}}
%\caption[jpfreport]{JPF Java layers}
%\label{jpfreport}
%\end{figure}
%The properties checked are either predefined (e.g. absence of a deadlock) or to be specified in LTL (Bandera) and via assertions related to the code (JPF). A typical feature of both Bandera and JPF is the combination of static program analysis and model checking. The former is used to create a program model; to lower the state space size, abstraction techniques are applied - these include partial order reduction and data abstraction.

\newpage

\subsubsection{Project modules and interfaces (discussions)}

In this part we discussed more precisely on the project architecture (Fig. \ref{archiEcoTask}), its modules and the minimal information we need for behavioural abstraction.

\begin{figure}[ht]
\centerline{\epsfig{figure=\repFIGURES/archiEcoTask.eps,width=12cm}}
\caption{Econet Architecture: final version}%[archiEcoTask]
\label{archiEcoTask}
\end{figure}

The abstraction process ((Fig. \ref{absProcess})) should infer components and structure for the behavioural abstraction.
The information are given directly by the source code via Java annotations.
A main information for the latter is the "entry point" information (intialisation).
The entry point denotes the active component.

\begin{figure}[ht]
\centerline{\epsfig{figure=\repFIGURES/absProcess.eps,width=7cm}}
\caption{Abstraction Process}%[absProcess]
\label{absProcess}
\end{figure}

The B process is more general than the A one since it can apply to non-behavioural abstract models.
\textit{It provides more complete results with less informations}.
The borders delimit frontiers and component contexts (separate business and management for example) and link classes to components.
The goal is to extract interfaces (one or more) using hierarchical graph analysis for example.
The approach uses annotation based methods and techniques coupled with user friendly graphical interface to get the missing informations from the user.
Possible starting points and resources are: Java only, UML models, component models, EJB program...

\subsubsection{Toward an annotation language (discussions)}

To define the required informations (and annotations) we tried to map the model concepts (Fig. \ref{absMapping}).
We separate business functionalities from non-business ones (related to Java computations or to management handling e.g. setRequirements).
We should find annotations about provided interfaces (which is absent or difficult to find in plain Java).
Provided interface are annoted on java interfaces and methods.
Required interfaces can be annoted from java attributes.
All the class belonging to a component should be annotated.
One question is: how many instances of a component do we accept, only one ?

\begin{figure}[ht]
\centerline{\epsfig{figure=\repFIGURES/absMapping.eps,width=10cm}}
\caption{Mapping concepts}%[absMapping]
\label{absMapping}
\end{figure}

\noindent
Remark 1: there is one protocol per component (frame) and not per interface.\\
Remark 2: the annotations must be complient with other java annotations (meta model).

%\newpage

\subsection{Friday, September 7, 2007}

\begin{center}
\begin{tabular}{||c|l|l||}
\hline
\textbf{Time} & \textbf{Activity} & \textbf{Speaker}\\
\hline
\hline
09:00 & Welcome & Pascal André\\
\cline{2-3}
$|$ & Comparison of Abstract Models (discussions) & - \\
\cline{2-3}
$|$ & Common Meta Models (discussions) & - \\
\cline{2-3}
12:00 & Round tables and discussions & -\\
\hline
\hline
13:30 & Technical discussions (RE techniques and tools,  & - \\
$|$ & annotation Language, collaborative tools...) & - \\
\cline{2-3}
17:00  & Closure & Pascal André, Ondrej Sery, Petr Hnetynka\\
\hline
\end{tabular}
\end{center}

\subsubsection{Welcome}
 
Pascal introduced the third day working session by giving an abstract of the
discussions and the gainful decisions of the previous days.
We significantly progressed on the project structure and module interfaces and reached partially the convergence of the means (see section \ref{ws:intro:pa}).
This can be summarised as follow
\begin{itemize}
\item DSRG experience - 
\textcolor{BrickRed}{CoCoME, Behaviour Extraction, Tools (JPF, Bandera)}
\item Project Architecture (Fig. \ref{archiEcoTask})
\textcolor{BrickRed}{Three parts}
\begin{enumerate}
\item Component Metamodel \textcolor{BrickRed}{cross LTS extensions, WFR}
\item Structure Abstraction \textcolor{BrickRed}{user interacted tool}
\item Behavior Abstraction \textcolor{BrickRed}{A-interface definition, annotations generation}
\end{enumerate}
\item Problem Domain Restriction
\begin{itemize}
\item metamodel $\implies$ components and behaviours
\item A $\implies$ no connections, no composition, no statement abstraction
\item B $\implies$ no composition, no statement abstraction, user-interactions
\end{itemize}
\item Benchmark = \textcolor{BrickRed}{CoCoME}
\end{itemize}
There remain things to do for this last day is to progress on the tasks definition, 
the responsabilities repartition and the planning building.
Moreover some discussions were mandatory on technical informations: 
models (abstract and concrete models toward a common meta model), 
techniques (control flow or parsing, detailed annotation language, ...).
The (optimistic) goal of day 5 is taht each participant has a somewhat clear idea of what he will do later.

Here are some guidelines for the definition of the tasks:
\begin{itemize}
\item What to do ? \textcolor{BrickRed}{on the draft architecture}
\begin{itemize}
\item Metamodel
\item Process A
\item Process B
\end{itemize}
\item Contributions ? \textcolor{BrickRed}{a subset of}
\begin{itemize}
\item Common Metamodel definition ?
\item Annotation language definition (input of process A)
\item Tools Prototypes for Metamodel verification, Process A, Process B
\end{itemize}
\item Synchronisation points = \\
A-interface, Metamodel def, B-Information def
\item Planning \textcolor{BrickRed}{deadlines}
\begin{itemize}
\item Evaluation (october 2007)
\item Workshop Nantes (begin of March 2008)
\item Workshop Cluj (end of august 2008)
\end{itemize}
\item ...
\end{itemize}

The slides (third plan) are provided on the Workshop Wiki at:\\
\small
\textcolor{BrickRed}{\url{http://www.lina.sciences.univ-nantes.fr/coloss/wiki/doku.php?id=econet:pragues2007:}\\ \url{program07}}
\normalsize

We started the day by a Comparison of Abstract Models and after several discussions on the Common Meta Model,the Annotation Language, the tools and the task repartition.


\subsubsection{Comparison of Abstract Models (discussions)}

The discussions continued with a fast comparison of the three abstract models (\sofa, \kadl, \kmelia) in order to grasp the structural and behavioural models and therefore tha annotations and some kind of metamodel.

\small
\begin{center}
\begin{tabular}{||l|c|c|c||}
\hline
\textbf{Concept/Model} & \textbf{\sofa EBPL} & \textbf{\kadl}  & \textbf{\kmelia}\\
\hline
\hline
\textbf{Attachment}  & Frame  & Component  & Service+ component\\
\hline
\textbf{Operations} & atomic assignments & atomic functions & atomic action+\\
\textbf{(computation)} & (constants?)  & (algebraic)   & service calls\\
\hline 
\textbf{Types}  & Enums  & any ADT  & "complex but open" \\
  &   &   &  means ad hoc \\
\hline
\textbf{Guards}  & logic + enum  & logic + ADT  & logic + ad hoc FL\\
\hline
\textbf{Dynamic formalism}  & reg. expr.  & state transition  & state transition +\\
  &   &   & "hierarchy" \\
\hline
\textbf{I/O}  & ! ?  & ? ! *  & ? ! ?? !!\\
\hline
\textbf{Labels}  & ?iface.notified   & [guard] event com/action  & [guard] action* \\
  & \{!iface2.pre\}  &   & (actions can be com or functions) \\\hline
\end{tabular}
\end{center}
\normalsize

We studied the corresponding java constructs in a engineering/reverse-engineering points of view.

\small
\begin{center}
\begin{tabular}{||l|c|c|c||}
\hline
\textbf{Concept/Model} & \textbf{\sofa EBPL} & \textbf{\kadl}  & \textbf{\kmelia}\\
\hline
\hline
\textbf{Attachment}  & set of classes  &  set of classes &  set of classes\\
\hline
\textbf{Operations} & plain methods & plain methods & methods + behaviours\\
\textbf{(computation)} & user Java statements  & algebraic translation   & generated code\\
\hline 
\textbf{Types}  & Java types  & Java types  & Java types +\\
  &  & classes (ADT)   & classes \\
\hline
\textbf{Guards}  & boolean expr.  &  boolean methods  &  conditions\\
\hline
\textbf{Dynamic formalism}  & control flows  & control flows  & various statements\\
  & (RMI...)  & (LTS Library) & (control structure, messages, methods))\\
\hline
\textbf{I/O} & method calls  & method calls & method calls\\
  & parameters & parameters   & parameters \\
\hline
\textbf{Labels}  & assignments   & if-then-else  & statements \\
  & user Java statements & patterns  & (Kml-lang) \\\hline
\end{tabular}
\end{center}
\normalsize

We started the day by a Comparison of Abstract Models and after a discussionson the Common Meta Models and the Annotation Language, and the task repartition.


\subsubsection{Common Meta Model (discussions)}

The common component meta model will include only the common part in its first design, leaving some holes for specific features.
The structural concepts are quite similar in the target languages.
The main features are those of the annotation language.
They differ mainly on the representation of behaviours (Fig. \ref{ecoCCMM}).

\begin{figure}[ht]
\centerline{\epsfig{figure=\repFIGURES/ecoCCMM.eps,width=7cm}}
\caption{Common Component Meta Model}%[ecoCCMM]
\label{ecoCCMM}
\end{figure}

\subsubsection{Technical discussions}

First a debate opened on the behaviour abstraction RE techniques and tools.
On one the usual way to proceed is to build the control graph: the states are the steps in the system evolution - its state space - and the transitions are the events and actions performed (method call, statements, control structure).
Then we can split the system behaviour onto components or just model check it.
The problem is that it contains low levl informations and it should be abstract:
group state and transitions.
This technique is well fitted to LTS base components.
Another technique is to parse the java code and build parse trees (AST abstractact syntax tree with terminal and non terminal tokens).
This provides modular trees that can be merged/collapsed/extended to a more general flow.
This technique seems to be interesting to build regular expressions for the \sofa model.
It uses the SunAPI for Java and tools like \texttt{javacc}, \texttt{antlr}, \texttt{JavaCup}, etc.
In any case, one has to cross the results with existing component structures.
The second solution is chosen.

\begin{figure}[ht]
\centerline{\epsfig{figure=\repFIGURES/ecoJBA.eps,width=7cm}}
\caption{Java Behaviour Abstraction}%[ecoJBA]
\label{ecoJBA}
\end{figure}

Some issues remain open:
\begin{itemize}
    \item Parse Tree
	\begin{itemize}
    \item Coloration used to collapse parts of the Parse Tree
    \item Tools ?
	\end{itemize}
    \item Control Flow
	\begin{itemize}
    \item Coloration used to collapse parts of the Control Flow
    \item Tools ?
    \item Format ? textual +API
	\end{itemize}
    \item Find a good common format for both parse tree and control flow.
\end{itemize}

Then we exchanged views about the annotation language.
%Here are the main 
The \textbf{constructs in the component model} are associated or derived from one or several annotations in the code.

\paragraph{Frame/Component}

\begin{itemize}
    \item Corresponding Java construct: One or more classes
    \item Corresponding java annotation:
	\begin{itemize}
    \item target class or interface \texttt{@InComponent(annotation\_source, name\_of\_the\_component)}
	\end{itemize}
\end{itemize}

\paragraph{Interface}

\begin{itemize}
    \item Corresponding Java construct: one or more interfaces, or a set of methods from a class
    \item Corresponding java annotation:
	\begin{itemize}
    \item target class \texttt{@provided(annotation\_source, name\_of\_the\_model\_interface, name\_of\_the\_java\_interface)}
    \item target method \texttt{@provided(annotation\_source, name\_of\_the\_model\_interface)}
    \item target attribute \texttt{@required(annotation\_source, name\_of\_the\_model\_interface)}
	\end{itemize}
   things to think about later : (temp requirement passed as parameters …) 
\end{itemize}

\paragraph{"entry point"}

\begin{itemize}
    \item Corresponding java construct: The main class of a component
    \item Corresponding java annotation:
	\begin{itemize}
    \item target class \texttt{@initclass(annotation\_source, name\_of\_the\_component)}
    \item target method \texttt{@initmethod(annotation\_source, name\_of\_the\_component)}
	\end{itemize}
 Gilles: \texttt{name\_of\_the\_component} seems redundant because the method or the class should already belong to  a component ( see InComponent annotation)\\
things to think about later: (consistency rules needed? is having several initclasses, methods in a component legal ? ) 
\end{itemize}

\paragraph{Operation}

Do we need it ? We already know methods from the provided annotation 

\begin{itemize}
    \item Corresponding java construct: Method
    \item Corresponding java annotation:
	\begin{itemize}
    \item target method \texttt{@}
	\end{itemize}
Business methods have to be singled out 
\end{itemize}

\paragraph{Types}

Goal: identify parameters of business methods \\
Problem: String or int may be used as business object sometimes and sometimes not 

\begin{itemize}
    \item Corresponding java construct: class or interface
    \item Corresponding java annotation:
	\begin{itemize}
    \item target class or Interface \texttt{@initclass(annotation\_source, name\_of\_the\_component)}
    \item target method \texttt{@ businessparameter(annotation\_source, parameter\_name)} (this one takes precedence over the previous one)
	\end{itemize}
things to think about later: another annotation could be for abstracting data : telling that an integer only has a few cases...
\end{itemize}

Business Types have to be annotated. In some cases (library without accessible source code) they can't be, so a textual configuration file will be used to list them or to list non-business types. White list, black list, regular expressions over full name ? 

%pre/post
%reverse informations not model treansformation


Last we disccused about tasks, responsabilities and milestones.
Every body participates to the common annoted bibliography on the wiki.
Here is a pictured summary of the responsability and participant repartition on the project structure (Fig. \ref{archiEcoTaskR}).

\begin{figure}[ht]
\centerline{\epsfig{figure=\repFIGURES/archiEcoTaskR.eps,width=12cm}}
\caption{Econet Architecture: responsabilities}%[archiEcoTaskR]
\label{archiEcoTaskR}
\end{figure}

As a collaborative tool, a version manager (CVS) will be installed by DSRG, in addition to the wiki plateforme installed by COLOSS.
We aim share the tools (source and experience) used during the development.

\subsubsection{Closure}

Production

\begin{itemize}
\item Workshop Report
\begin{itemize}
\item Collect paper and slides \textcolor{BrickRed}{Please send them to me}
\item Summary of the discussions
\end{itemize}
\item[+] Bibliographical Notes\\
\item[$\implies$] \textcolor{BrickRed}{project plan for year 2 and
 \textit{Evaluation}}\\
\item Fix the participants objectives
\item Documentation, research reports
\item Intermediate results $\implies$ Second Workshop
\item \textcolor{darkGray}{Publications (?)}
\end{itemize}
\textit{\textcolor{BrickRed}{see also the initial 'Second year objectives'}}

The organizers thanks the participants for their contributions and take a date for a next workshop at Nantes in 2007.

\endinput

