Skip to main content
SpringerLink
Log in

MAVEN: modular aspect verification and interference analysis

  • Published:
Formal Methods in System Design Aims and scope Submit manuscript

Abstract

Aspects are program modules that include descriptions of key events (called join-points) and code segments (called advice) to be executed at those key events when the aspect is bound (woven) to an underlying system. The MAVEN tool verifies the correctness of an aspect relative to its specification, independently of any specific underlying system to which it may be woven, and also allows establishing noninterference among aspects, or detecting potential interference. The specification includes assumptions about properties of the underlying system, and guaranteed properties of any system after the aspect is woven into it. The approach is based on model checking of a state machine constructed using the linear temporal logic (LTL) description of the assumptions, a description of the join-points, and the state machine of the aspect advice. The tableau of the LTL assumption is used in a unique way, as a representative of any underlying system satisfying the assumptions. This is the first technique for once-and-for-all verification of an aspect relative to its specification, thereby increasing the modularity of proofs for systems with aspects. The individual correctness proofs along with proofs of interference freedom are appropriate for a library of reusable aspects, when multiple aspects are to be woven to a system.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Similar content being viewed by others

References

  1. Abraham E, de Boer F, de Roever W, Steffen M (2005) An assertion-based proof system for multithreaded Java. Theor Comput Sci 331(2–3):251–290

    Article  MATH  Google Scholar 

  2. Balzarotti D, D’Ursi A, Cavallaro L, Monga M (2005) Slicing AspectJ woven code. In: Proc of foundations of aspect languages workshop (FOAL05)

    Google Scholar 

  3. Bergmans L, Aksit M (2001) Composing crosscutting concerns using composition filters. CACM 44:51–57

    Google Scholar 

  4. Blundell C, Fisler K, Krishnamurthi S, Hentenryck PV (2004) Parameterized interfaces for open system verification of product lines. In: Proc 19th IEEE international conference on automated software engineering (ASE’04), pp 258–267

    Chapter  Google Scholar 

  5. Common aspect proof environment (CAPE) (2008). http://www.cs.technion.ac.il/~ssdl/research/cape

  6. Cimatti A, Clarke EM, Giunchiglia F, Roveri M (1999) NuSMV: a new symbolic model verifier. In: CAV’99. Lecture notes in computer science, vol 1633. Springer, Berlin, pp 495–499. http://nusmv.itc.it

    Google Scholar 

  7. Clarke EM Jr., Grumberg O, Peled DA (1999) Model checking. MIT Press, Cambridge

    Google Scholar 

  8. Devereux B (2003) Compositional reasoning about aspects using alternating-time logic. In: Proc of foundations of aspect languages workshop (FOAL03)

    Google Scholar 

  9. Douence R, Fradet P, Sudholt M (2004) Composition, reuse, and interaction analysis of stateful aspects. In: Proc of 3th intl conf on aspect-oriented software development (AOSD’04). ACM, New York, pp 141–150

    Chapter  Google Scholar 

  10. Guelev DP, Ryan MD, Schobbens PY (2004) Model-checking the preservation of temporal properties upon feature integration. In: Proc 4th intl workshop on automated verification of critical systems (AVoCS’04). Electron Notes Theor Comput Sci 128(6):311–324

    Article  Google Scholar 

  11. Filman RE, Elrad T, Clarke S, Akşit M (eds) (2005) Aspect-oriented software development. Addison-Wesley, Boston

    Google Scholar 

  12. Goldman M, Katz S (2007) MAVEN: Modular aspect verification. In: Proc of TACAS 2007. Lecture notes in computer science, vol 4424. Springer, Berlin, pp 308–322

    Google Scholar 

  13. Grumberg O, Long DE (1994) Model checking and modular verification. ACM Trans Program Lang Syst 16(3):843–871

    Article  Google Scholar 

  14. Hatcliff J, Dwyer M (2001) Using the Bandera Tool Set to model-check properties of concurrent Java software. In: Larsen KG, Nielsen M (eds) Proc 12th int conf on concurrency theory, CONCUR’01. Lecture notes in computer science, vol 2154. Springer, Berlin, pp 39–58

    Google Scholar 

  15. Havelund K, Pressburger T (2000) Model checking Java programs using Java PathFinder. Int J Softw Tools Technol Transf (STTT) 2(4)

  16. Havinga W, Nagy I, Bergmans L, Aksit M (2007) A graph-based approach to modeling and detecting composition conflicts related to introductions. In: AOSD ’07. ACM, New York, pp 85–95

    Chapter  Google Scholar 

  17. Katz E, Katz S (2008) Incremental analysis of interference among aspects. In: FOAL ’08. ACM, New York, pp 29–38

    Chapter  Google Scholar 

  18. Katz S (2006) Aspect categories and classes of temporal properties. Trans Aspect-Oriented Softw Dev 1:106–134. LNCS 3880

    Article  Google Scholar 

  19. Katz S, Faitelson D The common aspect proof environment. Submitted for publication, 2009. See http://www.cs.technion.ac.il/~ssdl/research/cape/index.html

  20. Katz S, Sihman M (2003) Aspect validation using model checking. In: Proc of international symposium on verification. Lecture notes in computer science, vol 2772. Springer, Berlin, pp 389–411

    Google Scholar 

  21. Kiczales G, Hilsdale E, Hugunin J, Kersten M, Palm J, Griswold WG (2001) An overview of AspectJ. In: Proc ECOOP 2001. Lecture notes in computer science, vol 2072. Springer, Berlin, pp 327–353. http://aspectj.org

    Google Scholar 

  22. Kienzle J, Duala-Ekoko E, Gélineau S (2009) AspectOptima: A case study on aspect dependencies and interactions. Trans Aspect-Oriented Softw Dev 5:187–234

    Article  Google Scholar 

  23. Krishnamurthi S, Fisler K (2007) Foundations of incremental aspect model-checking. ACM Trans Softw Eng Methodol (TOSEM) 16(2)

  24. Manna Z, Pnueli A (1991) The temporal logic of reactive and concurrent systems: specification. Springer, Berlin

    MATH  Google Scholar 

  25. Owicki S, Gries D (1976) An axiomatic proof technique for parallel programs. Acta Inform 6:319–340

    Article  MATH  MathSciNet  Google Scholar 

  26. Rinard M, Salcianu A, Bugrara S (2004) A classification system and analysis for aspect-oriented programs. In: Proc of international conference on foundations of software engineering (FSE04)

    Google Scholar 

  27. Sereni D, de Moor O (2003) Static analysis of aspects. In: AOSD, pp 30–39

    Google Scholar 

  28. Sihman M, Katz S (2003) Superimposition and aspect-oriented programming. BCS Comput J 46(5):529–541

    MATH  Google Scholar 

  29. Sipma HB (2003) A formal model for cross-cutting modular transition systems. In: Proc of foundations of aspect languages workshop (FOAL03)

    Google Scholar 

  30. Storzer M, Krinke J (2003) Interference analysis for AspectJ. In: Proc of foundations of aspect languages workshop (FOAL03)

    Google Scholar 

  31. Weston N, Taiani F, Rashid A (2007) Interaction analysis for fault-tolerance in aspect-oriented programming. In: Proc workshop on methods, models, and tools for fault tolerance, MeMoT’07, pp 95–102

    Google Scholar 

  32. Zhao J (2002) Slicing aspect-oriented software. In: IEEE international workshop on programming comprehension, pp 251–260

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Computer Science Department, MIT, Cambridge, MA, USA

    Max Goldman

  2. Computer Science Department, Technion, Haifa, Israel

    Emilia Katz & Shmuel Katz

Authors
  1. Max Goldman
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Emilia Katz
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Shmuel Katz
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Emilia Katz.

Rights and permissions

Reprints and permissions

About this article

Cite this article

Goldman, M., Katz, E. & Katz, S. MAVEN: modular aspect verification and interference analysis. Form Methods Syst Des 37, 61–92 (2010). https://doi.org/10.1007/s10703-010-0101-1

Download citation

  • Received:

  • Accepted:

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s10703-010-0101-1

Keywords

Search

Navigation