Aspect-Oriented Modeling and Verification with Finite State Machines
Aspect-Oriented Modeling and Verification with Finite State Machines
复制标题
使用有限状态机进行面向方面的建模和验证
DOI：
10.1007/s11390-009-9269-5
复制
发表时间：
2009-09
期刊：
影响因子：
--
通讯作者：
Wang, Lin-Zhang
中科院分区：
文献类型：
--
作者：
许巍峰;徐殿祥;Omar El-Ariss;Xu, Dian-Xiang;王林章;El-Ariss, Omar;Xu, Wei-Feng;Wang, Lin-Zhang
面向方面的编程将横切关注点模块化为方面，并在程序执行的指定点调用建议。方面可能以有害的方式使用，使所需的属性无效，甚至破坏程序的概念完整性。为了保证面向方面的系统的质量，严格的方面分析和设计是非常必要的。在本文中，我们提出了一种面向方面的建模和验证的方法与有限状态机。我们的方法提供了明确的符号（例如，切入点、建议和方面），用于捕获横切关注点和关于类状态模型的增量修改需求。为了验证的目的，我们组成的方面模型和类模型在一个面向方面的模型，通过编织机制。然后将编织模型和不受方面影响的类模型转换为FSP（有限状态过程），由LTSA（标记转换系统分析器）模型检查器根据所需的系统属性进行检查。我们已经将我们的方法的建模和验证的三个面向方面的系统。为了进一步评估验证的有效性，我们创建了大量的有缺陷的方面模型，并根据系统需求对其进行了验证。结果表明，验证已发现所有有缺陷的模型。这表明我们的方法是有效的面向方面的状态模型的质量保证。因此，我们的方法可以用于模型检查面向方面设计的基于状态的规格说明，并可以发现一些系统的设计问题之前，系统的实施。
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.
登录
查看更多内容
DOI：
10.1007/3-540-44685-0_5
发表时间：
2001-08
期刊：
--
影响因子：
--
作者：
J. Hatcliff;Matthew B. Dwyer
通讯作者：
J. Hatcliff;Matthew B. Dwyer
DOI：
10.1007/3-540-45429-2_14
发表时间：
2001-09
期刊：
--
影响因子：
--
作者：
J. Andrews
通讯作者：
J. Andrews
DOI：
10.1145/602461.602506
发表时间：
2001-09
期刊：
--
影响因子：
--
作者：
G. Denaro;Mattia Monga
通讯作者：
G. Denaro;Mattia Monga
DOI：
--
发表时间：
2004
期刊：
--
影响因子：
--
作者：
R. Alexander;J. Bieman;A. Andrews
通讯作者：
R. Alexander;J. Bieman;A. Andrews
DOI：
10.1007/3-540-45429-2_12
发表时间：
2001-09
期刊：
--
影响因子：
--
作者：
T. Nelson;D. Cowan;P. Alencar
通讯作者：
T. Nelson;D. Cowan;P. Alencar