暂缺

徐殿祥; 许巍峰; 王林章

暂缺

Aspect-Oriented Modeling and Verification with Finite State Machines

摘要

摘要: 面向方面的程序设计方法将横切关注点封装为方面（Aspect)，并提供了可在程序执行过程中特定的连接点调用通知（Advice)的机制。这种思想旨在提供确定、分离、表示和组合横切关注点的系统的方法，已被推广到软件开发的各个阶段、应用到不同抽象层次的软件工件（Artifact），对软件工程影响和作用已经得到公认。但我们认识到，作为人的智力产品，软件有其固有的复杂度，面向方面技术并不能确保软件的正确性、不能保证软件的设计与实现过程不引入缺陷，甚至，由于应用了面向方面技术还会引入新的问题，例如，方面可能会被错误使用，使期望的系统性质被破坏。如果等到系统已经实现后，再发现和排除这些缺陷，将耗费更大的成本。现代软件工程的理念是通过建模技术来分析和可视化软件设计，通过验证技术来分析设计模型是否满足需求，从而及时发现设计与实现制品中的缺陷，通过过程改进来避免缺陷的引入。现有面向方面的建模方法普遍扩展现有面向对象建模语言（如UML）以描述方面规约，但建模语言的形式化程度制约了严格验证。为了保证面向方面软件系统的质量，本文提出了使用有穷状态机进行面向方面建模和验证的方法。首先，在设计阶段，用类模型描述系统，用有限状态机对对象或类的行为进行建模；其次，采用面向方面的建模技术将横切关注点封装为方面，通过显式的符号（如Pointcut，Advice和Aspect等）扩展有限状态机模型，获取关于类状态模型的横切关注点和增量修改需求，并产生包括类模型、方面模型、方面优先规定等在内的面向方面的状态模型；最后，为了实施验证，我们首先通过编织机制将方面模型和类模型组合成面向方面模型，以产生全局视图，将编织好的模型及未被方面影响到的类模型转换为FSP进程，基于系统需求用性质进程或/和线型时序逻辑描述软件应该满足的性质，再使用LTSA模型检验器验证产生的FSP进程是否满足期望的系统性质，从而实现在软件开发早期分析软件设计是否满足需求。为了研究该方法的实用性，我们选择了汽车巡航控制、电信和银行系统等三个基于事件的模拟系统，执行了实例研究，采用了本文提出的面向方面建模方法为这三个系统构造了面向方面的状态模型；为进一步的评估该验证方法的有效性，我们设计了大量含有的缺陷的方面模型，使用本文提出的面向方面的验证方法验证它们是否满足系统需求。实验结果表明，此验证方法发现了所有被植入缺陷的模型。本文的主要贡献在于：（1）提出了基于有限状态机的面向方面建模方法，提供了处理横切关注点和增量修改需求的有效机制；（2）提出基于模型检验的面向方面状态模型的验证方法，能够在系统实现之前发现设计缺陷。理论和实验表明，本文提出方法能够及时发现设计的缺陷、有效地减低整体开发成本，为面向方面状态模型的质量提供了有效的保障。
Abstract: 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.
- aspect-oriented modeling /
- finite state machines /
- modeling /
- verification /
- model checking

HTML全文

参考文献()

