Aspect-Oriented Formal Modeling: (AspectZ + Object-Z) = OOAspectZ


  • Cristian Vidal Silva Departamento de Computación e Informática, Facultad de Ingeniería, Universidad de Playa Ancha, Valparaíso
  • Rodolfo Villarroel Escuela de Ingeniería Informática, Facultad de Ingeniería, Pontificia Universidad Católica de Valparaíso
  • Rodolfo Schmal Simón Ingeniería Informática Empresarial, Facultad de Economía y Negocios, Universidad de Talca
  • Rodrigo Saens Ingeniería Comercial, Facultad de Economía y Negocios, Universidad de Talca
  • Tamara Tigero Ingeniería Comercial, Facultad de Economía y Negocios, Universidad de Talca
  • Carolina Del Rio Ingeniería Comercial, Facultad de Economía y Negocios, Universidad de Talca


AspectZ, Object-Z, Z, aspects, crosscutting concerns


The aspect-oriented software development (AOSD) paradigm permits modularizing crosscutting concerns of base modules, a non-usual task in other software development paradigms. Since AOSD was born in the programming stage as an extension of an object-oriented (OO) programming language, and AOSD considers, in addition to base modules, new modules named aspects, then a complete AOSD process requires that each stage considers the base and aspect modules. Therefore, looking for an AOSD process, mainly to apply AOSD in other phases of the OO software development process, so far, different OO modeling tools and language extensions to support AOSD have been proposed. As an example, AspectZ is an extension of the formal language Z to support AOSD. To reach a transparency of concepts and design in AOSD, the main contribution of this article is to propose OOAspectZ, a formal language for the requirements specification stage of aspect-oriented (AO) software applications, that, firstly, extends AspectZ and, secondly, integrates Object-Z and AspectZ formal specifications. Thus, OOAspectZ supports relevant AO elements such as join points, and This and Target objects for join point events. As an application example, this article applies OOAspectZ to a system named GradUTalca for a Chilean university. For GradUTalca, this article presents AO UML use cases and UML class diagrams, formal Object-Z and OOAspectZ specifications, and a final woven specification to show an integration of Object-Z and OOAspectZ specifications.


Download data is not yet available.




How to Cite

Vidal Silva, C., Villarroel, R., Schmal Simón, R., Saens, R., Tigero, T., & Del Rio, C. (2016). Aspect-Oriented Formal Modeling: (AspectZ + Object-Z) = OOAspectZ. COMPUTING AND INFORMATICS, 34(5), 996–1016. Retrieved from

Most read articles by the same author(s)