Model Checking Dynamic UML Consistency

  • Xiangpeng Zhao
  • Quan Long
  • Zongyan Qiu
Part of the Lecture Notes in Computer Science book series (LNCS, volume 4260)


UML is widely accepted and extensively used in software modeling. However, using different diagrams to model different aspects of a system brings the risk of inconsistency among diagrams. In this paper, we investigate an approach to check the consistency between the sequence diagrams and statechart diagrams using the SPIN model checker. To deal with the hierarchy structure of statechart diagrams, we propose a formalism called Split Automata, a variant of automata, which is helpful to bridge the statechart diagrams to SPIN efficiently. Compared with the existing work on model checking UML which do not have formal verification for their translation from UML to the model checker, we formally define the semantics and prove that the automatically translated model (i.e. Split Automata) does simulate the UML model. In this way, we can guarantee that the translated model does represent the original model.


UML Consistency Semantics Simulation Model Checking Algorithm 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Astesiano, E., Reggio, G.: An attempt at analysing the consistency problems in the UML from a classical algebraic viewpoint. In: Wirsing, M., Pattinson, D., Hennicker, R. (eds.) WADT 2003. LNCS, vol. 2755, pp. 56–81. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  2. 2.
    Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L.: Sequential circuit verification using symbolic model checking. In: DAC 1990: Proceedings of the 27th ACM/IEEE conference on Design automation, pp. 46–51. ACM Press, New York (1990)CrossRefGoogle Scholar
  3. 3.
    Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. The MIT Press, Cambridge (2000)Google Scholar
  4. 4.
    Fowler, M.: What is the point of UML. In: Bézivin, J., Muller, P.-A. (eds.) UML 1998. LNCS, vol. 1618. Springer, Heidelberg (1999)Google Scholar
  5. 5.
    Kuester, J.M., Engels, G., Groenewegen, L.: Consistent interaction of software components. In: Proc. of IDPT 2002 (2002)Google Scholar
  6. 6.
    Gallardo, M.M., Merino, P., Pimentel, E.: Debugging UML designs with model checking. Journal of Object Technology 1(2), 101–117 (2002)CrossRefGoogle Scholar
  7. 7.
    He, J., Li, X., Liu, Z.: RCOS: A refinement calculus for object-oriented systems. Theoretical Computer Science (accepted for publication) Also available as Technical Report 322. UNU/IIST, P.O.Box 3058, Macao SAR China,
  8. 8.
    Holzmann, G.J.: The SPIN Model Checker: Primer and Reference Manual. Addison-Wesley, Reading (2003)Google Scholar
  9. 9.
    Inverardi, P., Muccini, H., Pelliccione, P.: Checking consistency between architectural models using SPIN. In: Proc. of STRAW 2001 (2001)Google Scholar
  10. 10.
    Jacobson, I., Rumbaugh, J., Booch, G.: The Unified Modelling Language Reference Manual. Addison-Wesley, Reading (1999)Google Scholar
  11. 11.
    Knapp, A., Merz, S., Rauh, C.: Model checking timed UML state machines and collaborations. In: Damm, W., Olderog, E.-R. (eds.) FTRTFT 2002. LNCS, vol. 2469, pp. 395–416. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  12. 12.
    Küster, J.M., Stehr, J.: Towards explicit behavioral consistency concepts in the UML. In: Proc. of the 2nd International Workshop on Scenarios and State Machines: Models, Algorithms, and Tools, Portland, USA (2003)Google Scholar
  13. 13.
    Lilius, J., Paltor, I.P.: Formalising UML state machines for model checking. In: France, R.B., Rumpe, B. (eds.) UML 1999. LNCS, vol. 1723, pp. 430–444. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  14. 14.
    Long, Q., Liu, Z., Li, X., He, J.: Consistent code generation from UML models. In: Proc. of Australian Software Engineering Conference (ASWEC 2005), Brisbane, Australia. IEEE Computer Society, Los Alamitos (2005)Google Scholar
  15. 15.
    Long, Q., Qiu, Z., Qin, S.: The equivalence of statecharts. In: Dong, J.S., Woodcock, J. (eds.) ICFEM 2003. LNCS, vol. 2885, pp. 125–143. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  16. 16.
    Schäfer, T., Knapp, A., Merz, S.: Model checking UML state machines and collaborations. Electronic Notes in Theoretical Computer Science 55(3) (2001)Google Scholar
  17. 17.
    Visser, W., Havelund, K., Brat, G., Park, S.J.: Model checking programs. In: ASE 2000, Washington, DC, USA. IEEE Computer Society, Los Alamitos (2000)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2006

Authors and Affiliations

  • Xiangpeng Zhao
    • 1
  • Quan Long
    • 1
    • 2
  • Zongyan Qiu
    • 1
  1. 1.LMAM and Department of Informatics, School of Math.Peking UniversityBeijingChina
  2. 2.IBM China Research Laboratory 

Personalised recommendations