Specifying UML Protocol State Machines in Alloy

  • Ana Garis
  • Ana C. R. Paiva
  • Alcino Cunha
  • Daniel Riesco
Part of the Lecture Notes in Computer Science book series (LNCS, volume 7321)


A UML Protocol State Machine (PSM) is a behavioral diagram for the specification of the external behavior of a class, interface or component. PSMs have been used in the software development process for different purposes, such as requirements analysis and testing. However, like other UML diagrams, they are often difficult to validate and verify, specially when combined with other artifacts, such as Object Constraint Language (OCL) specifications. This drawback can be overcome by application of an off-the-shelf formal method, namely one supporting automatic validation and verification. Among those, we have the increasingly popular Alloy, based on a simple relational flavor of first-order logic. This paper presents a model transformation from PSMs, optionally complemented with OCL specifications, to Alloy. Not only it enables automatic verification and validation of PSMs, but also a smooth integration of Alloy in current software development practices.


UML OCL Protocol State Machines Alloy 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Anastasakis, K.: A Model Driven Approach for the Automated Analysis of UML Class Diagrams. Ph.D. thesis, University of Birmingham (2009)Google Scholar
  2. 2.
    Anastasakis, K., Bordbar, B., Georg, G., Ray, I.: On challenges of model transformation from UML to Alloy. Software and Systems Modeling 9(1), 69–86 (2008)CrossRefGoogle Scholar
  3. 3.
    de Andrade, F.R., Faria, J.P., Paiva, A.C.R.: Test generation from bounded algebraic specifications using alloy. In: ICSOFT (2), pp. 192–200 (2011)Google Scholar
  4. 4.
    ATLAS: ATLAS Transformation Language, LINA&INRIA (2009)Google Scholar
  5. 5.
    Bauer, S.S., Hennicker, R.: Views on Behaviour Protocols and Their Semantic Foundation. In: Kurz, A., Lenisa, M., Tarlecki, A. (eds.) CALCO 2009. LNCS, vol. 5728, pp. 367–382. Springer, Heidelberg (2009)CrossRefGoogle Scholar
  6. 6.
    Braga, B.F.B., Almeida, J.P.A., Guizzardi, G., Benevides, A.B.: Transforming OntoUML into Alloy: towards conceptual model validation using a lightweight formal method. Innovations in Systems and Software Engineering 6(1-2), 55–63 (2010)CrossRefGoogle Scholar
  7. 7.
    Dwyer, M.B., Avrunin, G.S., Corbett, J.C.: Patterns in property specifications for finite-state verification. In: Proceedings of the 21st International Conference on Software Engineering, ICSE 1999, pp. 411–420. ACM (1999)Google Scholar
  8. 8.
    Garis, A., Cunha, A., Riesco, D.: Translating Alloy Specifications to UML Class Diagrams Annotated with OCL. In: Barthe, G., Pardo, A., Schneider, G. (eds.) SEFM 2011. LNCS, vol. 7041, pp. 221–236. Springer, Heidelberg (2011)CrossRefGoogle Scholar
  9. 9.
    Georg, G., Anastasakis, K., Bordbar, B., Houmb, S.H., Toahchoodee, I.R.M.: Verification and trade-off analysis of security properties in UML system models. IEEE Transactions on Software Engineering 36(3), 338–356 (2010)CrossRefGoogle Scholar
  10. 10.
    Jackson, D.: Software Abstractions: Logic, Language, and Analysis. MIT Press (2006)Google Scholar
  11. 11.
    Kosiuczenko, P.: Specification of Invariability in OCL. In: Wang, J., Whittle, J., Harel, D., Reggio, G. (eds.) MoDELS 2006. LNCS, vol. 4199, pp. 676–691. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  12. 12.
    Lanoix, A., Souquières, J.: Trustworthy Assembly of Components using B Refinement. e-Informatica Software Engineering Journal (ISEJ) 2(1) (2008)Google Scholar
  13. 13.
    Maoz, S., Ringert, J.O., Rumpe, B.: CD2Alloy: Class Diagrams Analysis Using Alloy Revisited. In: Whittle, J., Clark, T., Kühne, T. (eds.) MODELS 2011. LNCS, vol. 6981, pp. 592–607. Springer, Heidelberg (2011)CrossRefGoogle Scholar
  14. 14.
    Mostefaoui, F., Vachon, J.: Verification of Aspect-UML models using Alloy. In: Proceedings of the 10th International Workshop on Aspect-Oriented Modeling, pp. 41–48. ACM (2007)Google Scholar
  15. 15.
    Nimiya, A., Yokigawa, T., Miyazaki, H., Amasaki, S., Sato, Y., Hayase, M.: Model checking consistency of UML diagrams using Alloy. World Academy of Science, Engineering and Technology 71(99), 547–550 (2010)Google Scholar
  16. 16.
    OMG: UML Superstructure, Version 2.4.1 (2011)Google Scholar
  17. 17.
    OMG: Object Constraint Language, Version 2.3.1 (2012)Google Scholar
  18. 18.
    Paiva, A.C.R., Faria, J.C.P., Vidal, R.F.A.M.: Towards the integration of visual and formal models for GUI testing. Electronic Notes in Theoretical Computer Science 190(2), 99–111 (2007)CrossRefGoogle Scholar
  19. 19.
    Porres, I., Rauf, I.: Generating class contracts from UML protocol statemachines. In: Proceedings of the 6th International Workshop on Model-Driven Engineering, Verification and Validation, MoDeVVa 2009. pp. 8:1–8:10. ACM (2009)Google Scholar
  20. 20.
    Rasch, H., Wehrheim, H.: Checking Consistency in UML Diagrams: Classes and State Machines. In: Najm, E., Nestmann, U., Stevens, P. (eds.) FMOODS 2003. LNCS, vol. 2884, pp. 229–243. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  21. 21.
    Ries, B.: SESAME: A Model-Driven Process for the Test Selection of Small-Size Safety- Related Embebbed Software. Ph.D. thesis, Université du Luxembourg (2009)Google Scholar
  22. 22.
    Schinz, I., Toben, T., Mrugalla, C., Westphal, B.: The Rhapsody UML verification environment. In: Proceedings of the Software Engineering and Formal Methods, SEFM 2004. pp. 174–183 (2004)Google Scholar
  23. 23.
    Snook, C., Butler, M.: UML-B: Formal modeling and design aided by UML. ACM Trans. Softw. Eng. Methodol. 15, 92–122 (2006)CrossRefGoogle Scholar
  24. 24.
    Taghdiri, M., Jackson, D.: A Lightweight Formal Analysis of a Multicast Key Management Scheme. In: König, H., Heiner, M., Wolisz, A. (eds.) FORTE 2003. LNCS, vol. 2767, pp. 240–256. Springer, Heidelberg (2003)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2012

Authors and Affiliations

  • Ana Garis
    • 1
  • Ana C. R. Paiva
    • 2
  • Alcino Cunha
    • 3
  • Daniel Riesco
    • 1
  1. 1.Universidad Nacional de San LuisArgentina
  2. 2.DEI-FEUPUniversidade do PortoPortugal
  3. 3.HASLabINESC TEC and Universidade do MinhoPortugal

Personalised recommendations