% Project: ECONET 
% Document: Prague07 Workshop Report
% Last writer: Andre Pascal 
% creation: 14/09/07 
% modification PA 27/09/07 
% *********************************** 
%\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: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:pragues2007:materials}}
\normalsize

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

\subsection{Introduction}

During the development process of an information system several models are produced (manually or automatically).
%The role of software engineering is 
A main objective of the ECONET partners are to contribute to improve both the  models and the production.
In particular, all partners are concerned with the verification of models and programs.

To simplify, let consider at least two levels for the models produced during the development process: an abstract model and a concrete model written in a programming language  \textit{i.e.} in Java.
From the verification point of view, the goal is to assert properties (by proof or by model checking) on both the abstract and the concrete models.
One way (the formal method approach) is to assert properties on the abstract model, then to refine it into a concrete model and prove the refinement.
Another way is to assert properties on both levels.

In this workshop we are mainly interested in the model-checking approach for property verification.
Model checking is the process of checking whether a given model satisfies a given logical formula. The concept is general and applies to all kinds of logics and their models. A simple model-checking problem is testing whether a given formula in the propositional logic is satisfied by a given model.
In case of properties to be checked, the most common ways to express them are
via a temporal logic (LTL, CTL) and in the form of assertions. 
However, it is also possible to check for a predefined set of properties - deadlocks or properties specific to a certain class of systems such as device drivers.

One can admit that model checking at the abstract level is well-known and 
there exist techniques and tools for model-checking abstract models but  model-checking concrete models is to discover.
Model checking of software is a popular research topic nowadays, mainly because there are several issues that have to be solved before the technique can be used for real-life applications.

How can we do ?
We can check the code it self with appropriate tool.
This is not convenient because the tools are not mature in this domain and
 the concepts at the concrete level are quite different from those of the abstract level, the informations are numerous and more detailed, model-checking quickly faces the problem of state explosion.
Another approach is to filter the informations:
\begin{itemize}
    \item by selecting informations of the code model checker (as explained in the presentation of Pavel Parisek)
    \item by abstracting informations of the code , this is main issue of our Econet Project:  extract abstraction \textit{i.e.} in order to apply model checking at the abstract level. Two cases are possible whether an abstract model exists or not.
\end{itemize}

The talked given during the presentation sessions addressed contributions on the above topics.
Many of them present an abstract model and model checking techniques (Petr Hnetynka, Jan Kofron, Jean-Claude Royer, Pascal André).
The talk of Pavel Parizek is more precisely about the problem of model checking concrete models against abstract ones).
The talk of Dan Chiorean was more general because it works on models and metamodels, moreover it assumes a quite different view of model checking, that is the verification of consistency and completion of models. 

Note that we summary the main issues of the team presentation and forget among others, history and members details.

\subsection{Monday, September 3, 2007}

\begin{center}
%\begin{table}[h]
%\centering
\begin{tabular}{||c|l|l||}
\hline
\textbf{Time} & \textbf{Title} & \textbf{Speaker}\\
\hline
%\multicolumn{3}{||c||}{\textcolor{BrickRed}{Monday 3 september 2007}} \\
\hline
10:30 & Welcome and Program & Pascal André\\
\cline{2-3}
$|$ & Participant presentation & each participant\\
\cline{2-3}
$|$ & Local Organisation & Ondrej Sery, Petr Hnetynka\\
\cline{2-3}
12:00 & DSRG Team presentation and position & Frantisek Plasil\\
\hline
\hline
13:30 & \sofa overview & Petr Hnetynka\\
\cline{2-3}
$|$ & (Extended) Behavior protocols + demo (from CoCoME contest) & Jan Kofron\\
\cline{2-3}
17:00 & Checking behavior protocols against code using Java PathFinder & Pavel Parizek\\
\hline
\end{tabular}
%\caption{Presentation Sessions Program}
%\label{tab:ps}
%\end{table}
\end{center}

%%%%%%%%%%%%%%%%%%%%%%%
\subsubsection{DSRG}

Frantisek Plasil presented the Distributed Systems Research Group, one of the research groups of
the Department of Software Engineering of Charles University.
Its areas of interest are:
\begin{itemize}
    \item Software Performance (Regression benchmarking),
    \item Software Components (\sofa, Fractal)
	\begin{itemize}
    \item Architecture/Component models,
    \item Design (Use cases, Behavior specification of components - Model checking),
    \item Deployment (Connectors - Addressing environment heterogeneity)
	\end{itemize}
\end{itemize}

