Aspect-oriented formal modeling: (Aspectz + Object-Z) = Ooaspectz

Cristian Vidal Silva, Rodolfo Villarroel, Rodolfo Schmal Simón, Rodrigo Saens, Tamara Tigero, Carolina Del Rio

Research output: Contribution to journalArticlepeer-review

8 Scopus citations


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 (00) 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 00 software development process, so far, different 00 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.

Original languageEnglish
Pages (from-to)996-1016
Number of pages21
JournalComputing and Informatics
Issue number5
StatePublished - 2015


  • AspectZ
  • Aspects
  • Crosscutting concerns
  • Object-Z
  • Z


Dive into the research topics of 'Aspect-oriented formal modeling: (Aspectz + Object-Z) = Ooaspectz'. Together they form a unique fingerprint.

Cite this