Our activities have as a common ground the use of
formal methods and techniques in the current practice of software
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
Moreover, we have developed a formalism, LTL (Labelled Transition Logic)
for the specification of
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
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
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.