DSRG focuses on research in distributed systems, particularly the construction of component and service middleware and its software engineering aspects - system architecture, formal definition and verification of behavioral properties, performance evaluation. This focus is reflected in the long running \sofa project, which deals with a distributed component model that provides advanced features such as formal verification of component properties, and which is provided as an open source platform. Other major projects that DSRG recently participated in include the ITEA PEPITA \& OSMOSE \& OSIRIS projects and industrial projects with partners such as France Telecom, Borland and Iona.

The areas of contribution to ECONET are in general a cross fertilization and joint publications. More specifically, they are 
providing \sofa, 
enhancing EBP by additional features from STS/eLTS (to enhance expressive power of EBP ),
extracting protocols (EBP) from code  (at least BP from code),
defining %OCL: WFR for component diagrams, activity diagrams? 
well-formed rules for \sofa components,
prviding a benchmark (CoCoME example). 


\subsubsection{\sofa overview}

As chief architect, Petr Hnetynka presented an overview of \sofa2.
The \sofa 2.0 is the new version of the \sofa component system. It focus on removing limitations of the current \sofa implementation (inconsistencies between
implementation and specifications e.g., protocols vs. connectors, architectures vs. dynamic reconfiguration,...), clear design and properly balanced support of advanced features. These are mainly:
\begin{itemize}
    \item  model-driven design
    \item  hierarchical architectures
    \item  support for dynamic architectures
    \item  support for multiple communication styles
    \item  formal modeling of both functional and non-functional parts of components
    \item  transparent distribution
    \item  behavior validation
\end{itemize}
It is implemented in Java (as \sofa was).
The implementation freely available (LGPL license) \url{http://sofa.objectweb.org/}.

The presentation included detailed informations on 
\begin{itemize}
    \item Component model
\begin{itemize}
    \item  meta-model
    \item  dynamic reconfiguration (dynamic architectures)
    \item  connectors
    \item  control parts (non-functional)
    \item  versioning
    \item  behavior specification
\end{itemize}
    \item Implementation
\begin{itemize}
    \item component lifecycle
    \item runtime environment
    \item usage, tools, current status
\end{itemize}
\end{itemize}

\noindent\underline{Questions}~\\

About consistency (Metamodel well-formedness rule) the project organization in two parts on the group (components archi / behavior specifications) lead to some independent (and not compatible) evolutions. Well-formedness rule are informal except for protocols.

The micro-components have a similar concept in fractal (monitoring methods and  repository).

The 'aspects' are not really those of Aspect Oriented Programming.

About the link between specification and code, non-\sofa components can be encapsulated in wrappers, connectors can be RMI, Corba, the implementation is
java specific with \sofa knowledge and annotations (future).

Communication style in connectors can be any communication style (method invocation, shared memory, ...).

\subsubsection{Modeling and Verifying Behavior of Software Components in \sofa 2}

Jan Kofron presented the (original) Behavior Protocols of \sofa and the extensions of Behavior Protocols (EBP) of \sofa 2.0.
Each part was organised as follow (presentation, description, verification, experience, demo).

The problem of behavior verification is undecidable in general. There are two ways to face it: (1) To use behavior description languages which describe behavior of the software precisely and to put up with the fact that the tools will never stop for some inputs (behavior descriptions). (2) To use behavior description languages, which are not expressive enough to describe behavior of software precisely, but the verification of the specifications is decidable. We have chosen the second approach. Therefore, a behavior protocol should be seen rather as an approximation of a component's behavior. The most important benefit of this approach is the existence of a fully automatic behavior verification procedure (implemented in our behavior protocol checker).

The purpose of behavior protocols is to specify the behavior of software components, so that interesting properties of their behavior can be verified (not only the operation signatures) using model checking techniques for example.
Model checking is one of the approaches to formal verification of finite state
hardware and software systems. A model checker usually accepts a finite model of
a target system and a property expressed in some property specification language, and checks whether the model satisfies the property via traversal of the state space that is generated from the model. 

Behaviors are an abstraction of the component interactions and can be represented by LTS, use cases, sequence diagrams, process
algebra expressions, etc.
In \sofa, behaviors are described by processes (regular expression and communication primitives as in process algebra).
Checking protocol compliance (both horizontally and vertically) is similar to checking component behavior compatibility.
Compliance means: absence of communication errors(Bad activity, No activity, Infinite activity) which can be found automatically) and verified separately for particular levels of nesting (hierarchy).

In \sofa two checkers were implemented:
the Behavior Protocol Checker (BPC) (proprietary explicit state model checker for BP, written in Java, uses Parse Tree automata for state space generation, able to verify state spaces of the order 10\^{ }7 states, May run several days)
and the dChecker (again proprietary tool, distributed state space traversal, significantly faster than BPC, state spaces of the order 10\^{ }7 for each computer i.e., entire state space of the order of 10\^{ }8 state).
\\
Several flaws of BP were identified during the
specification: lack of synchronization mechanisms (impossible to synchronize more than two components), 
lack of expressiveness (absence of macros caused parts repetition in the
specification which make it hard to fix the errors, absence of variables caused overspecification, absence of a way to express common patterns, e.g. until
loops, caused unreadable specification).

