Minutes of Genova workshop last weekend

[hussmann@inf.tu-dresden.de]

Dear colleagues,

please find enclosed the minutes of the CoFI-reactive workshop which was
held in Genova last weekend. As you can see, the meeting went well and
was quite effective.

Many thanks again to the Genova people for their splendid hospitality!

Best regards
Heinrich

--
Minutes of the CoFI-R Meeting in Genova, 5 Feb - 7 Feb 2000

Start: 5 Feb 2000, 14:30
End: 7 Feb 2000, 13:00

Participants: Egidio Astesiano, Hubert Baumeister, Maura Cerioli,
Christine Choppy, Heinrich Hussmann, Gianna Reggio, Markus Roggenbach,
Pippo Scollo, Alexandre Zamulin (5-6 Feb), Elena Zucca

Moderation: Egidio Astesiano/Heinrich Hussmann

Minutes: Heinrich Hussmann

Topic list:
1. Presentations and discussion
2. Discussion on draft papers
3. Methodological comparison between CASL extensions
4. Tools discussion
5. Organization and schedule


1. Presentations and Discussion
-------------------------------

The following presentations were made and discussed:

1.1. Gianna Reggio: CASL-LTL - A CASL extension for dynamic systems
 
This is joint work with Egidio Astesiano and Christine Choppy. 
An internal draft document is available and will be pulsihed on the
CoFI-R Web pages as soon as the revisions decided in this meeting are integrated.

The following issues were raised in the discussion:

(CL-1) The concrete syntax is not yet very user-friendly, in particular
regarding "dtype" and "Label_XX". Suggestions for improvement are sought.

(CL-2) The need of a semantic extension compared to syntactic shorthands
(macros) on top of CASL is not very clear in the paper. Good arguments
for the need of a semantic extension were given in the discussion, but
these need to be written down in the paper.

(CL-3) Give more details on the semantics of processes (CCS example),
including an explicit reference to Milner's book.

(CL-4) Add the "buffer example" in a CASL-LTL formulation.

(CL-5) Add a reference to the classification given in the article of the
IFIP book. Clarify in the introduction which variant is followed. Add a
reference to the comparison with other approaches which is given in the
full version.

(CL-6) Work out the methodological spects. Related to SB-3 below.

The overall decision was that a revised version of this extension shall
be submitted to the Language Design group in time for the Berlin workshop.


1.2. Hubert Baumeister: State-based extension for CASL

This is joint work with Alexandre Zamulin, which takes place in the
intersection between CoFI-Reactive and CoFI-Language Design. There is no
paper available yet, just a set of slides. A draft paper on teh
theoretcial background is available from the authors.
The basic idea is the "state as algebra" approach as used in ASMs. The
axioms are more general than just operational definitions.

The following issues were raised in the discussion:

(SB-1) Write it down as a CoFI note.

(SB-2) Coordinate the list of proposed extensions with Bernd Krieg-Brueckner.

(SB-3) Give some indications which of the (incompatible!) extensions to
be used for which practical purposes, from a methodological viewpoint.

In addition to this general discussion, there was a meeting of the
authors (held in parallel to other meetings on 6 Feb), where a detailed
review of 
the draft paper took place. The main decisions were as follows: 

- Extend the draft with the formal foundation of post-conditions
- Clarify the semantics of call-by-reference parameters
- Present a CoFI note at the CoFI meeting in Berlin


1.3. Gianna Reggio: CASL-Charts

