The SE2C Experience on Automating the Design, Transformation and Verification of Models

by Paris Avgeriou, Nicolas Guelfi and Paul Sterges

The Software Engineering Competence Centre (SE2C) at the University of Luxembourg conducts cutting-edge research in the area of automated software engineering. Ongoing research is focused on partially automating the design of applications through architectural frameworks, the transformations of UML models, the reconciliation of architectural models and formal verification of models.

Automated software engineering is at the centre of SE2C's research activities. We are interested in providing development teams with tools that will automate, at least partly, the design of applications. We are particularly interested in model-driven software engineering related to the Unified Modeling Language (UML), and in automating the transition between the various models through transformations. We are also working in architecture-centric software development, where the design and transformation of architectural models play a key role in the development process. Finally we are aim at providing formal verification of models in application domains, such as e-business transactions. The current work of the SE2C includes a UML model transformation tool, an architectural framework, transformations of architectural models, and verification tools.

MEDAL (uMl gEneric moDel trAnsformer tooL) is a CASE Tool that supports an approach named Visual Model Transformation (VMT), and that aims at providing generic transformations of UML models. The VMT approach is based on graph transformation theory: each transformation rule defines a graphical pattern to be matched in the source model (known as 'left-hand side' (LHS)) and another graphical pattern depicting the resulting target model ('right-hand side' (RHS)). Both the LHS and RHS are defined using a visual notation plus additional properties that are expressed with a textual notation. Composite transformations can be synthesised from primitive transformations in order to provide a modular mechanism for defining reusable transformations of desirable complexity. The MEDAL Tool is an extension of IBM-Rational's XDE, an environment that supports round-trip engineering, and builds upon XDE's model server, OCL engine, and pattern engine.

The FIDJI architectural framework aims to automate the application of FIDJI: a model-driven, architecture-centric, framework-based software development process. The FIDJI architectural framework is comprised of a component-based application framework for the development of J2EE-based applications, and a CASE tool that assists the extension and customisation of the framework for specific applications. In this sense, development teams of individual projects can reuse the application framework, customize it and extend it so as to satisfy their own functional and quality requirements. The CASE tool assists them in designing the final application and in transforming this design model into a prototype implementation consisting of a UML implementation model, Java source code, configuration files, and deployment descriptors.

The DIAS project deals with the task of keeping the requirements and the implementation of a software system in sync. This is done by transforming two architectural models - one of which is based on requirements and the other on implementation - into a common model. It is commonplace that the gap between the requirements and the implementation of a software system cannot be bridged directly, but demands intermediate representations. From an architecture-centric viewpoint, these representations take the form of an ideal architectural model that conforms to the requirements, and a realistic architectural model that conforms to the implementation. Semi-automated support in this case is provided through a transformation that combines the two architectural models into a new model that represents a trade-off between the desired requirements and implementation constraints. This form of architectural reconciliation takes advantage of the aforementioned VMT approach and MEDAL tool. In the context of this project, SE2C is organising a workshop for architectural design and UML, hosted at the UML 2004 conference.

In the E-fficient project, SE2C is working on verification tools for e-business transaction descriptions. The descriptions, which are made in UML by business experts, mainly consist of activity diagrams showing a decomposition of transactions into a number of activities, and of class diagrams indicating the structure of the messages that are exchanged during the transactions by the participants. We are working on an automated verification tool that consists of plug-ins implemented inside a modelling tool. This tool verifies that the set of UML diagrams of a given transaction fulfils a number of predefined static, dynamic and real-time properties. In running this verification, our tool calls the following model checkers: USE, SPIN and Kronos. The properties to be verified are written in the various languages supported by the tools: OCL for USE, PROMELA for SPIN and TCTL for Kronos. This approach requires translating the UML-based description into formal descriptions for the different tools. The use of different tools allows a wide range of constraints to be specified, ranging from syntactical constraints to real-time constraints.

Links:
SE2C homepage: http://se2c.uni.lu
FIDJI Project: http://se2c.uni.lu/projects/fidji
DIAS Project: http://se2c.uni.lu/projects/dias
E-fficient Project: http://se2c.uni.lu/projects/efficient

Please contact:
Nicolas Guelfi, University of Luxembourg
Tel: +352 420 101 251
E-mail: nicolas.guelfiuni.lu