This led to extensions of BP on data (method parameters and local variablescan be of enumerated types), 
synchronization (special events: joining events for synchronization of
more than two components) and Until loops (just a syntactic abbreviation to enhance the readability).
Performance issues were also a motivation, the new solution is a 
transformation of EBP into Promela, the input language of the Spin Model Checker.
The performances were improved on the same benchmak (CoCoME).
~\\

\noindent\underline{Questions}~\\

Guards are possible, they are branches on local state. 

A visual representation of the protocols is possible via parse trees.
The component picture is manually done with Visio in a UML flavor.

Local checks are performed. Promela checkes both horizontal and vertical compliance. One to many is in the metamodel.

About feedfack, there are solutions...

\subsubsection{Checking behavior protocols against code using Java PathFinder}

Pavel Paryzek addresses a topic that is close to the project concerns\footnote{See the remarks in the introduction section}:
the verification of conformance between behavior specifications and code.
This work locates in the general problem of model-checking programs and especially Java code. 
Remind that in the previous presentation, Jan Kofron talked about (abstract) model checking.
The problem addressed here is to do it at the implementation level.

A general problem of model checking is the necessity to create a model of the
system to be checked. Manual construction of the model is an error-prone process, and even if the model is automatically extracted from a specification of the system or from the source code, it is an abstraction - therefore, a model checker may find errors in the model that are not present in the original program and vice versa. A solution is to use a model checker that does not need to have a model, but works directly with the implementation of a target system.
There are several difficulties encountered with such an approach:
code model checkers are need,
the models and properties handled are low-level,
there is a problem of state explosion since an abstract state collapse many concrete states,
partial models are to check and not only full programs.
The talk of Pavel deals with these difficulties.

As to software model checking at the program source code level, a crucial
problem is the size of state space triggered by the model of a program (i.e. the
problem of state explosion). Despite that, there exist such model checkers. For Java programs, these are most notably the Java PathFinder (JPF) and Bandera  tools. (An advantage of JPF over Bandera is that the most recent release of the latter is an alpha version, not being fully stable yet, and that JPF is also more extensible). 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.
State explosion can be also mitigated by the decomposition of a software system
into small and well-defined units, components. Typically, a software component
generates smaller state space than the whole system and therefore can be checked
with fewer requirements on space and time. Nevertheless, model checking of code
of software components usually brings along the problem of missing environment,
what means that it is not possible to model check an isolated component, because
it does not form a complete program with an explicit starting point (e.g. the main method). In order to solve this obstacle, it is necessary to create a model of the environment of the component subject to model checking, including the
specification of possible values of method parameters, and then check the whole
program, composed of the environment and component. A specific feature of
software components is the existence of ADLs (Architecture Description
Languages) used to specify component interfaces, and first of all composition of
components via bindings of their interfaces (i.e to specify the architecture of a component-based application at a higher level of abstraction than code). Some
ADLs even include the option to specify behavior of the components, typically in
a LTS-based formalism.
An obvious challenge, not addressed yet to our knowledge, is to check the code
of software components against a high-level behavior specification provided at the ADL component specification level.

In this work, it is assumed that each primitive component (Java code) is compliant with its frame protocol (we thus have an abstract model).
It has to accept/issue exactly those method call related event sequences on its frame that are specified by the frame protocol.
The goal is to design an algorithm and a tool for checking compliance between Java implementation of a primitive component and its frame protocol via Java source code or byte code analysis.

The experimentation is done with JPF (Java PathFinder)
 a model checker for Java programs which is highly customizable and extensible ;
it is able to check only low-level properties (such as deadlocks, uncaught exceptions) with non-deterministic value choice.
It supports a \texttt{Publisher/Listener} pattern that can can watch the course of the state space traversal and check for specific properties.
Checking by JPF is not directly possible because JPF is able to check only low-level properties.
So an extension of JPF is necessary to check the compliance between Java code and frame protocol is a high-level property: \textit{a cooperation between JPF and the BP checker is defined with a backtracking policy}.

