We use cookies to improve your experience with our site.

Indexed in:

SCIE, EI, Scopus, INSPEC, DBLP, CSCD, etc.

Submission System
(Author / Reviewer / Editor)
Advanced Search
Volume 24 Issue 5
September  2009
Turn off MathJax
Article Contents
Abstract
References
Dian-Xiang Xu, Omar El-Ariss, Wei-Feng Xu, Lin-Zhang Wang. Aspect-Oriented Modeling and Verification with Finite State Machines[J]. Journal of Computer Science and Technology, 2009, 24(5): 949-961.
Citation: Dian-Xiang Xu, Omar El-Ariss, Wei-Feng Xu, Lin-Zhang Wang. Aspect-Oriented Modeling and Verification with Finite State Machines[J]. Journal of Computer Science and Technology, 2009, 24(5): 949-961.
shu

Aspect-Oriented Modeling and Verification with Finite State Machines

  • 1National Center for the Protection of the Financial Infrastructure, Dakota State University, Madison, SD 57042, U.S.A.
    2Department of Computer Science, North Dakota State University, Fargo, ND 58105, U.S.A.
    3Computer and Information Science Department, Gannon University, 109 University Square, Erie, PA 16541, U.S.A.
    4State Key Laboratory of Novel Software Technology, Department of Computer Science and Technology, Nanjing University, Nanjing 210093, China

Funds: 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.
More Information
  • Author Bio:

    Dian-Xiang Xu received the B.S., M.S., and Ph.D. degrees incomputer science from Nanjing University, China in 1989, 1992, and1995, respectively. He is currently an associate professor with theNational Center for the Protection of the Financial Infrastructure atDakota State University in South Dakota, USA. He was assistantprofessor of computer science at North Dakota State University fromJuly 2003 to May 2009, research assistant professor and engineer ofcomputer science at Texas A&M University from August 2000 to July2003, and research associate at Florida International University fromMay 1999 to August 2000. Prior to that, he was associate professor andassociate department chair of the Department of Computer Science andTechnology, Nanjing University. His research interests are in the areasof software security, software testing, aspect-oriented softwaredevelopment, and applied formal methods. He is a senior member of theIEEE.

    Omar El-Ariss received his B.S. and M.S. degrees in computerscience from the Lebanese American University, Beirut, Lebanon in 2001and 2005 respectively. He is currently pursuing his Ph.D. degree at theComputer Science Department in North Dakota State University. Hisresearch interests are in the areas of software safety, softwaresecurity, software modeling and verification, and software testing.

    Wei-Feng Xu received the B.S. and M.S. degrees in computer science fromSoutheast Missouri State University and Towson University in 2000 and2002, respectively. He received his Ph.D. degree in softwareengineering from North Dakota State University in 2007. Currently, Dr.Xu is the director of Keystone Software Development Institute and anassistant professor of software engineering at Gannon University inErie, PA. He also serves as an IT consultant for General Electric'sLocomotive Remote Diagnostics Service Center in developing aninnovative remote monitoring system. His research interests includesoftware testing and aspect-oriented software development. He is asenior member of the IEEE.

    Lin-Zhang Wang received his B.Sc. degree in computer sciencefrom the Shenyang University of Technology in 1995, and his Ph.D.degree in computer science from Nanjing University in 2005. He iscurrently an associate professor in the Department of Computer Scienceand Technology at Nanjing University, China. His research interest isin the area of software engineering, particularly model-driven softwaretesting and verification. He is a member of IEEE, ACM, and CCF.

  • Received Date: November 30, 2008
  • Revised Date: June 22, 2009
  • Published Date: September 04, 2009
    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.
    • FullText(HTML)
    • References (33)
  • [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.
    • Relative Articles
  • Supplements (0)

  • Cited by

    Periodical cited type(2)

    1. Babar Khan, Andreas Koch. Reflecting on the Past 17 Years of Shingled Magnetic Recording for Insights into Future Disk Transitions: A Survey. ACM Transactions on Storage, 2025. DOI:10.1145/3731453
    2. Peng Jin, Ping Xie, Zhu Yuan, et al. An Approach for RAID-6 Scaling Based on D-code. 2019 IEEE 5th International Conference on Computer and Communications (ICCC), DOI:10.1109/ICCC47050.2019.9064323

    Other cited types(0)

Catalog

    Get Citation
    XML
    Article views (24) PDF downloads (1842) Cited by(2)
    Related

    Copyright ©2025 JCST, All Rights Reserved     京ICP备05002829号-1

    Institute of Computing Technology, Chinese Academy of Sciences
    P.O. Box 2704, Beijing 100190, P.R. China

    Tel.: 86-10-62610746 E-mail: jcst@ict.ac.cn

    /

    DownLoad:  Full-Size Img  PowerPoint
    Return
    Return