Towards the UML-Based Formal Verification of Timed Systems

  • Luciano Baresi
  • Angelo Morzenti
  • Alfredo Motta
  • Matteo Rossi
Part of the Lecture Notes in Computer Science book series (LNCS, volume 6957)


This paper presents the approach to the formal verification of UML-based models of timed systems developed in the MADES project. The approach differs from many current ones in that it aims at (i) being inclusive in the range of diagrams considered when producing the formal model, and (ii) adhering to the UML notation as much as possible. The metric temporal logic-based semantics developed in the project is presented through an example system.


Time Instant Temporal Logic Class Diagram Sequence Diagram State Diagram 
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.
    Baresi, L., Morzenti, A., Motta, A., Rossi, M.: D3.1 domain-specific and user-centred verification. Technical report, MADES Consortium (2010)Google Scholar
  2. 2.
    Baresi, L., Morzenti, A., Motta, A., Rossi, M.: D3.3 formal dynamic semantics of the modelling notation. Technical report, MADES Consortium (2011)Google Scholar
  3. 3.
    Bersani, M.M., Frigeri, A., Pradella, M., Rossi, M., Morzenti, A., San Pietro, P.: Bounded reachability for temporal logic over constraint systems. In: Proc. of the Int. Symp. on Temporal Representation and Reasoning (TIME), pp. 43–50 (2010)Google Scholar
  4. 4.
    Bouabana-Tebibel, T.: Semantics of the interaction overview diagram. In: Proc. of the IEEE Int. Conf. on Information Reuse Integration (IRI), pp. 278–283 (2009)Google Scholar
  5. 5.
    Burmester, S., Giese, H., Hirsch, M., Schilling, D., Tichy, M.: The fujaba real-time tool suite: model-driven development of safety-critical, real-time systems. In: Proc. of the 27th Int. Conf. on Soft. Eng., ICSE 2005, pp. 670–671 (2005)Google Scholar
  6. 6.
    Cengarle, M.V., Knapp, A.: Operational semantics of UML 2.0 interactions. Technical Report TUM-I0505, Technische Universität Mnchen (2005)Google Scholar
  7. 7.
    Ciapessoni, E., Coen-Porisini, A., Crivelli, E., Mandrioli, D., Mirandola, P., Morzenti, A.: From formal models to formally-based methods: an industrial experience. ACM TOSEM 8(1), 79–113 (1999)CrossRefGoogle Scholar
  8. 8.
    Damm, W., Josko, B., Pnueli, A., Votintseva, A.: A discrete-time uml semantics for concurrency and communication in safety-critical applications. Sci. Comput. Program. 55, 81–115 (2005)MathSciNetCrossRefzbMATHGoogle Scholar
  9. 9.
    Diethers, K., Huhn, M.: Vooduu: Verification of object-oriented designs using uppaal. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 139–143. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  10. 10.
    Eshuis, R.: Symbolic model checking of UML activity diagrams. ACM Trans. Softw. Eng. Methodol. 15(1), 1–38 (2006)CrossRefGoogle Scholar
  11. 11.
    Eshuis, R., Wieringa, R.: Tool support for verifying UML activity diagrams. IEEE Trans. Software Eng. 30(7), 437–447 (2004)CrossRefGoogle Scholar
  12. 12.
    Hammal, Y.: A formal semantics of uml statecharts by means of timed petri nets. In: Wang, F. (ed.) FORTE 2005. LNCS, vol. 3731, pp. 38–52. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  13. 13.
    Hansen, H., Ketema, J., Luttik, B., Mousavi, M., van de Pol, J.: Towards model checking executable uml specifications in mcrl2. Innovations in Systems and Software Engineering 6, 83–90 (2010)CrossRefGoogle Scholar
  14. 14.
    Object Management Group. UML Profile for Modeling and Analysis of Real-Time Embedded Systems. Technical report, OMG, formal/2009-11-02 (2009)Google Scholar
  15. 15.
    Object Management Group. OMG Systems Modeling Language (OMG SysML). Technical report, OMG, formal/2010-06-01 (2010)Google Scholar
  16. 16.
    Object Management Group. OMG Unified Modeling Language (OMG UML), Superstructure. Technical report, OMG, formal/2010-05-05 (2010)Google Scholar
  17. 17.
    Pradella, M., Morzenti, A., San Pietro, P.: The symmetry of the past and of the future: bi-infinite time in the verification of temporal properties. In: Proceedings of ESEC/SIGSOFT FSE, pp. 312–320 (2007)Google Scholar
  18. 18.
    Pradella, M., Rossi, M., Mandrioli, D.: ArchiTRIO: A UML-compatible language for architectural description and its formal semantics. In: Wang, F. (ed.) FORTE 2005. LNCS, vol. 3731, pp. 381–395. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  19. 19.
    Saldhana, J.A., Shatz, S.M.: Uml diagrams to object petri net models: An approach for modeling and analysis. In: Proc. of SEKE 2000, pp. 103–110 (2000)Google Scholar
  20. 20.
    Störrle, H., Hausmann, J.H.: Towards a formal semantics of UML 2.0 activities. In: Software Engineering. Lec. Not. in Inf, vol. 64, pp. 117–128 (2005)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2011

Authors and Affiliations

  • Luciano Baresi
    • 1
  • Angelo Morzenti
    • 1
  • Alfredo Motta
    • 1
  • Matteo Rossi
    • 1
  1. 1.Dipartimento di Elettronica e Informazione, Deep-SE GroupPolitecnico di MilanoMilanoItaly

Personalised recommendations