More over JPF accepts only complete Java programs: \textit{an automated generation of component environment is proposed to solve the problem of missing environments} (for components).
The model should force the environment to call a certain method of a particular provided interface at the moment the component expects it and 
to accept a certain method call issued on a particular required interface at the moment the component "wishes" to do so.
Two options are possible:
\begin{itemize}
\item Inverted frame protocol which is constructed from the frame protocol by replacing all the accept events with emit events and vice versa.
This option models the most general valid environment
\item Context protocol which specifies actual use of the target component by the other components in the particular hierarchical architecture.
This option models the simplest valid environment.
\end{itemize}
Context protocol is more suitable because the component application typically exploits a subset of functionality provided by the target component and
completeness and feasibility are taken into account at the same time.
But context protocol is time consuming and there are no java construct for acceptance of a method call calling protocol.

Last, two techniques are proposed to reduction of environment's complexity (state explosion problem) : reduction of level of parallelism (static code analysis, concurrent metrics) and reduction of repetitions.
~\\

\noindent\underline{Questions}~\\

You used the base BP model checking for this experimentation, did you investigate it in the context of EBP with promela and SPIN.
No really we shoukd have the same problems probably.

Do you think JPF can be used for reverse engineering ?
Not exactly JPF provides executions abstractions through the traversal of execution flows on ibjects and classes.
It can be associate to other tools via its listeners.

\subsection{Tuesday, September 4, 2007}

\begin{center}
\begin{tabular}{||c|l|l||}
\hline
\textbf{Time} & \textbf{Title} & \textbf{Speaker}\\
\hline
\hline
09:00 & Introduction & Pascal André\\
\cline{2-3}
$|$ & LCI Team presentation and position & Dan Chiorean\\
\cline{2-3}
12:00 & (UML) Model Checking - an OCL Based Approach & Dan Chiorean\\
\hline
\hline
13:30 & OBASCO Team presentation and position & Jean-Claude Royer\\
\cline{2-3}
$|$ & Introduction Illustrating The STSLIB Project:  & Jean-Claude Royer\\
$|$ & Towards a Formal Model Component Based on STS & \\
\cline{2-3}
$|$ & COLOSS Team presentation and position & Gilles Ardourel\\
\cline{2-3}
18:00 & The \kmelia Component Model Hierarchical Service Description and Analysis & Pascal André\\
\hline
\end{tabular}
\end{center}

\subsubsection{Welcome}

Pascal André introduced the program of this second day of presentations including three team presentations and technical talks.

%%%%%%%%%%%%%%%%%%%%%%%
\subsubsection{LCI}

Dan Chiorean presented the Computer Science Research Laboratory (LCI or Laboratorul de Cercetare Stiintifica In Informatica).
The Computer Science Research Laboratory  was established in 1990, as an auxiliary department of the  Mathematics and Computer Science Faculty. The projects handled by the laboratory are included in contracts with the Ministry for Research and Technology and certain academic institutes. 
Its main purpose being the promotion of research activity in a top field, that of object-oriented technology.
% and the actual involvement of the best students in this activity.
%All the members of the team, except the head of the laboratory, were students at the time they were employed. If we refer only to the period of 1995-1998, 5 of the members of the laboratory were granted, through selection, PHD scholarships abroad
%Beginning with 1995, six members of the laboratory have held TEMPUS scholarships for a period of time of 2 to 6 months. Other members, who decided to leave the laboratory, work now for IT Industry leaders such as Siemens or Microsoft.
%The average age of the team is very low. All the members of the laboratory (except the head of the project) are between 22 and 27 years of age.
%Carrying out the activity under these circumstances has been made possible by the special quality of the members of the team. Most of them were winners of the national contests of Computing and Mathematics, for example, RADU Lupsa won the first prize at the International Olimpic Contest of Computer Science. 

The main products designed and implemented in the lab
so far were the mFOOPS environment, and the ROCASE and OCLE tools.
The UBB-LCI team participated in the EU Research Project IST
1999-20017 NEPTUNE. The LCI team obtained recognised results in
the areas of model checking. Continuing the work begun in the
NEPTUNE IST project, and using some of the results obtained in
that framework, the LCI team designed and implemented OCLE, one of
the most complete OCL tools existing today. The LCI group is very
keen on continuing its work in the above-mentioned domains, with
special interest in MOF based repositories, OCL support for all
abstraction levels, OCL extensions for transformations and action
support, improved code generation, application of MDD (Model
Driven Development).

In the context of this ECONET project, the UBB-LCI team brings its
experience in the definition of contract and data features in the
definition of the component specification and in the verification
of consistency between these features and the Java code.

\subsubsection{(UML) Model Checking - an OCL Based Approach}

