A UML2 Profile for Reusable and Verifiable Software Components for Real-Time Applications

  • V. Cechticky
  • M. Egli
  • A. Pasetti
  • O. Rohlik
  • T. Vardanega
Part of the Lecture Notes in Computer Science book series (LNCS, volume 4039)


Software frameworks offer sets of reusable and adaptable compo-nents embedded within an architecture optimized for a given target domain. This paper introduces an approach to the design of software frameworks for real-time applications. Real-Time applications are characterized by functional and non-functional (e.g. timing) requirements. The proposed approach separates the treatment of these two aspects. For functional issues, it defines an extensible state machine concept to define components that encapsulate functional behaviour and offer adaptation mechanisms to extend this behaviour which warrant preservation of the functional properties that characterize the framework. For timing issues, it defines software structures that are provably endowed with specific timing properties and which encapsulate functional activity in a way that warrants their enforcement. A UML2 profile is defined that formally captures both aspects and allows the proposed strategy to be deployed at design level.


State Machine Software Framework UML2 Class Diagram State Chart Framework Component 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Pasetti, A.: Software Frameworks and Embedded Control Systems. LNCS, vol. 2231, p. 29. Springer, Heidelberg (2002)zbMATHCrossRefGoogle Scholar
  2. 2.
    Wang, F.: Formal verification of timed systems: A survey and perspective. Proceedings of the IEEE 92(8), 1283–1305 (2004)CrossRefGoogle Scholar
  3. 3.
    Cechticky, V., Pasetti, A., Rohlik, O., Schaufelberger, W.: XML-Based Feature Modelling. In: Bosch, J., Krueger, C. (eds.) ICOIN 2004 and ICSR 2004. LNCS, vol. 3107, pp. 101–114. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  4. 4.
    Cechticky, V., Pasetti, A., Rohlik, O., Vardanega, T.: Automated proof-based System and Software Engineering for Real-Time Applications: Framework Design Report. Technical Report (2005) Available at ASSERT project website:
  5. 5.
    Cechticky, V., Pasetti, A., Rohlik, O.: The Model-to-Code Transformation Project website,
  6. 6.
    ISO SC22/WG9: Ada Reference Manual. Language and Standard Libraries. Consolidated Standard ISO/IEC 8652:1995(E) with Technical Corrigendum 1 and Amendment 1 (Draft 16) (2006) Available at,
  7. 7.
    Mazzini, S., D’Alessandro, M., Di Natale, M., Lipari, G., Vardanega, T.: Issues in Mapping HRT-HOOD to UML. In: Proc. 15th Euromicro Conference on Real-Time Systems, July 2003, pp. 221–228. IEEE, Los Alamitos (2003)CrossRefGoogle Scholar
  8. 8.
    Mazzini, S., D’Alessandro, M., Di Natale, M., Domenici, A., Lipari, G., Vardanega, T.: HRT-UML: Taking HRT-HOOD onto UML. In: Rosen, J.-P., Strohmeier, A. (eds.) Ada-Europe 2003. LNCS, vol. 2655, pp. 405–416. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  9. 9.
    Vardanega, T., Di Natale, M., Mazzini, S., D’Alessandro, M.: Component-Based Real-Time Design: Mapping HRT-HOOD to UML. In: Proc. 30th Euromicro Conference, pp. 6–13. IEEE CS Press, Los Alamitos (2004)CrossRefGoogle Scholar
  10. 10.
    Vardanega, T., Zamorano, J., de la Puente, J.A.: On the Dynamic Semantics and the Timing Behaviour of Ravenscar Kernels. Real-Time Systems 29(1), 59–89 (2005)zbMATHCrossRefGoogle Scholar
  11. 11.
    Goodenough, J., Sha, L.: The priority ceiling protocol: a method for minimizing the blocking of high priority Ada Tasks. Technical Report SEI-SSR-4, Software Engineering Institute, Pittsburgh, Pennsylvania (1988)Google Scholar
  12. 12.
    Dijkstra, E.: Guarded commands, nondeterminacy and formal derivation of programs. CACM 18(8), 453–457 (1975)zbMATHMathSciNetGoogle Scholar
  13. 13.
    Bordin, M., Vardanega, T.: Automated Model-based Generation of Ravenscar-compliant Source Code. In: Proc. 17th Euromicro Conference on Real-Time Systems, July 2005, pp. 69–77. IEEE, Los Alamitos (2005)Google Scholar
  14. 14.
    Bordin, M., Vardanega, T.: A New Strategy for the HRT-HOOD to Ada Mapping. In: Vardanega, T., Wellings, A.J. (eds.) Ada-Europe 2005. LNCS, vol. 3555, pp. 51–66. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  15. 15.
    Ober, I., Graf, S., Ober, I.: Validating timed UML models by simulation and verification. STTT. Int. Journal on Software Tools for Technology Transfer (2005)Google Scholar
  16. 16.
    Latella, D., Majzik, I., Massink, M.: Automatic verification of a behavioral subset of UML statechart diagrams using the SPiN model-checker. Formal Aspects of Computing (11) (1999)Google Scholar
  17. 17.
    Packet Utilization Standard, European Space Agency, ESA PSS-07-101 (ECSS version ECSS-E-70-41). Available from:

Copyright information

© Springer-Verlag Berlin Heidelberg 2006

Authors and Affiliations

  • V. Cechticky
    • 1
  • M. Egli
    • 1
  • A. Pasetti
    • 1
  • O. Rohlik
    • 1
  • T. Vardanega
    • 2
  1. 1.Institut für Automatik, ETH-ZentrumZürichSwitzerland
  2. 2.Dept. of Pure and Applied MathematicsUniversity of PaduaPadovaItaly

Personalised recommendations