Abstract
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.
Supported by NNSF of China (No. 605730081).
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
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)
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)
Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. The MIT Press, Cambridge (2000)
Fowler, M.: What is the point of UML. In: Bézivin, J., Muller, P.-A. (eds.) UML 1998. LNCS, vol. 1618. Springer, Heidelberg (1999)
Kuester, J.M., Engels, G., Groenewegen, L.: Consistent interaction of software components. In: Proc. of IDPT 2002 (2002)
Gallardo, M.M., Merino, P., Pimentel, E.: Debugging UML designs with model checking. Journal of Object Technology 1(2), 101–117 (2002)
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, http://www.iist.unu.edu
Holzmann, G.J.: The SPIN Model Checker: Primer and Reference Manual. Addison-Wesley, Reading (2003)
Inverardi, P., Muccini, H., Pelliccione, P.: Checking consistency between architectural models using SPIN. In: Proc. of STRAW 2001 (2001)
Jacobson, I., Rumbaugh, J., Booch, G.: The Unified Modelling Language Reference Manual. Addison-Wesley, Reading (1999)
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)
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)
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)
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)
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)
Schäfer, T., Knapp, A., Merz, S.: Model checking UML state machines and collaborations. Electronic Notes in Theoretical Computer Science 55(3) (2001)
Visser, W., Havelund, K., Brat, G., Park, S.J.: Model checking programs. In: ASE 2000, Washington, DC, USA. IEEE Computer Society, Los Alamitos (2000)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Zhao, X., Long, Q., Qiu, Z. (2006). Model Checking Dynamic UML Consistency. In: Liu, Z., He, J. (eds) Formal Methods and Software Engineering. ICFEM 2006. Lecture Notes in Computer Science, vol 4260. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11901433_24
Download citation
DOI: https://doi.org/10.1007/11901433_24
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-47460-9
Online ISBN: 978-3-540-47462-3
eBook Packages: Computer ScienceComputer Science (R0)