Dan Chiorean exposed his point of view on model checking UML models.
This research area is taken in the context of latest modeling approaches.
This means that it take place in the Model Driven Approach and Languages (MDA, MDE,  LDD, DSL) which are characterized by:
the use of metamodeling,
modeling languages more specialized compared with UML,
modeling languages are MOF based languages.
In this context, a robust and thoroughly tested MOF model would be in the benefit of all modeling languages  
Specifying a precise syntax and semantics requires usage of rules (another formalism - algebraic specs)
An appropriate OCL support is needed 
(U)ML uses different formalisms for specifying architectural and behavioral information, therefore checking (U)ML models is quite complex.
The results and conclusions obtained in UML Model Checking, can be used, both direct or indirect in checking models specified using the latest modeling approaches.

The objectives are: 
to ensure that the model conforms with different kinds of rules
(UML Well Formedness Rules WFR, Profile Rules PR, Business Model Rules BMR, Methodological Rules MR, Behavioral constraints rules BCR),
to use  accepted and easy to understand standards in the modelers community
to validate the standard specification on real models.

The following results are expected.
Realized applications comply with requirements.
Application become more reliable. 
Time needed for developing applications is diminished.
The application costs decrease.
Promoting reuse to all model element levels (classes, components, patterns, frameworks).

In the context of new modeling approaches, model compilation has to become a mandatory requirement (like source code compilation)
In order to accomplish these objectives an incremental and iterative approach is proposed: rule specification, rule validation, identification of reasons for rule failures, model updating - applied to different modeling layers.

Then Dan described some features of UML Models related to OCL and verification rules, and some examples of rules in each category (WFR, PR, BMR, MR, BCR).
%The aspects considered in (UML) Model Checking - 
(UML) Model Checking concerns: Model Completeness, Model Consistency, Model Correctness and Model Architecture Accuracy.
Model Checking related activities must be supported by appropriate CASE tools.
Some questions are: what could be done in order to improve the state of facts?
Is the needed information disposable?
Is the textual formalism appropriate?

In previous related work, people mainly faced the problem of the model consistency property, but it is only a part of model checking.



Despite of its important potential and role in defining a more rigorous modelling language and in designing and implementing safer applications, until today OCL was not used at its true value. Using the results obtained in implementing OCL support in ROCASE 3 , and taking into account the conclusions obtained testing the tools mentioned at http://www.klasse.nl/ocl, the paper tries to analyse this state of facts. The requirements needed in order to obtain a strong OCL support are presented. The ROCASE OCL support beyond semantical analysis is presented by means of a real example. Finally the conclusions acquired in our activity are offered.

demo

~\\

\noindent\underline{Remark}~\\

The definition of model checking is quite different from the one in \sofa, \kadl, and \kmelia approaches. The main reason is that it works at a model level rather than at the system level.

\noindent\underline{Questions}~\\



%%%%%%%%%%%%%%%%%%%%%%%

\subsubsection{OBASCO}

Jean-Claude Royer presented the OBjects, ASpects, and COmponents (OBASCO) team.
OBASCO is a joint research group of (the CS Departement of) Ecole des Mines Nantes and INRIA's research unit in Rennes, IRISA (see also OBASCO's home page at IRISA). OBASCO is also a team of Laboratoire Informatique de Nantes Atlantique (LINA, FRE CNRS 2729). 
%See section \ref{pres:coloss} for the presentation of LINA.
The LINA laboratory in "Sciences and technologies of the software" is mainly a cooperation between Ecole des Mines de Nantes and the University of Nantes.
It is specialized on two axes : distributed software architectures and computerized decision-making systems.

%Just-in-time production of plug and play software components is today a necessity. It has created increased demand in a number of domains related to distributed applications assembled using heterogeneous components. As a result, generative programming offers a set of techniques that automatically manufacture software components by developing programs that transform or generate other programs. The OBASCO team of the distributes software architecture branch of the LINA laboratory is an intrinsic part of this approach. It assumes the existence of a continuum between OBjects, ASpects, and COmponents that facilitates software industrialisation while also supporting the adaptation of its components. OBASCO addresses the general problem of adapting software for its purposes by developing tools to build distributed software architectures based on reusable, crosscutting units such as components and aspects. We are developing techniques that emerge from the arena of generative programming languages, in particular post object-oriented and domain specific languages. Our two main application domains are on the one hand, Operating Systems and Networks, on the other, Middleware and Entreprise Information Systems. 

The OBASCO (Objects, Aspects and Components) research group addresses the general problem of adapting software to its uses by developing tools for building software architectures based on components and aspects. We are (re)using techniques developed in the programming languages domain, and more precisely in object-oriented programming. 
%Our research focuses on the three topics:
%\begin{itemize}
%    \item Component-oriented programming\\
%    Definition of a language making it possible (i) to program components by explicitly representing their composition both at the structural and behavioral level, (ii) to manage their adaptation all along their life cycle. To this aim, we are relying on reflection and specialization techniques. We are also looking at how to interface such a language with de facto industrial standards such as EJB, .NET, and CCM. 
%    \item Aspect-Oriented programming\\
%    Formalization of aspect-oriented programming based on the concepts of event, trace, and monitor. Implementation of a corresponding language using reflection, as well as program analysis and transformation techniques. This work is currently applied to both the Java and C programming languages. 
%    \item Post-Object-Oriented programming\\
%    Contribution to the evolution from an object model to a unified model supporting programming in the large and adaptation through reflection. Study of the problems resulting from integrating objects and aspects on the one hand, objects and components on the other hand. 
%\end{itemize}

