Rigorous Open Development Environment for Complex Systems - RODIN

by Alexander Romanovsky

The RODIN project will create a methodology and a supporting open tool platform for the cost-effective rigorous development of dependable complex software systems and services.

RODIN is a strategic targeted research project which falls squarely within the remit of the strategic objective ‘Open Development Platforms for Software and Services’ of the IST FP6 second call. RODIN focuses on tackling complexity caused by the environment in which the software is to operate and which comes from poorly conceived architectural structure.

Mastering complexity requires design techniques that support clear thinking and rigorous validation and verification. Formal design methods do so. Coping with complexity also requires architectures that are tolerant of faults and unpredictable changes in environment. This is addressed by fault tolerance design techniques.

The project is developing a unified methodology combining formal methods with fault tolerance design principles by using a systems of systems approach, where both software and environment are modelled together.

We are tackling complex architectures: our systems approach supports the construction of appropriate abstractions and provide techniques for their structured refinement and decomposition.

The project ensures cost effectiveness, the methods and platform support reuse of existing software. RODIN thus extends existing formal methods with generic mechanisms to support component reuse and composition.

Tool support for construction, manipulation and analysis of models is crucial and we concentrate on a comprehensive tool platform which is openly available and openly extendable and has the potential to set a European standard for industrial formal methods tools.

The methods and platform are validated and assessed through industrial case studies.

The novel aspects of this project are the pursuit of a systems approach, the combination of formal methods with fault tolerance techniques, the development of formal method support for component reuse and composition and the provision of an open and extensible tools platform for formal development. In particular, we believe that the open tools platform will have a significant impact on future research in formal method tools and will encourage greater industrial uptake.

The interplay between methods, tools and case studies is at the heart of the RODIN plan.

To achieve the RODIN objectives the research and development are being directed by the following criteria:

• The methods and platform should support a systems approach to software development.
• The methods and platform should support the development of systems that are tolerant of faults and unpredictable changes in the environment.
• The methods and platform should support reuse of existing software developments.
• The tools supporting the methods should be integrated on a single platform which should be open to extension by other parties.
• The methods and platform should be properly validated and assessed through industrial case studies.

Case Studies
The methods and platform are being validated and assessed through industrial case studies:

• Formal Approaches to Protocol Engineering
• Engine Failure Management System
• Formal Techniques within an MDA Context
• CDIS Air Traffic Control Display System
• Ambient Campus.

The aim is to produce the RODIN methodology for rigorous development of complex systems. To achieve this aim the project is making advances in basic research areas related to system modelling and mapping of models, software reuse, and formal reasoning about system fault tolerance, reconfiguration, mobility and adaptivity.

This includes development of templates for fault tolerant design methods (atomic actions, exception handling, compensation), as well as for reconfigurability, adaptivity and mobility.
An open tool kernel is built as a set of basic kernel tools implemented on a platform that can be extended by plug-ins. Openness and generality of the platform are the primary aim of the development. The work is being carried out in the Eclipse environment.

RODIN is developing a range of tools to support the application of the RODIN methodology
The overall objective of RODIN leads to the following specific measurable outcomes:

• a collection of reusable development templates (models, architectures, proofs, components) produced by the case studies
• a set of guidelines on a systems approach to the rigorous development of complex systems, including design abstractions for fault tolerance and guidelines on model mapping, architectural design and model decomposition
• an open tool kernel supporting extensibility of the underlying formalism and integration of tool plug-ins
• a collection of plug-in tools for model construction, model simulation, model checking, verification, testing and code generation.

Consortium
The consortium includes:

• University of Newcastle upon Tyne (UK) - Coordinator
• Aabo Akademi University (Finland)
• ClearSy System Engineering (France)
• Nokia Corporation (Finland)
• Praxis Critical Systems Ltd (UK)
• AT Engine Controls Ltd (UK)
• Swiss Federal Institute of Technology Zurich (Switzerland)
• University of Southampton (UK).

Two major RODIN events:

• Workshop on Rigorous Engineering of Fault Tolerant Systems, 19 July 2005, associated with Formal Methods (FME) 2005, Newcastle upon Tyne, UK
• RODIN Open Industry Day, 5 April 2006, Aix en Provence, France.

Link:
http://rodin.cs.ncl.ac.uk/

Please contact:
Alexander Romanovsky
University of Newcastle upon Tyne, UK
Tel: 44 191 222 8135
E-mal: Alexander.Romanovskyncl.ac.uk