To facilitate handling crosscutting concerns at earlier software development phases, In our previous work [1], we proposed an aspect-oriented model-driven approach based on UML activity diagrams. The approach shifts aspect-oriented techniques from a code-centric to a model-centric, which is employed to handle the crosscutting concerns during design phases. Thus, it alleviates software complexity in a more abstract level. The primary functional concerns are modeled with activity diagrams, and crosscutting concerns are modeled with aspectual activity diagrams, respectively. Then the overall system design model, which is also an activity diagram, is integrated by weaving aspect models into primary model`s.

    Aspect-oriented modeling (AOM) alleviates software complexity in a more abstract level. However, aspect-oriented modeling techniques cannot guarantee the correctness of produced design models. wrong weaving sequences may cause the integrated models violate system crosscutting requirements. Design models are widely used as a basis of subsequent implementation and testing processes. As a result, it is costly if defects in design models are discovered at later implementation and testing stages. Therefore, assuring the correctness of the aspect-oriented design models is vitally important. So far, the applicable approach is manual review. It is time consuming and dependent on reviewers’ expertise. However, existing automatic verification tools cannot deal with aspect-oriented activity diagrams directly.

   We implemented a tool named Jasmine-AOV based on Topcased [2]and LoLA [3]. As Figure 5 shows, this tool is composed of 4 main parts: Model Transformer, Crosscutting Concern Manager, CTL Generator, and Model Checker. The Model Transformer converts an activity diagram to a Petri net automatically. The inputs of Model Transformer are UML diagrams designed by Topcased in the form of XML file and the outputs of the tool are Petri net files which are readable for LoLA to perform verification tasks. The Crosscutting Concern Manager is used to manage mapping relations between crosscutting concerns in requirements and elements in corresponding activity diagrams. It provides an assistant for mapping textual crosscutting requirements to design activity diagrams. The CTL Generator can automatically generate CTL formulas from crosscutting requirements that are mapped to design models. The CTL Generator also supports users to input CTL formulas manually. Model Checker is implemented by directly wrapped an existing checker, LoLA. It can verify the Petri net against crosscutting properties in the format of CTL formulas and report the result.

Figure1 The freamework of Jasmine-AOV

   To evaluate the effectiveness of our approach, we have applied our approach to the design models adapted from the Ship Order example in [4] and the Telecom System in [5]. The Ship Order example contains 5 crosscutting concerns and the Telecom System contains 6 crosscutting concerns. For both of the 2 case studies, we transformed the integrated models to Petri nets, and mapped crosscutting requirements to the design models with the help of the tool. Then, corresponding CTL formulas of verification tasks are generated automatically. Finally, the Petri nets are checked against the CTL formulas generated. The verifications are passed which means the Petri nets pass satisfies the crosscutting requirements。

   To further evaluate the ability of our approach to detect the faults of aspect-oriented models, mutated models are created based on preceding category of aspect model faults. 26 and 28 model mutants are constructed for the 2 case studies, respectively. Table 1 classifies all these model mutants by their fault types. All of them are killed because they violate the crosscutting requirements from various ways and these violations are detected by the verification process. This result illustrates the ability of our approach to find the faults in aspect-oriented models and to improve the quality of design models.

Table1 Model mutants of the 2 case studies

Reference

[1] Jasmine-AOV, http://cs.nju.edu.cn/lzwang/Jasmine-AOI/index.htm

[2] Topcased, http://www.topcased.org/

[3] LoLA, http://www.informatik.uni-rostock.de/tpp/lola/

[4] UML Superstructure V2.1, OMG, http://www.omg.org/technology/documents/ formal/uml.htm.

[5] AJDT Toolkit: http://www.eclipse.org/ajdt.

Software Engineering Group

Department of Computer Science and Technology

Nanjing University