The objectives are to solve scalability problems in software engineering and to
 improve software architectures adaptation.
Two main directions are followed the separation of concern (specific programs for specific problems) and correct composition of existing programming artefacts.

The research domain covers topics on the Software Engineering
\begin{itemize}
    \item Software components and scalability
    \item Programming languages
    \item Post object-oriented programming
    \item Generative programming
	\begin{itemize}
    \item Sequential, concurrent and distributed
    \item Mechanism for separation and composition
    \item Objects versus aspects versus components
	\end{itemize}
    \item Model driven engineering: transformation techniques
\end{itemize}
according to three swim lanes
\begin{itemize}
    \item Aspect-oriented programming
	\begin{itemize}
    \item To explicit links between metaobject and aspect
    \item To formalize aspect-oriented models
    \item To design and implement a language
    \item Reverse engineering of legacy code with aspects
	\end{itemize}
    \item Software component
	\begin{itemize}
    \item Explicit protocols for components
    \item Property verification for components and architectures
    \item Understand relations between aspects and components
	\end{itemize}
    \item Domain specific language
	\begin{itemize}
    \item Domain specific language
    \item Expressiveness, extensibility and compilation
    \item Aspect languages, composition and DSL
	\end{itemize}
\end{itemize}

%The research work is applied to real-sized applications in the domain of enterprise information systems (middleware, business components) and embedded systems (dedicated operating systems and network equipment).

OBASCO brings its experience to the ECONET project with an abstract model based on algebraic specification and LTS, and its derivation to Java code (engineering process while in ECONET we work on the reverse-engineering process).
A first work was to verify some properties in component systems with
data, we have some results here, which make it possible to abstract
component protocols with data.  We have also shown how to generate
Java code from protocol descriptions, such that components can
communicate according to their declared behaviour.  Finally, we have
investigated aspect languages for the modularization of crosscutting
concerns defined in terms and through modification of protocols. A
question, which we did not study, was the compatibility between some
Java code and a protocol.
%Plasil and Co have some interesting experience in this area so w
OBASCO is also interested in extending the \sofa
approach to introduce data, parameters and
guards. Furthermore, we intend to study the integration of these
techniques with our on-going effort on the static analysis of
properties of protocol-modifying aspects.

\subsubsection{Introduction Illustrating The STSLIB Project: Towards a Formal Model Component Based on STS}

Jean-Claude Royer presented an approach that covered the whole development models from abstract description to Java implementation.

Component-based software engineering is becoming an important approach for system development. It is assumed here that explicit protocols are integrated into component interfaces to describe their behaviour in a formal way.
In this case explicit protocols are often dissociated from component code, it is not ensured that component execution will respect protocols rules.
A crucial issue is to fill the gap between high-level models, needed for design and verification, and implementation.

This talk introduces first a component model with explicit protocols based on symbolic transition systems. 
Some related models are quickly overviewed: Java/A, CADP, Behavior Protocols models (\sofa, PROCOL, CO-OPN), FSP java, JCSP.\\
The model is presented through an example: The Cash-Point Case Study.
The main concept is STS, for Symbolic Transition System, that is a dynamic description coupled with a data type description. A Labelled Transition System or LTS is an automaton with simple labels, states are sometimes called control states in this document. STS add to LTS full data types, guards and
input/output values. A transition is defined by \texttt{[guard] event
communication / action}.
The communication can be an emission (simple or multiple) or a receipt.
The data types describe the operation semantics of the emitters, the guards, the generators and the actions.
An algebraic style with positive conditional axioms is used to described the data types.\\
An architecture is almost a UML communication diagram rather than a UML component diagram: a link between ports denote event synchronization with
communications.
This was rather the \kadl model which is dedicated to analysis and verification purposes: the communication glue is simplified which is
very expressive in KADL and some other features are forgot: No inheritance between STS, ADT description are less general, No component parameterization.

The cash point example is illustrated on two points: defining a STS, defining the architecture. The existing elements or experimentations for tool support are explained.
\begin{itemize}
    \item Defining an STS\\
