ACTIVITIES:

Our activities have as a common ground the use of formal methods and techniques in the current practice of software development. Therefore the specific topics range from development and analysis of formalisms to the production of tools for system modelling support and to variations of industrially used techniques.

Starting with the Compass Working Group (Esprit Projects 3264 and 6112), in the late 80's, we have developed several algebraic formalisms, addressing problems raised by software specifications, like partiality and non-strictness of functions, or error-recovery.

In computer science, the conceptual needs posed by the proliferation of formalisms were first addressed by Goguen and Burstall, who proposed their theory of institutions as a general framework.

We have significantly contributed to the development of this theory, with a particular interest for relating, translating and composing different (algebraic) formalisms.

Moreover, we have developed a formalism, LTL (Labelled Transition Logic) for the specification of reactive\concurrent\parallel\distributed systems, both at the requirement and at the design level, extending to labelled transition systems the logical\algebraic specification method of abstract data types.

Building over this body of experience, we have played a significant role in the CoFI initiative, a group consisting of most researchers in algebraic techniques responsible for the definition of CASL, the Common Algebraic Specification Language, intended to be the academic standard.

Our group has been active in the Language Design, Semantics and Reactive Systems task groups.

Among the results of this latter task group we have the CASL-LTL, the CASL variant of LTL, and CASL-Chart, a variant of state charts, where the used data and the decorations of the transitions are given by using CASL.

The interest for the UML, started within the Reactive Systems task group, has led to the analysis of its semantic foundations, that are, so far, quite shaky, as shown by the number of papers in the literature addressing them.
In particular, the multiview nature of the UML actually poses new interesting challenges to the standard techniques to describe the semantics of more traditional languages.

Our contributions are an attempt at giving a precise meaning to UML diagrams in isolation in a way that can be composed to get the semantics of the overall UML models, both using traditional techniques, and investigating the feasability of the new "metamodelling" techniques.

The analysys of UML has also lead to propose some extensions to allow to better model particular aspects of a system.