Abstract
Aspects are program modules that include descriptions of key events (called joinpoints) 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. 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 single state machine constructed using the linear temporal logic (LTL) description of the assumptions, a description of the joinpoints, 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.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Kiczales, G., et al.: An overview of AspectJ. In: Knudsen, J.L. (ed.) ECOOP 2001. LNCS, vol. 2072, pp. 327–353. Springer, Heidelberg (2001)
Filman, R.E., et al. (eds.): Aspect-Oriented Software Development. Addison-Wesley, Boston (2005)
Sihman, M., Katz, S.: Superimposition and aspect-oriented programming. BCS Computer Journal 46(5), 529–541 (2003)
Abraham, E., et al.: An assertion-based proof system for multithreaded java. Theoretical Computer Science 331(2-3), 251–290 (2005)
Katz, S.: Aspect categories and classes of temporal properties. In: Rashid, A., Aksit, M. (eds.) Transactions on Aspect-Oriented Software Development I. LNCS, vol. 3880, pp. 106–134. Springer, Heidelberg (2006)
Clarke Jr., E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (1999)
Goldman, M.: Modular verification of aspects. MSc thesis, Technion — Israel Institute of Technology (2006), Available at http://www.cs.technion.ac.il/Labs/ssdl/thesis/finished/2006/max
Sereni, D., de Moor, O.: Static analysis of aspects. In: AOSD’03: Proc. 2nd Intl. Conf. on Aspect-oriented Software Development, pp. 30–39. ACM Press, New York (2003)
NuSMV: http://nusmv.irst.itc.it/
Douence, R., Südholt, M.: A model and a tool for Event-based Aspect-Oriented Programming (EAOP). TR 02/11/INFO, Ecole des Mines de Nantes (2002)
Krishnamurthi, S., Fisler, K., Greenberg, M.: Verifying aspect advice modularly. In: Proc. SIGSOFT Conference on Foundations of Software Engineering, FSE’04, pp. 137–146. ACM, New York (2004)
Katz, S., Sihman, M.: Aspect validation using model checking. In: Dershowitz, N. (ed.) Verification: Theory and Practice. LNCS, vol. 2772, pp. 389–411. Springer, Heidelberg (2004)
Hatcliff, J., Dwyer, M.: Using the Bandera Tool Set to model-check properties of concurrent Java software. In: Larsen, K.G., Nielsen, M. (eds.) CONCUR 2001. LNCS, vol. 2154, pp. 39–58. Springer, Heidelberg (2001)
Havelund, K., Pressburger, T.: Model checking Java programs using Java PathFinder. International Journal on Software Tools for Technology Transfer (STTT) 2(4) (2000)
Devereux, B.: Compositional reasoning about aspects using alternating-time logic. In: Proc. of Foundations of Aspect Languages Workshop, FOAL03 (2003)
Sipma, H.: A formal model for cross-cutting modular transition systems. In: Proc. of Foundations of Aspect Languages Workshop, FOAL03 (2003)
Grumberg, O., Long, D.E.: Model checking and modular verification. ACM Transactions on Programming Languages and Systems 16(3), 843–871 (1994)
Blundell, C., et al.: Parameterized interfaces for open system verification of product lines. In: Proc. 19th IEEE International Conference on Automated Software Engineering, ASE’04, Washington, DC, pp. 258–267. IEEE Computer Society, Los Alamitos (2004)
Guelev, D.P., Ryan, M.D., Schobbens, P.Y.: Model-checking the preservation of temporal properties upon feature integration. In: Proc. 4th Intl. Workshop on Automated Verification of Critical Systems (AVoCS). Electronic Notes in Theoretical Computer Science, vol. 128(6), pp. 311–324 (2004)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer Berlin Heidelberg
About this paper
Cite this paper
Goldman, M., Katz, S. (2007). MAVEN: Modular Aspect Verification. In: Grumberg, O., Huth, M. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2007. Lecture Notes in Computer Science, vol 4424. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-71209-1_24
Download citation
DOI: https://doi.org/10.1007/978-3-540-71209-1_24
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-71208-4
Online ISBN: 978-3-540-71209-1
eBook Packages: Computer ScienceComputer Science (R0)