Paper:
Generating Maude Specifications from M-UML Statechart Diagrams
Mourad Kezai and Abdallah Khababa
Department of Computer Science, University of Sétif 1
El Bez Campus, Sétif 19000, Algeria
Corresponding author
The unified modeling language (UML) is used for the specification, visualization, and documentation of object-oriented software systems. Mobile UML (M-UML) is an extension of UML that considers mobility aspects, and a mobile statechart is an extension of the standard UML diagram that deals with the requirements for modeling, specifying, and visualizing mobile agent-based systems. However, mobile statecharts inherit UML’s lack of formal notation for analysis and verification purposes. The rewriting logic language Maude is a formal method that deals with mobile computations. In this paper, we propose a formalization of M-UML statechart diagrams using Maude to provide formal semantics for such diagrams. The generated Maude specifications are then used to analyze and check the systems using Maude analytical tools. This approach is illustrated through an example.
- [1] A. Fuggetta, G. P. Picco, and G. Vigna, “Understanding code mobility,” IEEE Trans. on Software Engineering, Vol.24, No.5, pp. 342-361, 1998.
- [2] D. B. Lange and M. Oshima, “Seven good reasons for mobile agents,” Communications of the ACM, Vol.42, No.3, pp. 88-89, 1999.
- [3] OMG: OMG Unified Modeling Language, Superstructure, v2.3, 2010, https://www.omg.org/spec/UML/2.3/Superstructure/PDF [accessed May 3, 2010]
- [4] K. Saleh and C. El-Morr, “M-UML: an extension to UML for the modeling of mobile agent-based software systems,” J. of Information and Software Technology, Vol.46, No.4, pp. 219-227, 2004.
- [5] J. Warmer and A. Kleppe, “The Object Constraint Language: Getting your Models Ready for MDA,” 2nd Edition, Addison-Wesley Professional, 2003.
- [6] A. Evans, R. France, K. Lano, and B. Rumpe, “The UML as a formal modeling notation,” J. Bézivin and P.-A. Muller (Eds.), “The Unified Modeling Language 〈〈UML〉〉 ’98: Beyond the Notation,” Lecture Notes in Computer Science, Vol.1618, pp. 336-348, Springer, 1999.
- [7] J. A. Saldhana, S. M. Shatz, and Z. Hu, “Formalisation of object behavior and interaction from UML models,” Int. J. of Software Engineering and Knowledge Engineering, Vol.11, No.6, pp. 643-673, 2001.
- [8] X. Hei, L. Chang, W. Ma, J. Gao, and G. Xie, “Automatic transformation from UML statechart to Petri nets for safety analysis and verification,” Int. Conf. on Quality, Reliability, Risk, Maintenance, and Safety Engineering (ICQR2MSE), pp. 948-951, 2011.
- [9] M. Wang and L. Lu, “A transformation method from UML statechart to Petri nets,” IEEE Int. Conf. on Computer Science and Automation Engineering (CSAE), Vol.2, pp. 89-92, 2012.
- [10] E. Kerkouche, A. A. Chaoui, E. B. Bourennane, and O. Labbani, “A UML and colored Petri nets integrated modeling and analysis approach using graph transformation,” J. of Object Technology, Vol.9, No.4, pp. 25-43, 2010.
- [11] J. Araujo and A. Moreira, “Specifying the Behavior of UML Collaborations Using Object-Z,” Americas Conf. on Information Systems (AMCIS) 2000 Proc., 364, 2000.
- [12] H. Ledang and J. Souquières, “Formalizing UML Behavioral Diagrams with B,” 10th OOPSLA Workshop on Behavioral Semantics: Back to Basics, 2001.
- [13] C. A. R. Hoare, “Communicating Sequential Processes,” Prentice Hall Int. Series in Computer Science, Prentice Hall, 1985.
- [14] P. Gagnon, F. Mokhati, and M. Badri, “Applying model checking to concurrent UML models,” J. of Object Technology, Vol.7, No.1, pp. 59-84, 2008, http://www.jot.fm/issues/issue_2008_01/article1.pdf [accessed February 1, 2008]
- [15] M. L. Crane and J. Dingel, “On the semantics of UML state machines: Categorization and comparison,” Technical Report 2005-501, School of Computing, Queen’s University, 2005.
- [16] C. Rossi, M. Enciso, and I. P. de Guzmán, “Formalization of UML state machines using temporal logic,” Software & Systems Modeling, Vol.3, No.1, pp. 31-54, 2004.
- [17] M. Y. Ng and M. Butler, “Towards formalizing UML state diagrams in CSP,” 1st Int. Conf. on Software Engineering and Formal Methods (SEFM 2003), pp. 138-147, 2003.
- [18] W. L. Yeung, K. R. P. H. Leung, J. Wang, and W. Dong, “Improvements towards formalizing UML state diagrams in CSP,” 12th Asia-Pacific Software Engineering Conf. (APSEC 2005), 2005.
- [19] J. Lilius and I. P. Paltor, “The Semantics of UML State Machines,” TUCS Technical Report, No.273, Turku Centre for Computer Science, 1999.
- [20] S. A. Seshia, R. K. Shyamasundar, A. K. Bhattacharjee, and S. D. Dhodapkar, “A translation of statecharts to Esterel,” J. M. Wing, J. Woodcock, and J. Davies (Eds.), “World Congress on Formal Methods in the Development of Computing Systems,” Lecture Notes in Computer Science, Vol.1709, pp. 983-1007, Springer, 1999.
- [21] V. S. W. Lam and J. Padget, “Formalization of UML statechart diagrams in the π-calculus,” Proc. of Australian Software Engineering Conf., pp. 213-223, 2001.
- [22] A. Knapp, S. Merz, and M. Wirsing, “Refining mobile UML state machines,” C. Rattray, S. Maharaj, and C. Shankland (Eds.), “Algebraic Methodology and Software Technology,” Lecture Notes in Computer Science, Vol.3116, pp. 274-288, Springer, 2004.
- [23] M. R. Bahri, A. Hettab, A. Chaoui, and E. Kerkouche, “Transforming mobile UML statecharts models to nested nets models using graph grammars: An approach for modeling and analysis of mobile agent-based software systems,” 4th South-East European Workshop on Formal Methods (SEEFM 2009), pp. 33-39, 2009.
- [24] A. Belghiat, A. Chaoui, M. Maouche, and M. Beldjehem, “Formalization of mobile UML statechart diagrams using the π-calculus: An approach for modeling and analysis,” G. Dregvaite and R. Damasevicius (Eds.), “Information and Software Technologies,” Communications in Computer and Information Science, Vol.465, pp. 236-247, Springer, 2014.
- [25] J. Meseguer, “A logical theory of concurrent objects and its realization in the Maude language,” G. Agha, P. Wegner, and A. Yonezawa (Eds.), “Research Directions in Object-Oriented Programming,” pp. 314-390, MIT Press, 1992.
- [26] J. Meseguer, “Software Specification and Verification in Rewriting Logic,” Computer Science Department, University of Illinois at Urbana-Champaign, 2003.
- [27] M. Clavel, F. Durán, S. Eker, P. Lincoln, N. Martí-Oliet, J. Meseguer, and C. Talcott, “Maude Manual (version 2.2),” SRI International, 2007.
- [28] S. Eker, J. Meseguer, and A. Sridharanarayanan, “The Maude LTL model checker,” Proc. of the 4th Int. Workshop on Rewriting Logic and its Applications (WRLA), Electronic Notes in Theoretical Computer Science, Vol.71, pp. 162-187, 2004.
- [29] F. Mokhati and M. Badri, “Generating Maude specifications from UML use case diagrams,” J. of Object Technology, Vol.8, No.2, pp. 119-136, 2009.
- [30] E. Kerkouche, K. Khalfaoui, A. Chaouio, and A. Aldahoud, “UML activity diagrams and Maude integrated modeling and analysis approach using graph transformation,” The 7th Int. Conf. on Information Technology (ICIT 2015), pp. 515-521, 2015.
This article is published under a Creative Commons Attribution-NoDerivatives 4.0 Internationa License.