Modular verification of strongly invasive aspects: summary

ABSTRACT

An extended specification for aspects, and a new verification method based on model checking are used to establish the correctness of strongly-invasive aspects, independently of any particular base program to which they may be woven. Such aspects can change the underlying base program variables to new states, and after the aspect advice has completed, the base program code continues from states that were previously unreachable.

REFERENCES

• 1: Alessandro Cimatti , Edmund M. Clarke , Fausto Giunchiglia , Marco Roveri, NUSMV: A New Symbolic Model Verifier, Proceedings of the 11th International Conference on Computer Aided Verification, p.495-499, July 06-10, 1999
• 2: Simplice Djoko Djoko , Rémi Douence , Pascal Fradet, Aspects preserving properties, Proceedings of the 2008 ACM SIGPLAN symposium on Partial evaluation and semantics-based program manipulation, January 07-08, 2008, San Francisco, California, USA [doi>10.1145/1328408.1328429]
• 3: M. Goldman and S. Katz. MAVEN: Modular aspect verification. In Proc. of TACAS 2007, volume 4424 of LNCS, pages 308--322, 2007.
• 4: E. Katz and S. Katz. Verifying scenario-based aspect specifications. In Proc. Formal Methods: International Symposium of Formal Methods Europe (FM'05), volume 3582 of LNCS, pages 432--447. Springer, 2005.
• 5: Emilia Katz , Shmuel Katz, Incremental analysis of interference among aspects, Proceedings of the 7th workshop on Foundations of aspect-oriented languages, p.29-38, April 01-01, 2008, Brussels, Belgium [doi>10.1145/1394496.1394500]
• 6: S. Katz. Aspect categories and classes of temporal properties. Transactions on Aspect Oriented Software Development (TAOSD), 1:106--134, 2006. LNCS 3880.
• 7: S. Katz and M. Sihman. Aspect validation using model checking. In Proc. of International Symposium on Verification, LNCS 2772, pages 389--411, 2003.
• 8: Shriram Krishnamurthi , Kathi Fisler, Foundations of incremental aspect model-checking, ACM Transactions on Software Engineering and Methodology (TOSEM), v.16 n.2, p.7-es, April 2007 [doi>10.1145/1217295.1217296]
• 9: Matthew W. Moskewicz , Conor F. Madigan , Ying Zhao , Lintao Zhang , Sharad Malik, Chaff: engineering an efficient SAT solver, Proceedings of the 38th conference on Design automation, p.530-535, June 2001, Las Vegas, Nevada, United States [doi>10.1145/378239.379017]
• 10: 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
• 11: H.B. Sipma. A formal model for cross-cutting modular transition systems. In FOAL'03, 2003.
• 12: N. Weston, F. Taiani, and A. Rashid. Interaction analysis for fault-tolerance in aspect-oriented programming. In MeMoT'07, pages 95--102, 2007.

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, model-checking, modularity, specification