TY - JOUR
T1 - Aspect-Oriented Modeling and Verification with Finite State Machines
AU - Xu, Dian Xiang
AU - El-Ariss, Omar
AU - Xu, Wei Feng
AU - Wang, Lin Zhang
N1 - Funding Information:
Regular Paper The research was supported in part by the ND EPSCoR IIP-SG via NSF of USA under Grant No. EPS-047679. The fourth author was supported in part by the National Natural Science Foundation of China under Grant No. 60603036, the National Basic Research 973 Program of China under Grant No. 2009CB320702, and the National High-Tech Research and Development 863 Program of China under Grant No. 2009AA01Z148.
PY - 2009/9
Y1 - 2009/9
N2 - Aspect-oriented programming modularizes crosscutting concerns into aspects with the advice invoked at the specified points of program execution. Aspects can be used in a harmful way that invalidates desired properties and even destroys the conceptual integrity of programs. To assure the quality of an aspect-oriented system, rigorous analysis and design of aspects are highly desirable. In this paper, we present an approach to aspect-oriented modeling and verification with finite state machines. Our approach provides explicit notations (e.g., pointcut, advice and aspect) for capturing crosscutting concerns and incremental modification requirements with respect to class state models. For verification purposes, we compose the aspect models and class models in an aspect-oriented model through a weaving mechanism. Then we transform the woven models and the class models not affected by the aspects into FSP (Finite State Processes), which are to be checked by the LTSA (Labeled Transition System Analyzer) model checker against the desired system properties. We have applied our approach to the modeling and verification of three aspect-oriented systems. To further evaluate the effectiveness of verification, we created a large number of flawed aspect models and verified them against the system requirements. The results show that the verification has revealed all flawed models. This indicates that our approach is effective in quality assurance of aspect-oriented state models. As such, our approach can be used for model-checking state-based specification of aspect-oriented design and can uncover some system design problems before the system is implemented.
AB - Aspect-oriented programming modularizes crosscutting concerns into aspects with the advice invoked at the specified points of program execution. Aspects can be used in a harmful way that invalidates desired properties and even destroys the conceptual integrity of programs. To assure the quality of an aspect-oriented system, rigorous analysis and design of aspects are highly desirable. In this paper, we present an approach to aspect-oriented modeling and verification with finite state machines. Our approach provides explicit notations (e.g., pointcut, advice and aspect) for capturing crosscutting concerns and incremental modification requirements with respect to class state models. For verification purposes, we compose the aspect models and class models in an aspect-oriented model through a weaving mechanism. Then we transform the woven models and the class models not affected by the aspects into FSP (Finite State Processes), which are to be checked by the LTSA (Labeled Transition System Analyzer) model checker against the desired system properties. We have applied our approach to the modeling and verification of three aspect-oriented systems. To further evaluate the effectiveness of verification, we created a large number of flawed aspect models and verified them against the system requirements. The results show that the verification has revealed all flawed models. This indicates that our approach is effective in quality assurance of aspect-oriented state models. As such, our approach can be used for model-checking state-based specification of aspect-oriented design and can uncover some system design problems before the system is implemented.
UR - http://www.scopus.com/inward/record.url?scp=70349606643&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=70349606643&partnerID=8YFLogxK
U2 - 10.1007/s11390-009-9269-5
DO - 10.1007/s11390-009-9269-5
M3 - Article
AN - SCOPUS:70349606643
SN - 1000-9000
VL - 24
SP - 949
EP - 961
JO - Journal of Computer Science and Technology
JF - Journal of Computer Science and Technology
IS - 5
ER -