A proposal for the formalization of the class diagram in Maude Language
Keywords:
Class diagram, formal specification, Maude language, software engineeringAbstract
The class diagram is a tool for developing object-oriented software. It is essential that its interpretation by any analyst lacks ambiguity. In this paper, we present an interpretation of the class diagram from the perspective of an equational logic through a systematic breakdown of each of its elements. Our aim is to provide a formal specification for the class diagram susceptible of being processed and executed. For our formalization, we used the Maude language, because it allows us to define formal algebraic specifications for abstract data types.
Article Metrics
Abstract: 372 HTML (Español (España)): 134 PDF (Español (España)): 477 XML (Español (España)): 29References
G. Booch, R. Maksimchuk, M. Engle, J. Conallen, K. Houston, and J. Bobbi, Object oriented design with applications. Redwood City, USA, 1991.
J. Rumbaugh, M. Blaha, W. Premerlani, and F. Eddy, Object-oriented modeling and design. Prentice-hall, 1991.
I. Jacobson, “Object Oriented Software Engineering: A Use Case Driven Approach,” 1992.
B. Meyer, Object-oriented software construction, Vol 2. New York, USA: Prentice hall, 1988.
G. Booch, I. Jacobson, and J. Rumbaugh, “OMG Unified Modeling Lenguage Specification,” 2000. [Online]. Available: http://www.omg.org/spec/UML/. [Accessed: 20-Apr-2016].
F. Arango Isaza, Aplicaciones de la Lógica al Desarrollo de Software: Lenguajes Lógicos y Funcionales (sec 4.3), 2nd ed. Medellín, Colombia: Universidad Nacional de Colombia, 2016.
B. Rumpe, “A Note on Semantics (with an Emphasis on UML),” Second ECOOP Work. Precise Behav. Semant., 1998.
J. Warmer and A. Kleppe, “The Object Constraint Language: Precise Modeling With Uml (Addison-Wesley Object Technology Series),” 1998.
J. Fitzgerald, P. Larsen, P. Mukherjee, and N. Plat, Validated designs for object-oriented systems. 2005.
C. B. Jones, Systematic software development using VDM. Prentice Hall, 1990.
A. Evans, R. France, K. Lano, and B. Rumpe, “Developing the UML as a formal modelling notation,” UML’98 Beyond notation. Int. Work. Mulhouse Fr., 1998.
A. Evans, “Reasoning with UML class diagrams,” , 1998. Proceedings. 2nd IEEE Work., 1998.
A. Evans and S. Kent, “Core meta-modelling semantics of UML: the pUML approach,” Int. Conf. Unified Model., 1999.
A. Hall, “Specifying and interpreting class hierarchies in Z,” Z User Work. Cambridge 1994, 1994.
M. Cengarle, H. Grönninger, and B. Rumpe, “System model semantics of class diagrams,” arXiv Prepr., 2008.
N. Zafar and F. Alhumaidan, “Transformation of class diagrams into formal specification,” Int. J. Comput. Sci., 2011.
J. Woodcock and J. Davies, Using Z: specification, refinement, and proof. Prentice hall, 1996.
D. Berardi, D. Calvanese, and G. De Giacomo, “Reasoning on UML class diagrams,” Artif. Intell., 2005.
L. Efrizoni and W. Wan-Kadir, “Formalization of UML class diagram using description logics,” 2010 Int. Symp. Inf. Technol., vol. 3, 2010.
F. Baader, The description logic handbook: Theory, implementation and applications. 2003.
H. Ledang, “Automatic translation from UML specifications to B,” Autom. Softw. Eng. 2001.(ASE 2001), 2001.
H. Ledang, “Formal techniques in the objectoriented software development: an approach based on the B method,” 11th PhDOOS ECOOP2001 Dr. Work., 2001.
C. Snook and M. Butler, “UML-B: Formal modeling and design aided by UML,” ACM Trans. Softw. Eng., 2006.
A. T. Álvarez and J. L. Alemán, “Formally modeling UML and its evolution: a holistic approach,” Form. Methods Open Object-Based Distrib. Syst. IV, vol. 49, 2000.
N. Bourbaki, “Theory of sets,” Springer Berlin Heidelb., pp. 65–129, 2004.
A. Hall, “Using Z as a specification calculus for object-oriented systems,” Int. Symp. VDM Eur., 1990.
R. H. Bourdeau and B. H. C. Cheng, “A formal semantics for object model diagrams,” IEEE Trans. Softw. Eng., vol. 21, no. 10, pp. 799–821, 1995.
J. Guttag, J. Horning, S. J. Garland, K. D. Jones, A. Modet, and J. M. Wing, Larch: languages and tools for formal specification. 1993.
M. Clavel, F. Durán, S. Eker, P. Lincoln, N. Martı́-Oliet, J. Meseguer, and J. F. Quesada, “Maude: specification and programming in rewriting logic,” Theor. Comput. Sci., vol. 285, no. 2, pp. 187–243, 2002.
J. Guttag, “Abstract Data Types and the Development of Data Structures,” in Software Pioneers, Berlin, Heidelberg: Springer Berlin Heidelberg, 2002, pp. 453–479.
S. Clérici, R. Jiménez, and F. Orejas, “Classsort polymorphism in GLIDER,” in Recent Trends in Data Type Specification, Springer Berlin Heidelberg, 1996, pp. 143–160.
F. Baader and T. Nipkow, Term rewriting and all that. Cambridge University Press, 1999.
D. A. Plaisted, “Equational reasoning and term rewriting systems,” in Handbook of logic in artificial intelligence and logic programming (vol. 1), New York, NY, USA: Oxford University Press, 1998, pp. 274–364.
M. Clavel, F. Durán, S. Eker, P. Lincoln, N. Martí-Oliet, J. Meseguer, and C. Talcott, All About Maude - A High-Performance Logical Framework: How to Specify, Program, and Verify Systems in Rewriting Logic, vol. 4350. Berlin, Heidelberg: Springer Berlin Heidelberg, 2007.
M. Clavel, F. Durán, S. Eker, P. Lincoln, N. Martí-oliet, J. Meseguer, and C. Talcott, “Maude Manual (Version 2.5),” 2010.
_
