×

MAVEN: Modular aspect verification and interference analysis. (English) Zbl 1207.68206

Summary: 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.

MSC:

68Q60 Specification and verification (program logics, model checking, etc.)
68N19 Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.)
PDFBibTeX XMLCite
Full Text: DOI

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 · Zbl 1070.68016 · doi:10.1016/j.tcs.2004.09.019
[2] Balzarotti D, D’Ursi A, Cavallaro L, Monga M (2005) Slicing AspectJ woven code. In: Proc of foundations of aspect languages workshop (FOAL05)
[3] Bergmans L, Aksit M (2001) Composing crosscutting concerns using composition filters. CACM 44:51–57
[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
[5] Common aspect proof environment (CAPE) (2008). http://www.cs.technion.ac.il/\(\sim\)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 · Zbl 1046.68587
[7] Clarke EM Jr., Grumberg O, Peled DA (1999) Model checking. MIT Press, Cambridge
[8] Devereux B (2003) Compositional reasoning about aspects using alternating-time logic. In: Proc of foundations of aspect languages workshop (FOAL03)
[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
[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 · doi:10.1016/j.entcs.2005.04.019
[11] Filman RE, Elrad T, Clarke S, Akşit M (eds) (2005) Aspect-oriented software development. Addison-Wesley, Boston
[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 · Zbl 1186.68291
[13] Grumberg O, Long DE (1994) Model checking and modular verification. ACM Trans Program Lang Syst 16(3):843–871 · doi:10.1145/177492.177725
[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 · Zbl 1006.68536
[15] Havelund K, Pressburger T (2000) Model checking Java programs using Java PathFinder. Int J Softw Tools Technol Transf (STTT) 2(4) · Zbl 1059.68585
[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
[17] Katz E, Katz S (2008) Incremental analysis of interference among aspects. In: FOAL ’08. ACM, New York, pp 29–38
[18] Katz S (2006) Aspect categories and classes of temporal properties. Trans Aspect-Oriented Softw Dev 1:106–134. LNCS 3880 · Zbl 1165.68363 · doi:10.1007/11687061_4
[19] Katz S, Faitelson D The common aspect proof environment. Submitted for publication, 2009. See http://www.cs.technion.ac.il/\(\sim\)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 · Zbl 1077.68593
[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 · Zbl 0982.68552
[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 · Zbl 05571811 · doi:10.1007/978-3-642-02059-9_6
[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 · Zbl 0753.68003
[25] Owicki S, Gries D (1976) An axiomatic proof technique for parallel programs. Acta Inform 6:319–340 · Zbl 0324.68007 · doi:10.1007/BF00268134
[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)
[27] Sereni D, de Moor O (2003) Static analysis of aspects. In: AOSD, pp 30–39
[28] Sihman M, Katz S (2003) Superimposition and aspect-oriented programming. BCS Comput J 46(5):529–541 · Zbl 1077.68593 · doi:10.1093/comjnl/46.5.529
[29] Sipma HB (2003) A formal model for cross-cutting modular transition systems. In: Proc of foundations of aspect languages workshop (FOAL03)
[30] Storzer M, Krinke J (2003) Interference analysis for AspectJ. In: Proc of foundations of aspect languages workshop (FOAL03)
[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
[32] Zhao J (2002) Slicing aspect-oriented software. In: IEEE international workshop on programming comprehension, pp 251–260
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.