[1]	Kiczales G, Hilsdale E, Hugunin J, Kersten M, Palm J, Griswold W G. An overview of AspectJ. In Proc. ECOOP2001, Budapest, Hungary, June 18-22, 2001, pp.327-353.
[2]	Kiczales G, Lamping J, Mendhekar A, Maeda C, Lopes C V, Loingtier J M, Irwin J. Aspect-oriented programming. In Proc. ECOOP1997, JyvÄaskylÄa, Finland, June 9-13, 1997, pp.220-242.
[3]	Rinard M, Salcianu A, Bugrara S. A classification system and analysis for aspect-oriented programs. In Proc. FSE 2004, New Delhi, India, Feb. 5-7, 2004, pp.147-158.
[4]	Sullivan K, Griswold W G, Song Y, Cai Y, Shonle M, Tewari N, Rajan H. Information hiding interfaces for aspect-oriented design. In Proc. ESEC/FSE 2005, Lisbon, Portugal, Sept. 5- 9, 2005, pp.166-175.
[5]	Xu D, Xu W. State-based incremental testing of aspectoriented programs. In Proc. the Fifth International Conf. Aspect-Oriented Software Development (AOSD2006), Bonn, Germany, March 20-24, 2006, pp.180-189.
[6]	Katz S. Aspect Categories and Classes of Temporal Properties. Transactions on Aspect-Oriented Software Development I, Rashid A, Aksit M (eds.), LNCS 3880, 2006, pp.106- 134.
[7]	Schauerhuber A, Schwinger W, Retschitzegger W, Wimmer M. A survey on aspect-oriented modeling approaches. Technical Report, Vienna University of Technology, January 2006, http://www.wit.at/people/schauerhuber/publications/aomSurvey/AOMSurvey2006-01-30.pdf.
[8]	Xu D, Alsmadi I, Xu W. Model checking aspect-oriented design specification. In Proc. the 31st Annual International Computer Software and Applications Conference (COMPSAC2007), Beijing, China, July 23-27, 2007, pp.491- 500.
[9]	Magee J, Kramer J. Concurrency: State Models and Java Programs. Second Edition, John Wiley & Sons Ltd, 2006.
[10]	Binder R V. Testing Object-Oriented Systems: Models, Patterns, and Tools. Addison-Wesley, 2000.
[11]	UML 2.0 superstructure and infrastructure specification. http://www.omg.org/technology/documents/formal/uml.htm.
[12]	Alexander R T, Bieman J M, Andrews A A. Towards the systematic testing of aspect-oriented programs. Technical Report, Colorado State University, 2004, http://www.cs.colostate.edu/»rta/publications/CS04-105.pdf.
[13]	Aldawud O, Bader F, Elrad T. Weaving with statecharts. In The Second International Workshop on Aspect-Oriented Modeling with UML, Dresden, Germany, Sept. 30-Oct. 4, 2002.
[14]	Chavez C, Lucena C. A meta-model for aspect-oriented modeling. In The 2nd Int. Workshop on Aspect-Oriented Modeling with UML, Dresden, Germany, Sept. 30-Oct. 4, 2002.
[15]	Clarke S, Walker R J. Generic Aspect-Oriented Design with Theme/UML. Aspect-Oriented Software Development. Filman R E, Elrad T, Clarke S, Aksit M (eds.), Boston: AddisonWesley, 2005, pp.425-458.
[16]	Han Y, Kniesel G, Cremers A B. A meta model and modeling notation for AspectJ. In The 5th Workshop on AspectOriented Modeling with UML, in conjunction with UML2004, Lisbon, Portugal, October 11-15, 2004.
[17]	Pawlak R, Duchien L, Florin G, Legond-Aubry F, Seinturier L, Martelli L. A UML notation for aspect-oriented software design. In The 1st Int. Workshop on Aspect-Oriented Modeling with UML, in conjunction with AOSD2002, Enschede, The Netherlands, April 22-26, 2002.
[18]	Stein D, Hanenberg S, Unland R. An UML-based aspectoriented design notation. In Proc. the 1st Int. Conf. Aspect-Oriented Software Development (AOSD2002), Enschede, The Netherlands, April 22-26, 2002, pp.106-112.
[19]	Stein D, Hanenberg S, Unland R. On representing join points in the UML. In The Second International Workshop on Aspect-Oriented Modeling with UML, Dresden, Germany, Sept. 30-Oct. 4, 2002.
[20]	Zavaleta E B, Fuster G G, Morillo J L. An approach to aspect modeling with UML 2.0. In The 5th Workshop on AspectOriented Modeling with UML, in conjunction with UML2004, Lisbon, Portugal, October 11-15, 2004.
[21]	Elrad T, Aldawud O, Bader A. Expressing Aspects Using UML Behavior and Structural Diagrams. AspectOriented Software Development, Filman et al. (eds.), Boston: Addison-Wesley, 2005, pp.459-478.
[22]	Xu D, Nygard K. Threat-driven modeling and verification of secure software using aspect-oriented Petri nets. IEEE Trans. Software Engineering. April 2006, 32(4): 265-278.
[23]	Ubayashi N, Tamai T. Aspect-oriented programming with model checking. In Proc. the First International Conf. Aspect-Oriented Software Development (AOSD2002), Enschede, The Netherlands, April 22-26, 2002, pp.148-154.
[24]	Denaro G, Monga M. An experience on verification of aspect properties. In International Workshop on Principles of Software Evolution (IWPSE 2001), Vienna, Austria, Sept. 10-11, 2001, pp.186-189.
[25]	Nelson T, Cowan D D, Alencar P S C. Supporting formal verification of crosscutting concerns. In Proc. Reflection, Kyoto, Japan, Sept. 25-28, 2001, pp.153-169.
[26]	Krishnamurthi S, Fisler K, Greenberg M. Verifying aspect advice modularly. In Proc. the 12th ACM SIGSOFT Symposium on Foundations of Software Engineering (FSE 2004), Newport Beach, USA, Oct. 31-Nov. 6, 2004, pp.137-146.
[27]	Katz S, Sihman M. Aspect-validation using model-checking. In Proc. the International Symposium on Verification, in honor of Zohar Manna, LNCS 2772, Springer-Verlag, 2003, pp.389-411, Also early version in FOAL 2003.
[28]	Sihman M, Katz S. Model checking applications of aspects and superimpositions. In Proc. Foundations of AspectOriented Languages, Bonn, Germany, March 20-24, 2003, pp.51-60.
[29]	Hatcliff J, Dwyer M. Using the Bandera tool set to modelcheck properties of concurrent Java software. In Proc. the 12th Int. Conf. Concurrency Theory (CONCUR2001), Aalborg, Denmark, LNCS 2154, Larsen K G, Nielsen M (eds.), Springer-Verlag, Aug. 20-25, 2001, pp.39-58.
[30]	Katz E, Katz S. Verifying scenario-based aspect specifications. In Proc. the International Symposium of Formal Methods Europe, Newcastle, UK, July 18-22, 2005, pp.432-447.
[31]	Goldman M, Katz S. Modular generic verification of LTL properties for aspects. In Proc. Foundations of Aspect Languages Workshop (FOAL2006), Bonn, Germany, March 20- 24, 2006.
[32]	Andrews J H. Process-algebraic foundations of aspectoriented programming. In Proc. Reflection, Kyoto, Japan Sept. 25-28, 2001, pp.187-209.
[33]	Xu J, Rajan H, Sullivan K. Aspect reasoning by reduction to implicit invocation. In Proc. Foundations of Aspect-Oriented Languages, Lancaster, UK, March 23, 2004.