[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
CoFI-Reactive meeting/Paris/18-20 June' 99/minutes
CoFI WG
Working Meeting of the CoFI-Reactive Task Group in Paris, 18-20 June, 1999
Organization and location
The meeting was organized by Christine Choppy (Paris 13) and Francoise
Tort (CNRS-Cachan).
The first two days have been hosted at Universite' Paris7,Jussieu;the last
day at
ENS -Cachan.
The organization was perfect; even the weather looked carefully planned
with a magnificent sun faded by some clouds only at the very end of the
meeting.
Participants
Egidio Astesiano,Hubert Baumeister,Maura Cerioli,Christine Choppy,Heinrich
Hussmann,Alexander Knapp,Piotr Kosiuczenko,Gianna Reggio,Francoise Tort.
Agenda
A. Choice of a UML subset
B.Technical discussion on the semantic modelling of UML,the constraint
language and its relationship to CoFI-CASL (Static part)
C.Technical discussion on the semantic modelling of UML and its
relationship to CoFI-CASL(Dynamic part)
D.Revision of the working plan
============
A. Choice of a UML subset
Static Part
A preliminary document by Francoise Tort was presented and revised.
Dynamic part
There was a discussion confined to the State diagrams part, based on the paper
submitted to UML'99.
B. Technical discussion on the semantic modelling of UML and its
relationship to CoFI-CASL (Static part)
The discussion was aimed at reaching some tentative conclusions about
the directions of the work. Below are the current conclusions.
1. To take a global view of a UML model and to derive more local views
from it.
2. Underlying UML models include a (global) state possibly algebraically
specified. This state includes both global and local views to support
the most convenient way of presenting specifications.
(Using the following definitions: "UML systems” = systems specified by
UML models; "Underlying UML models (shortly U-UML models)” = formal
structures for specifying UML systems)
Remark: Look at this methodological issue and derive technical
consequences.
3. First attempt (waiting for confirmation through experimentation):
sorts include
- global state
- local state (for each class)
- selectors for attributes and associations in two forms
Question: Which induction principle?
4. For inheritance, we assume that the Liskov substitution principle is
enforced strictly,as it results the current official "semantics' of UML.
This means that constraints are inherited from
superclass to subclass.
5. There was a discussion whether the translation from UML to CASL will
be a function or a relation, and whether it will be compositional and
incremental. This is related to the question whether UML diagrams can be
incomplete. In the case of complete UML models, there is a belief that
there is a "natural” translation that is a function. After a long
discussion, UML models in general should be considered as complete, so
it seems that the semantic transformation is a function.
6. As soon as we are stating a "closed frame assumption” on the local
state of a set of objects, we are imposing the corresponding method to
be atomic (i.e. non-interruptable) and mutually exclusive with any other
action that can be performed on the same set of objects. Discussion of
syntactic representation of frames is postponed until after we have some
experience with examples.
7. In order to admit concurrent execution of methods, the signature of
operations can no longer result in a global state. One possible solution
is to have a state transformer as the result of the method.
8. When specifying axioms (for operations) in terms of state
transformers, preconditions are needed to restrict the states for which
the transformation axiom is applied.
9. We want to define a shorthand notation as much implicit as possible,
near to OCL, but with a precise meaning by translation into CASL. It may
be useful to look at the treatment of state-based systems in Haskell.
Technical remarks:
- Sort "Person” to be used where "PersonId” was used in the UML99/ADT
paper.
- Sort "PersonState” to be used where "PersonObj” was used in the
UML99/ADT paper.
- Inheritance modelled by subsorting: Employee < Person and
EmployeeState < PersonState
Task to be done (see also workplan below):
- Look at examples for CASL-annotated UML specifications in our
framework, explore possibilities (translation of OCL, enhancement of OCL
etc.)
C. Technical discussion on the semantic modelling of UML and its
relationship to CoFI-CASL(Dynamic part)
Gianna Reggio gave a presentation of the general underlying model (U-UML
model),based on the representation of the processes as labelled transition
systems (or equivalently general automata), but excluding collaboration.
* Generalities on the U-UML model
We choose as U-UML model a Labelled Transition System
(STATE,LABEL,-->)
where
STATE will be the structure already determined by the class diagram (see
above)
and also LABEL will be defined as an algebraic specification.
The active objects (objects of active classes, i.e., processes with an
indipendent execution thread)
will be in turn modelled by a labelled transition system
(STATE-a,LABEL-a,-->a)
where the STATE-a will be just the local views corresponding to active
objects of
the global states (STATE).
The execution and collaboration diagrams, the communication structure of
UML, the parallelism among the components of the UML-systems will determine
the transitions of the global labelled transition systems (-->) starting
from the transitions of the active components (-->a) and the local views
corresponding to the
nonactive objects of the global states.
* Active classes with associated state machine
assumptions on (STATE-a,LABEL-a,-->a)
* LABEL-a
They fully describe the interface of the active objects towards their
external environment (the other objects compsing the system)
and are a set/multiset of the following elementary parts
- input
to receive a signal
to receive an operation call
to have an attribute updated
to be destroyed
to receive the actual time *
- output
to send a signal
to call an operation
to update an attribute of a different object
to create destroy another object
(* this will be present in any label)
* STATE-a
they should record the following information
- actual values of the attributes
- event queue (queue is the official UML terminology, but it is just a
multiset)
- history
- whether the object is locked or not (to handle the ``run to completion''
way of executing the transitions)
- set of the states of the threads corresponding to concurrent ``states''
of the state machine
* -->a
it will be determined by the transitions of the state machine and by the
operations and signals of the class
D.Workplan
Meetings
-WADT: there will be a session with some papers and a report on the work of
the TG by Heinrich (replacing Egidio,not participating in WADT)
-It is felt that at the WADT there will not be enough time for a serious
technical meeting,nor it will be possible to hold it at the FM'99 the
following week. So it would seem reasonable to try to organize it in
Dagstuhl in November 7-12, during a seminar to which most of the people
here in Paris are already invited, asking Martin Wirsing about the
possibility of few more participants.
-Consequently the Genova scheduled meeting should take place in February 2000.
Task T1: Choice of UML subset
- Static part.
There is a preliminary draft of a document by Francoise, which was
reviewed at the meeeting. A new version will be sent out to the CoFI-UML
list by Francoise.
-Dynamic part.
A first part on state diagrams by Gianna Reggio is due before the end of June .
The other parts will be covered at the end of the summer; anyway before the
Dagstuhl meeting (if any).
Task T2: Modelling and semantics
It was decided to produce notes, with a three step procedure: production by
authors (with people in charge of reading the draft version); discussion
within CoFI-UML subgroup;circulation among official CoFI-Reactive.
Static part: Authors of a draft CoFI note are Heinrich Hussmann, Maura
Cerioli, Hubert Baumeister, readers are Alexander Knapp, Christine
Choppy. Technical editor: Maura Cerioli.
- First rough internal draft to other authors by Maura: end of June
- First version to the readers: July 16
- Official note to be available: September 6
- Dynamic part: The involved persons are Gianna Reggio, Christine
Choppy, Egidio Astesiano; readers are Pjotr Kosiuczenko and Heinrich Hussmann.
The updated part related to the State diagrams should be ready before
Dagstuhl. In parallel there should be a preliminary note on collaborations.
Task T3: Constraint language
Static part
- During task 2, the applicability for specifying constraints should be
checked.
- Involved people are Francoise Tort, Maura Cerioli, Heinrich Hussmann,
Hubert Baumeister.
- Appendix to note from task 2 to be produced, starting mid July,
readable draft September 6.
Task T4: Case studies
- Not a large-scale case study to be produced, but illustrative examples
giving methodological guidance with the goal to be incorporated into the
general "user guide”.
Related topics
Two presentations on related topics, thoguh not part of the work of the
groupo were presented and discussed.
- Alexander Knapp on "Generating Maude specifications from
UML collaborations"
- Francoise Tort on "Correct realizations of interface
constrains with OCL"
Prof. Egidio Astesiano
Director
Dipartimento di Informatica e Scienze dell'Informazione (DISI )
Universita' di Genova-Italia
Postal address
DISI-Universita' di Genova
Via Dodecaneso 35
16146 Genova
Italy
Phone ++ 39 010 353 6703 (direct)/6646 (answering machine)
Secr. ++39 010 353 6701 (Elli Ferrando;10am to 1 pm-2pm to 6pm))
Fax ++ 39 010 353 6699
Mobile ++ 39 (0)335 8084769
e-mail astes@disi.unige.it
http://www.disi.unige.it