Incremental analysis of interference among aspects

ABSTRACT

Often, insertion of several aspects into one system is desired and in that case the problem of interference among the different aspects might arise, even if each aspect individually woven is correct relative to its specification. In this type of interference, one aspect can prevent another from having the required effect on a woven system. Such interference is defined and specifications of aspects are described. An incremental proof strategy based on model checking pairs of aspects for a generic model expressing the specifications is defined. When an aspect is added to a library of noninterfering aspects, only its interaction with each of the aspects from the library needs to be checked. Such checks for each pair of aspects are proven sufficient to detect interference or establish interference freedom for any order of application of any collection of aspects in a library. Implemented examples of interfering aspects are analyzed and the results are described, showing the advantage of the incremental strategy over a direct proof in space needed for the model check. Early analysis and detection of such interference in libraries of aspects will enable informed choice of the aspects to be applied, and of the weaving order.

REFERENCES

• 1: D. Balzarotti, A. D'Ursi, L. Cavallaro, and M. Monga. Slicing AspectJ woven code. In Proc. of Foundations of Aspect Languages Workshop (FOAL05), 2005.
• 2: Lodewijk Bergmans , Mehmet Aksit, Composing crosscutting concerns using composition filters, Communications of the ACM, v.44 n.10, p.51-57, Oct. 2001 [doi>10.1145/383845.383857]
• 3: Edmund M. Clarke, Jr. , Orna Grumberg , Doron A. Peled, Model checking, MIT Press, Cambridge, MA, 2000
• 4: Rémi Douence , Pascal Fradet , Mario Südholt, Composition, reuse and interaction analysis of stateful aspects, Proceedings of the 3rd international conference on Aspect-oriented software development, p.141-150, March 22-24, 2004, Lancaster, UK [doi>10.1145/976270.976288]
• 5: M. Goldman and S. Katz. MAVEN: Modular aspect verification. In Proc. of TACAS 2007, volume 4424 of LNCS, pages 308--322, 2007.
• 6: John Hatcliff , Matthew B. Dwyer, Using the Bandera Tool Set to Model-Check Properties of Concurrent Java Software, Proceedings of the 12th International Conference on Concurrency Theory, p.39-58, August 20-25, 2001
• 7: Wilke Havinga , Istvan Nagy , Lodewijk Bergmans , Mehmet Aksit, A graph-based approach to modeling and detecting composition conflicts related to introductions, Proceedings of the 6th international conference on Aspect-oriented software development, March 12-16, 2007, Vancouver, British Columbia, Canada [doi>10.1145/1218563.1218574]
• 8: E. Katz and S. Katz. Verifying scenario-based aspect specifications. In Proc. Formal Methods: International Symposium of Formal Methods Europe (FM05), volume 3582 of LNCS, pages 432--447. Springer, 2005.
• 9: S. Katz. Aspect categories and classes of temporal properties. Transactions on Aspect Oriented Software Development (TAOSD), 1:106--134, 2006. LNCS 3880.
• 10: S. Katz and M. Sihman. Aspect validation using model checking. In Proc. of International Symposium on Verification, LNCS 2772, pages 389--411, 2003.
• 11: Raffi Khatchadourian , Neelam Soundarajan, Rely-guarantee approach to reasoning about aspect-oriented programs, Proceedings of the 5th workshop on Software engineering properties of languages and aspect technologies, p.5-es, March 12-16, 2007, Vancouver, British Columbia, Canada [doi>10.1145/1233843.1233848]
• 12: Gregor Kiczales , Erik Hilsdale , Jim Hugunin , Mik Kersten , Jeffrey Palm , William G. Griswold, An Overview of AspectJ, Proceedings of the 15th European Conference on Object-Oriented Programming, p.327-353, June 18-22, 2001
• 13: Jörg Kienzle , Samuel Gélineau, AO challenge - implementing the ACID properties for transactional objects, Proceedings of the 5th international conference on Aspect-oriented software development, March 20-24, 2006, Bonn, Germany [doi>10.1145/1119655.1119683]
• 14: Shriram Krishnamurthi , Kathi Fisler , Michael Greenberg, Verifying aspect advice modularly, Proceedings of the 12th ACM SIGSOFT twelfth international symposium on Foundations of software engineering, October 31-November 06, 2004, Newport Beach, CA, USA
• 15: Zohar Manna , Amir Pnueli, The temporal logic of reactive and concurrent systems, Springer-Verlag New York, Inc., New York, NY, 1992
• 16: S. Owicki and D. Gries. An axiomatic proof technique for parallel programs. Acta Informatica, 6:319--340, 1976.
• 17: Martin Rinard , Alexandru Salcianu , Suhabe Bugrara, A classification system and analysis for aspect-oriented programs, Proceedings of the 12th ACM SIGSOFT twelfth international symposium on Foundations of software engineering, October 31-November 06, 2004, Newport Beach, CA, USA
• 18: M. Storzer and J. Krinke. Interference analysis for AspectJ. In Proc. of Foundations of Aspect Languages Workshop (FOAL03), 2003.
• 19: Toll system demonstrator. http://www.aosd-europe.net (under the "Industry" section).
• 20: Jianjun Zhao, Slicing Aspect-Oriented Software, Proceedings of the 10th International Workshop on Program Comprehension, p.251, June 27-29, 2002

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Model checking

Additional Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs

General Terms:
Languages, Verification

Keywords:
aspects, detection, interference, model-checking, specification