Abstract
UML statecharts are used for describing dynamic aspects of system behavior. The work presented here extends a general Petri net-based methodology to support formal modeling of UML statecharts. The approach focuses on the specific task of generating explicit transition models associated with the hierarchical structure of statechart. We introduce a state-transition notation to serve as an intermediate model for conversion of UML statecharts, and in particular, the complexity of composite states, to other target specifications. By defining a process for deriving, from UML statecharts, a state-transition notation that can serve as an intermediate state machine model, we seek to deepen understanding of modeling practices and help bridge the gap between model development and model analysis. This work covers all of the primary issues associated with the hierarchical structure of composite states, including entry and exit transitions, transition priorities, history states, and event dispatching. Thus, the results provide an important step forward toward the goal of modeling increasingly complex semantics of UML statecharts.
Article PDF
Similar content being viewed by others
Explore related subjects
Discover the latest articles, news and stories from top researchers in related subjects.Avoid common mistakes on your manuscript.
References
von der Beek, M.: Formalization of UML-statecharts. In: Gogolla, M., Kobryn, C. (ed.), Proc. of UML’2001—The Unified Modeling Language, vol. 2185, in LNCS, Springer Verlag, (2001)
Bondavalli, A., Dal Cin, M., Latella, D., Majzik, I., Fataricza, A., Savoia, G.: Dependability analysis in the early phases of UML-based system design. J Comp. Syst. Sci. Eng. 16(5), 265–275 (2001)
Binder, R.V.: Testing Object-Oriented Systems: Models, Patterns, and Tools. Addison Wesley (2000)
Booch, G., Jacobson, I., Rumbaugh, J.: The Unified Modeling Language User Guide. Addison-Wesley (1999)
Bruel, J.M., Lilius, J., Moreira, A., France, R.B.: Defining precise semantics for UML. In: Malefant, J., Moisan, S., Moreira, A. (eds.) ECOOP 2000 Workshop Reader, vol. 1964 in LNCS. Springer Verlag (2000).
Baresi, L., Pezzè, M.: On formalizing UML with high-level Petri nets. In: Agha, G., Cindio, F. De (eds.) Concurrent Object-Oriented Programming and Petri Nets (a special volume in Petri Nets series), vol. 2001 of LNC, pp. 271–300, Springer Verlag (2001)
Compton, K., Huggins, J., Shen, W.: A semantic model for the state machine in the unified modeling language. In: Kent S., Evans A., Selic B. (eds.) Proc. of UML’2000 Workshop—Dynamic Behaviour in UML Models: Semantic Questions, vol. 1939 in LNCS. Springer Verlag (2000)
Design/CPN. Available at www.daimi.au.dk/designCPN/
Dong, Z., Fu, Y., He, X.: Deriving hierarchical predicate/transition nets from statechart diagrams. In: Proc. of Software Engineering and Knowledge Engineering (2003)
Dwyer, M.B., Avrunin, G.S., Corbett, J.C.: Patterns in property specifications for finite-state verification. In: Proc. of Int’l Conf. on Software Engineering (ICSE99). IEEE (1999)
Dwyer, M.B., Avrunin, G.S., Corbett, J.C.: A System of Specification Patterns. Available at patterns.projects.cis.ksu.edu/
France, R., Evans, A., Lano, Rumpe, B.: The UML as a formal modeling notation. In: Proc. of UML’98 Workshop—Beyond the notation, vol. 1618 of LNCS, pp. 336–348, Springer (1999)
Gábor, H., István, M.: Quantitative analysis of dependability critical systems based on UML statechart models. In: Proc. of Fifth IEEE International Symposium on High Assurance Systems Engineering, pp. 83–92 (2000)
Gery, E., Harel, D., Palatshy, E. Rhapsody: A complete lifecycle model-based development system. In: Proc. of Int’l Conf. on Intergrated Formal Methods (2002)
Gogolla, M., Parisi-Presicce, F.: State diagrams in UML: A formal semantics using graph transformations. In: Broy, M., Coleman, D., Maibaum, T.S.E., Rumpe, B. (eds.) Proc. of PSMT’98 Workshop on Precise Semantics for Modeling Techniques. Technische Universität München, TUM-I9803, pp. 55–72 (1998)
Gnesi, S., Latella, D., Majzik, I., Massink, M.: Formal validation of UML statechart diagrams models. In: Kent S., Evans A., Selic B. (eds.) Proc. of UML’2000 Workshop—Dynamic Behaviour in UML Models: Semantic Questions, vol. 1939 in LNCS, Springer Verlag (2000)
Harel, D.: Statecharts: A visual formalism for complex systems. Sci. Comp. Progr. 8, 231–274 (1987)
Hu, Z., Shatz, S.: Mapping UML diagrams to a Petri net notation to exploit tool support for system simulation. In: Proc. Int’l Conf. on Software Engineering and Knowledge Engineering (SEKE’04), pp. 213–219 (2004)
Kristensen, L.M., Christensen, S., Jensen, K.: The practitioner’s guide to coloured Petri nets. Int. J. Softw. Tool Technol. Trans.; pp. 98–132, Springer Verlag (1998)
King, P., Pooley, R.: Using UML to derive stochastic Petri net to the models. In: Proc. of the 15th Annu. UK Performance Engineering Workshop, pp. 45–56 (1999)
Kuske, S.: A formal semantics of UML state machines based on structured graph transformation. In: Gogolla M., Kobryn C. (eds.) Proc. of UML’2001—The Unified Modeling Language, vol. 2185 in LNCS. Springer Verlag (2001)
Lano, K., Bicarregui, J., Evans, A.: Structured axiomatic semantics for UML models. In: Proc. of ROOM 2000, Electronic Workshops in Computer Science. Springer Verlag (2000)
Latella, D., Majzik, I., Massink, M.: Towards a formal operational semantics of UML statechart diagrams. In: Proc. of FMOODS’99, IFIP TC6/WG6.1, Third IFIP International Conference On Formal Methods for Open Object-based Distributed System, pp. 331–347 (1999)
Lilius, J., Paltor, I.: The semantics of UML state machines. Technical Report 273, Turku Centre for Computer Science (1999)
McUmber, W.E., Cheng, B.H.: UML-based analysis of embedded systems using a mapping to VHDL. In: Proc. of IEEE high Assurance Software Engineering (HASE99). IEEE (1999)
Merseguer, J.: Software Performance Modeling Based on UML and Petri nets. Doctoral Thesis, Universidad de Zaragoza (2003)
ITU-T Recommendation Z.120: Message Sequence Chart. International Telecommunication Union; Telecommunication Standardization Section (ITU-T) (1999)
Murata, T.: Petri nets: Properties analysis and applications. Proc. of the IEEE, 77(4), 541–580 (1989)
OMG, UML semantics 1.5, 2003, available at www.uml.org
Pettit IV, R.G., Gomaa, H.: Validation of dynamic behavior in UML using colored petri nets. In: Kent S., Evans A., Selic B. (eds.) Proc. of UML’2000 Workshop—Dynamic Behaviour in UML Models: Semantic Questions, vol. 1939 in LNCS. Springer Verlag (2000)
Paltor, I., Lilius, J.: Formalizing UML state machines for model checking. In: France R., Rumpe B. (eds.) UML’99—The Unified Modeling Language. Beyond the Standard, vol. 1723 in LNCS. Springer (1999)
Poole, J.D.: Model-driven architecture: Vision, standards and emerging technologies. In: Proc. of ECOOP’2001Workshop on Object-Oriented Architectural Evolution (2001)
The Precise UML Group. Available at www.cs.york.ac.uk/puml/
Reggio, G.: Metamodelling behavioral aspects: the case of the UML state machines complete version. Technical Report of DISI—Università di Genova, DISI-TR-02-3, Italy (2002)
Rumpe, B.: A note on semantics (with an emphasis on UML). In: Kilov H., Rumpe B. (eds.) Proc. of Second ECOOP Workshop on Precise Behavioral Semantics, Technische Universität München, TUM-I9813 (1998)
Saldhana, J.A., Shatz, S.M., Hu, Z.: Formalization of object behavior and interactions from UML models. Int. J. Softw. Eng. Knowl. Engi. 11(6), 643–673 (2001)
Author information
Authors and Affiliations
Corresponding author
Additional information
This material is based upon work supported by the U.S. Army Research Office under grant number DAAD19-01-1-1-0672, and the U.S. National Science Foundation under grant number CCR-9988168.
Rights and permissions
About this article
Cite this article
Hu, Z., Shatz, S.M. Explicit modeling of semantics associated with composite states in UML statecharts. Autom Software Eng 13, 423–467 (2006). https://doi.org/10.1007/s10515-006-0272-6
Issue Date:
DOI: https://doi.org/10.1007/s10515-006-0272-6