On Formalizing Predefined OCL Properties

Authors: Meryem Lamrani, Younès El Amrani, Aziz Ettouhami

Abstract:

The ability of UML to handle the modeling process of complex industrial software applications has increased its popularity to the extent of becoming the de-facto language in serving the design purpose. Although, its rich graphical notation naturally oriented towards the object-oriented concept, facilitates the understandability, it hardly successes to report all domainspecific aspects in a satisfactory way. OCL, as the standard language for expressing additional constraints on UML models, has great potential to help improve expressiveness. Unfortunately, it suffers from a weak formalism due to its poor semantic resulting in many obstacles towards the build of tools support and thus its application in the industry field. For this reason, many researches were established to formalize OCL expressions using a more rigorous approach. Our contribution join this work in a complementary way since it focuses specifically on OCL predefined properties which constitute an important part in the construction of OCL expressions. Using formal methods, we mainly succeed in expressing rigorously OCL predefined functions.

Keywords: Formal methods, Z, OCL, predefined properties, metamodel types.

Digital Object Identifier (DOI): doi.org/10.5281/zenodo.1328894

References:

[1] The Object Management Group, Object Constraint Language 2.2, http://www.omg.org/spec/OCL/2.2/
[2] The Object Management Group, UML 2.3 superstructure specification, http://www.omg.org/spec/uml/2.3/
[3] J.M. Spivey, "The Z Notation: A Reference Manual," in Prentice Hall international series in computer science xi, 158, 1989.
[4] J. Woodcock, and J. Davies, "Using Z: specification, refinement, and proof," in Prentice Hall international series in computer science xi, 39, 1996.
[5] L. Henocque, "Z specification of Object Oriented Constraint Programs," in Revista Real Academia de Ciencias SerieA. Math. (RACSAM). 98 (1): pp. 127-152, 2004.
[6] M. Lamrani, Y. El Amrani, and A. Ettouhami, "Formal Specification of Software Design Metrics," The Sixth International Conference on Software Engineering Advances, pp. 348-355. Barcelona, 2011.
[7] M. Richters, and M. Gogolla, "On Formalizing the UML Object Constraint Language OCL," in Wirtschaftsinformatik 50, 449-464, 1998.
[8] 8. Flake, and W. Mueller, "Formal Semantics of OCL Messages," in Electronic Notes in Theoretical Computer Science 102, 77-97, 2003.
[9] S. Flake, "Towards the Completion of the Formal Semantics of OCL 2. 0," in Reproduction 73-82, 2003.
[10] G. Mezei, T. Levendovszky, and H. Charaf, "Formalizing the Evaluation of OCL Constraints," in Acta Polytechnica Hungarica. 4, 89-110, 2007.
[11] M. Kyas, et al., "Formalizing UML Models and OCL Constraints in PVS1," in Electronic Notes in Theoretical Computer Science 115, 39-47, 2005.
[12] R. Marcano, and N. Levy, "Transformation rules of OCL constraints into B formal expressions," (CSDUML2002) Workshop on critical systems development with UML 5th International Conference on the Unified Modeling Language, 2002.
[13] J. Woodcock, P.G. Larsen, J. Bicarregui, and J. Fitzgerald, "Formal methods," in ACM Computing Surveys 41, 1-36, 2009.
[14] M. Saaltink, " Z and EVES," Z User Workshop York 1991 223-242, 1992.