One first implementation was done Python (it is rewriting it in Java 1.5 under Eclipse) for the STS: the user writes a \texttt{.sts} file
(a parser exists for the dynamic part), 
an interface generator builds an ADT skeleton \texttt{.adt} 
(the user has to fill the axioms),
a Java translator generates a Java class from the ADT
(experimental) but the user may also write a Java class or reuse an
existing one.
    \item Defining an architecture\\
A grammar allow to express component types, local
instances, bindings and exports.
This is a bit more complex since the parser and the
loader have to be recursive.
It also needs to call the STS parser and loader.
When loading an architecture we have also to specify
where are the Java classes.
The instantiation process is also a bit more complex.
It is not completely stable since some choices about
bindings are pending.
\end{itemize}

The talk pursue by the level devoted to verification. 
In the past an approach using PVS (Theorem prover) has been 
experimented.
The new approach rather close to model-checking is
based on the notion of Configuration Graph (or CFG) which is a LTS but with a data value associated to each control state.
This allows formal analysis methods to analyze component and their interactions. 
Currently the verification process is to compute the synchronous product and check it or to compute the configuration graph and prove some
properties.
This tackle the difficult problem of state explosion when model checking with data.

Then a Java implementation for it is presented (runtime interpreter) that relies on a rendez-vous mechanism to synchronize events between component protocols. This talk showed how to get a correct implementation of a complex rendez-vous in presence of full data types, guarded transitions and, possibly, guarded receipts.

A tool support is made of a library with parsers and analysis tools
STSLIB is a project devoted to the design of sophisticated concurrent systems, their verification and code
generation. Currently this is rather a Java API and the targetted runtime language is also Java. It may be
used in the context of Eclipse or as a Java application.
~\\

\noindent\underline{Questions}~\\

One question was about the assistance for specification: only textual representations, the systematic usage of a 'self' parameter for data type operations, manual chain of specification processing.
These point should be improved with the future (planned) GUI (Graphical User Interface) on Eclipse.

Another was about funtional (for specification) and imperative (for implementation) styles for ADT.
Only a restricted form of ADT is accepted.

A last question was about communication primitives and especially the multiple one. Only the multiple rendez-vous is implemented.

Time and durations were also discussed.

\subsubsection{COLOSS}
\label{pres:coloss}

Gilles Ardourel presented the Safe Components and Softwares (COLOSS - COmposants et LOgiciels SűrS) group, a team of Laboratoire Informatique de Nantes Atlantique (LINA, FRE CNRS 2729).
The LINA laboratory in "Sciences and technologies of the software" is mainly a cooperation between Ecole des Mines de Nantes and the University of Nantes.
It is specialized on two axes : distributed software architectures and computerized decision-making systems.
%The first axis attacks in particular the problems related on the engineering of the software and the data management, in massively distributed architectures, wandering, communicating and adaptive. The second axis develops the research intended for the development of software tools powerful for the decision-making aid. The LINA treats the majority of the aspects of the domaine : from the representation and extraction of knowledge to the treatment of the natural language, the resolution of problems, or the optimization of resources, etc.
%These themes are developed within the ten research teams.

The research activities of the COLOSS Team range from Fundamental Research to Applications.
The main goal is the elaboration of concepts, methods and techniques supported by tools for software designers and developers
We explore formal approaches (based on mathematical foundations) to the assistance and the analysis in the development of software:
\begin{itemize}
    \item Multi-formalism specification and analysis of software systems,
    \item Specification, verification and validation of components and software architectures.\\
The goal is to ensure correctness of components used and their composition in complex software systems.
\end{itemize}

The motivations (fundamental challenges) are correct the software construction, the software quality and safety and the support for specific development methods.
The main research areas are 
\begin{itemize}
    \item Multi formalism specifications, multi-faceted analysis.\\
The monoformalism approaches are limited by a partial covering
of problem and a partial analysis.
COLOSS studies the Formal methods integration and faces some of its challenges (decomposition, semantic interoperability, formal analysis).
Multi-platforms experiments are leaded on B, PVS, Spin, Grafcet, Petri nets...
    \item Design and verification of model properties.\\
We investigate the use of formal methods and tools for modular modeling (component, objects) and property verification (system and model properties).
In the CBSE context the motivation is to provide models and practical tools to assist users in formal component-based development ; it covers the abstract definition of components and composition (simple, flexible and expressive), the verification of properties (safety, consistency, compatibility...) and the binding from components to code (refinement or code generation).\\
In the UML context the motivation is to improve the confidence in large and multifacet (diagrams) specifications where a formal semantics does not exist and where properties are quite complex \textit{e.g.} model consistency is made of plenty (sub) properties.
A single property can be decomposed into finer ones, can concern several groups of model elements, can be verified at different levels of completeness, and 
can be verified using several techniques with various costs and performances.
%We work on a generic and customizable verification process for checking UML models consistency (extensible to other models).
We work on %designed 
a generic verification process 
composite verification processes (with ordering, filtering, results propagation and annotation of faulty elements. . . )
that supports the classification of verifications and properties (levels, diagrams...) and the abstraction of the results of different tools and formalisms.
\end{itemize}

