Top > JACIII > Generating Maude Specifications from M-UML Statechart Diagrams

single-jc.php

JACIII Vol.26 No.1 pp. 8-16
doi: 10.20965/jaciii.2022.p0008
(2022)

Paper:

Views over last 60 days: 577

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

Received:
November 17, 2018
Accepted:
August 27, 2021
Published:
January 20, 2022
Creative Commons License
Keywords:
M-UML, mobile statechart, multi-agent system, Maude system, rewriting logic
Abstract

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.

Cite this article as:
M. Kezai and A. Khababa, “Generating Maude Specifications from M-UML Statechart Diagrams,” J. Adv. Comput. Intell. Intell. Inform., Vol.26 No.1, pp. 8-16, 2022.
Data files:
References
  1. [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. [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. [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. [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. [5] J. Warmer and A. Kleppe, “The Object Constraint Language: Getting your Models Ready for MDA,” 2nd Edition, Addison-Wesley Professional, 2003.
  6. [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. [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. [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. [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. [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. [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. [12] H. Ledang and J. Souquières, “Formalizing UML Behavioral Diagrams with B,” 10th OOPSLA Workshop on Behavioral Semantics: Back to Basics, 2001.
  13. [13] C. A. R. Hoare, “Communicating Sequential Processes,” Prentice Hall Int. Series in Computer Science, Prentice Hall, 1985.
  14. [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. [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. [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. [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. [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. [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. [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. [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. [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. [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. [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. [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. [26] J. Meseguer, “Software Specification and Verification in Rewriting Logic,” Computer Science Department, University of Illinois at Urbana-Champaign, 2003.
  27. [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. [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. [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. [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.

Creative Commons License  This article is published under a Creative Commons Attribution-NoDerivatives 4.0 Internationa License.

*This site is desgined based on HTML5 and CSS3 for modern browsers, e.g. Chrome, Firefox, Safari, Edge, Opera.

Last updated on Apr. 18, 2024