HRT-UML

Mission

The Hard Real-Time Unified Modeling Language (HRT-UML) method, and the supporting toolset, aims to provide a comprehensive solution to the modeling of hard real-time and dependable systems and their early verification, according to rigorous techniques based on formal theories, such as schedulability analysis, formal verification and quantitative evaluation of dependability attributes and simulation.

Description

HRT-UML defines a customized version of UML to express the HRT-HOOD methodology, making the most of both standards and also capturing and compensating for the respective weaknesses. The resulting design method, and the support toolset, permits static scheduling analysis of the system and also caters for automated generation of consistent Ada 95 code that complies with the Ravenscar Profile and C code for standard OSEK/VDX RTOSs.
A relevant aspect of HRT-UML is the integration of design activities with selected methods for the development of dependable systems. The approach is to assist the designer by offering an appropriate design methodology, and a support toolset, that integrates dependability validation techniques based on formal verification of system behavioral properties by model-checking, modeling of dependability aspects and well established techniques for quantitative assessment of system dependability attributes, automatic translations from the design to the mathematical models and the analysis tools tools that are most appropriate for the different kinds of validation, the SPIN model-checker and the Möbius behaviour modelling tool.

Support is offered by HRT-UML also for the development of systems with control aspects, by integrating major lifecycle activities such as functional control design, software/hardware architecture design, and validation through analysis and co-simulation

HRT-UML Design Principles

The focus of an HRT design is not the definition of classes but rather the set of objects that compose the system and their interconnections. interacting objects are organized in a structure according to the following principles:

• Object Modeling Prevalence
• Multiple Static Instances
• Hierarchical Decomposition
• User-Provider Relationships

Moreover, it is possible to associate timing and dependability tags to objects, so as to enable schedulability and dependability analysis.

Merging the UML and HRT-HOOD methods with dependability

The experience shows that the design of Hard Real-Time systems needs methodologies suitable for the modeling and analysis of aspects related to time, schedulability, performance, and RAMS (Reliability, Availability, Maintainability, Safety). In the context of the European Aerospace community a reference method for design is HOOD and particularly its extension for the modeling of hard real time systems, Hard Real-Time-HOOD (HRT-HOOD), recommended by the European Space Agency (ESA) for the development of on-board systems. On the other hand in recent years the Unified Modeling Language (UML) has been gaining a very large acceptance in a wide range of domains, all over the world, becoming a de-facto international standard.

A major extension of HRT-UML is the integration of design activities with selected methods for the development of dependable systems and for control design. The design method, and the support toolset, integrate validation techniques based on formal verification of system behavioral properties by model-checking, modeling of dependability aspects and well established techniques for quantitative assessment of system dependability attributes, automatic translations from the design to the analysis tools (SPIN and Möbius) that are the most appropriate for the different kinds of validation.

Implementation constraints

The Toolset has been developed entirely using Java. HRT-UML can be installed on Windows and Linux based systems. According to the Java technology portability, it is possible to migrate to other open systems with a limited effort.

To use the Toolset, the following software packages should be previously installed:

• Java Runtime Environment
  
• Cygwin environment (Linux emulator, for Windows only) (for schedulability analysis)
  
• SPIN (for formal verification)
  
• MOBIUS (for quantitative evaluation)

No particular performance hardware requirements apply. It is only suggested to run HRT-UML Toolset with at least 128MBs of RAM memory.

The HRT-UML toolset does not includes the SPIN and Möbius tools, they have to be procured separately

Maturity

Developed through R&D projects co-funded by the Italian Space Agency and the EC, HRT-UML evaluation and enhancements activities were supported by the European Space Agency Research and Technology Centre.

HRT-UML has already been widely employed by representative industries from the European space software community.