This is joint work with L. Repetto. There are two papers available: 
- Technical Report DISI-TR-00-2 (ftp://ftp.disi.unige.it/person/ReggioG/ReggioRepetto00b.ps)
- Draft CoFI document "CASL-Chart: Syntax and Semantics".
(ftp://ftp.disi.unige.it/person/ReggioG/ReggioRepetto00a.ps)
The following issues were raised in the discussion:

(CS-1) Decide whether CASL-Charts will be further developed towards UML
statecharts and LTL-based semantics. 

(CS-2) To be submitted to the Language group, but with a "preface"
explaining that the status of this extension is for CoFI-internal
purposes mainly (to demonstrate the potential of CASL), but not to
become part of the "official" CASL.

(CS-3) Semantics is currently defined in a style different from the
standards of the CASL semantics definition. In order to homogenize the
styles,  somebody from the semantics group has to team up with Gianna.
This has to be clarified with the semantics group.


1.4 Markus Roggenbach: CSP & CASL

Markus Roggenbach presented some general ideas about work in Bremen on
the combination of CSP and CASL. An advantage of such a combination
could be that there are tools available for CSP as well as for CASL,
which build on the same software platform (Isabelle).
Further discussion of this issue will take place at the Berlin workshop.


2. Discussion on Draft Papers
-----------------------------

2.1. CoFI-R Study Note "From UML to CASL (Static Part)"

This is joint work by Hubert Baumeister, Maura Cerioli and Heinrich Hussmann.
A draft paper, mainly resulting from the discussions at the Paris
meeting, is available.
The following general issues were raised in the discussion:

(US-1) Why don't we use the state-based extension? 
The answer to this question is twofold. First, the model developed here
shall be used for developing a semantics of dynamic aspects, including
detailed questions of concurrency and synchronization. In its current
form, the state-based extension is not well-suited for this purpose.
Second, the actual formalism used to map class diagrams to CASL is only
of minor relevance, since such a translation should not be made visible
to the users/specifiers. Essentially, the user will write CASL
constraints using the assumption of an implicit state.

(US-2) Can update operations be modelled as CASL functions?
Semantically, it is difficult if not impossible to do the formal
transition from separate sequential specifications to a proper
specification of concurrent executions. So it seems not feasible to
interpret an operation as a function on a local state. However,
specifiers want to ignore the aspects of concurrency, as long as they
are doing static modelling, and deal with these separately in a later
step. Therefore, it was decided to model update operations as binary
relations on states, in order to allow for concurrent updates of
unaffected parts of the state.  When linking static and dynamic
semantics, these relations will be mapped onto predicates in the
temporal logic language LTL.

In addition to this general discussion, there was a meeting of the
authors (held in parallel to other meetings), where a detailed review of
the draft paper took place. The main decisions were as follows:
- The specification will be brought into observational style, leading to
significant simplifications. Examples will be included, how constructor
operations can be specified.
- The section dealing with "effect" expressions will be removed.
- A new and almost final version of the paper will be made available
soon, i.e. within the next few weeks.


2.2. CoFI-R Study Note "From UML to CASL (Dynamic Part)"

This is joint work by Gianna Reggio, Christine Choppy and Heinrich Hussmann.
The main technical contents is a semantics for UML statecharts within
CASL-LTL. 
A conference paper has been accepted for FASE 2000, the final version is
available. The study note will consist in an extended version of this
paper, for which a draft is also available.

In an authors' meeting (held in parallel to other meetings), a review of
the draft paper was carried out.


2.3. Combining Static and Dynamic Aspects

There is no paper available yet on the final goal, which is to combine
static and dynamic semantics. 
The basic idea is to give an overall formal model of a UML system as a
loose CASL-LTL specification and to show how the various diagrams define
additional constraints on the loose specification. On the specification
level, this means an integration of CASL-annotated class diagrams
(giving e.g. pre- and postconditions to operations) with UML statecharts
for the individual classes. But also other diagrams (e.g. sequence
diagrams, on which some work is ongoing) and passive objects have to be included.

The work towards a concrete paper will be initiated by Gianna and Maura,
who will write a first outline and draft.

In this context, another idea came up which is a UML "profile" (i.e. the
official mechanism for variants of the plain UML) with formal
justification (preliminary name "preferred precise semantics"). Further
discussion on this idea was delayed to the Berlin meeting.


3. Methodological comparison between CASL extensions
----------------------------------------------------

A first brainstorming session took place where some thoughts from the
LTL point of view were collected to compare the state-based extension
and the LTL extension, i.e. items SB-3 and CL-6 from above. Due to
organisational restrictions, the people representing the state-based
extension could not attend this discussion.

The following results were achieved:
- Basically, the two approaches may be seen as technically equivalent.
The difference appears to be in the applicability.
- Applications dealing with concurrency and synchronisation may be
better suited for the LTL approach.
- The suitability is influenced by concurrency architecture. E.g. when
branching is relevant, stream-processing functions are not adequate. A
similar effect may appear here.
- Claim (by Gianna): State-based approach is adequate for purely
sequential oo programming.

The discussion has to be continued involving more people, in particular
the authors of the state-based extension of CASL.


4. Tools discussion
-------------------

In a short discussion, the situation regarding tools for the approaches
of this group was summarized.
There are the following main issues:
(T-1) For the LTL approach, there are no tools, not even independent of
CASL. This, of course, makes it completely unrealistic to achieve any
tool support within the CoFI runtime.
(T-2) For interfacing to UML editors, techniques have been developed and
prototype tools are available at TU Dresden. However, there remains the
question of "round-trip engineering": A translation from UML into a
formal specification should be reversible to reflect changes made on the
formal specification back into the UML specification.


5. Organization and schedule
----------------------------

5.1 Berlin meeting

There will be a CoFI meeting on April 1 and 2, beginning with a "public" part.
Since time at this meeting will be limited and Christine will be not
available on April 2, it was suggested to have a working meeting during
the ETAPS week. Thursday, March 30, is a candidate date. Heinrich will
further investigate the possibilities for such a meeting. (Additional
information: The meeting of the ETAPS steering committee is on
Wednesday, March 29, at lunchtime.)
Heinrich and Egidio will discuss with the CoFI coordinators when and how
to present the state of CoFI-Reactive in the public part of the meeting.

5.2 Edinburgh meeting

Heinrich shall clarify details about Edinburgh meeting with Don.
(Preliminary result of email conversation with Don: The current time
frame is one week within August 28 - September 22).

5.3 Publicity

An extended version of the FASE paper should be submitted to  a journal (Gianna).
Future plan: Hold a workshop on UML+CASL at OOPSLA 2001.