科研之友
微信
新浪微博
Facebook
分享链接
摘要
Aspect-oriented programming modularizes cross cutting concerns in to aspects with the advice invoked at the specified points of program execution. Aspects can be use din a harmful way that invalidates desired properties and even estroys 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 a reflected by the aspects in to 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 erectiveness of verification,we created a large number of a we aspect models and verified them against the system requirements. The results show that the verification has revealed all a wed models. This indicates that our approach is erective 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 be fore the system is implemented.
- 出版日期2009-9
- 单位计算机软件新技术国家重点实验室