COLOSS contributes to ECONET by providing Kmelia (an abstrat model) and its COSTO tool,
its experience on formal methods and property verification,
its experience on Java programming
and a first experimentation on reverse-engineering Java to UML. 
COLOSS also expects fruitful exchanges with \kadl and \sofa to both enrich these models and \kmelia.

\subsubsection{The \kmelia Component Model Hierarchical Service Description and Analysis}

Pascal André presented the \kmelia Component Model and the Property Formal Verification towards the COmponent Study TOolbox (COSTO: Component Study Toolbox). The COSTO modules are being developed with JAVA.
The modules have been integrated into the Eclipse IDE as plug-ins.
Both the specification and analysis were illustrated on a bank Automatic Teller Machine (ATM) Case Study and its withdraw service.

The presentation begins by an overview of the model.
The \kmelia model is a simple, formal and abstract component
model based on the description of complex services. 
\begin{itemize}
    \item 
The simplicity relies on the few number of concepts that are used to
describe the components and their assemblies.
The main characteristics are: components, services, software architectures, protocols, contracts, specification of complex interaction between services.
    \item 
The components are abstract, independent from their environment and therefore non-executable.
\kmelia can be used to model software architectures and their properties, these models being later refined to execution platforms. It can also be used as a common model for studying component or service model properties (abstraction, interoperability, composability). 
    \item 
A formal model is defined for components and services, including syntax and type checking, contracts and LTS.
This is the basis for any automated processing support.
    \item 
The service are first class elements and not only messages
which means that 
(1) services may be defined by a dynamic behaviour (a protocol) in addition to their signature and contract and
(2) services may be composed of other services.
Each service has an enhanced service interface which includes a service dependency composed of the provided services and the required services which are used in its context.
The notion of service is central to \kmelia and a component interface describes mainly services.
This means that the components are connected via their services (functional connections).
The interaction model is therefore simple: required services are
directly linked to provided services.
\end{itemize}
The model is extensible: it is possible to add new concepts from the kernel \textit{e.g.} protocols, adaptors, aspects...

A component is a structuring unit that encapsulates a state and services; has an interface with usage constraints.
A component has an interface including provided services and required
services.
A service is an abstraction of a functionality (signature, contract); it has a behaviour (dynamic evolution).
The behaviour is defined by an extended LTS where transitions accept functional actions or communications (messages send or receipt, services call or return).
A service also has an interface including provided services and required
services that may lead to a hierarchical structuration.
Assembly links are a simple support for component connection and interaction.
Promotion links are a means for simplifying encapsulation.

The second part of the talk is dedicated to the verification of properties and its support with COSTO.
The verification principles are: a formal verification of properties, a
reduced user interaction (automation), customisable verification process, 
interconnection with appropriate tools (open framework).
For this last point, the specific property analysis modules is realised by COSTO modules and the general property analysis are checked by connection with existing tools (Model-checking or theorem-proving).
This is illustrated on the ATM example for the behavioural compatibility property.
Its scope is correctness of components and assemblies compositions
availability of components and services, the 
compatibility of linked interfaces, the service compatibility and a diagnosis on mismatch.
The service compatibility is defined at four levels of control: service signatures, enhanced service interfaces, contracts (pre/post conditions), and the behaviours (correct interactions between the caller service and the called service via the required service).
An illustration with MEC an existing powerful model-checker for synchronised LTS.
MEC has a compatible definition of STS that allows a 
Systematic translation into input formalisms and feedback.
A verification is done for each triple of service based on an first level assembly link.
In the ATM example, a deadlock is detected and visualized.
~\\

\noindent\underline{Questions}~\\

Questions were asked all along this talk.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{Working Session}
\label{working_sessions}

\subsection{WS}

\paragraph{Position}

F. Plasil recalls that the ECONET project is a small project (budget, duration) - see the project goals in section \ref{econet:project}.
The contribution (
General remark
Output
Cross fertilization
Joint publication
Benchmark: CoCoME example
Available from www.cocome.org


Providing \sofa
STS/eLTS : enhancing EBP by additional features 
to enhance expressive power of  EBP 
Protocols (EBP) from code 
at least BP from code 
OCL: WFR for component diagrams, activity diagrams? 
WFR for \sofa components

Benchmark: CoCoME example
Available from www.cocome.org
or from Tomas Poch, …. 

\endinput

