Aspect-oriented programming with model checking

ABSTRACT

Aspect-oriented programming (AOP) is a programming paradigm such that crosscutting concerns including synchronization policies, resource sharing and performance optimizations over objects are modularized as aspects that are separated from objects. A compiler, called a weaver, weaves aspects and objects together into a program. In AOP, however, it is not easy to verify the correctness of a woven program because crucial behaviors are strongly influenced by aspect descriptions. In order to deal with such problem, this paper proposes an automatic verification approach using model checking that verifies whether the woven program contains unexpected behaviors such as deadlocks. The objectives of this paper are as follows: 1) to verify the correctness of AOP-based programs using model checking, 2) to provide AOP-based model checking frameworks.

REFERENCES

• 1: Mehmet Aksit , Anand Tripathi, Data abstraction mechanisms in SINA/ST, Conference proceedings on Object-oriented programming systems, languages and applications, p.267-275, September 25-30, 1988, San Diego, California, United States
• 2: AspectJ. http://aspectj.org/.
• 3: The AspectJ Programming Guide, 2001.
• 4: Bandera. http://www.cis.ksu.edu/ santos/bandera/.
• 5: Kent Beck, Extreme programming explained: embrace change, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1999
• 6: Edmund M. Clarke, Jr. , Orna Grumberg , Doron A. Peled, Model checking, MIT Press, Cambridge, MA, 2000
• 7: James C. Corbett , Matthew B. Dwyer , John Hatcliff , Shawn Laubach , Corina S. Păsăreanu , Robby , Hongjun Zheng, Bandera: extracting finite-state models from Java source code, Proceedings of the 22nd international conference on Software engineering, p.439-448, June 04-11, 2000, Limerick, Ireland [doi>10.1145/337180.337234]
• 8: Czarnecki, K. and Eisenecker, U. W.: Generative Programming, Addison-Wesley, 2000.
• 9: Demeter Project. http://www.ccs.neu.edu/research/demeter/.
• 10: Tzilla Elrad , Robert E. Filman , Atef Bader, Aspect-oriented programming: Introduction, Communications of the ACM, v.44 n.10, p.29-32, Oct. 2001 [doi>10.1145/383845.383853]
• 11: William Harrison , Harold Ossher, Subject-oriented programming: a critique of pure objects, Proceedings of the eighth annual conference on Object-oriented programming systems, languages, and applications, p.411-428, September 26-October 01, 1993, Washington, D.C., United States
• 12: Havelund, K.: Java PathFinder User Guide, 1999.
• 13: Gerard J. Holzmann, The Model Checker SPIN, IEEE Transactions on Software Engineering, v.23 n.5, p.279-295, May 1997 [doi>10.1109/32.588521]
• 14: Daniel Jackson , Ian Schechter , Hya Shlyahter, Alcoa: the alloy constraint analyzer, Proceedings of the 22nd international conference on Software engineering, p.730-733, June 04-11, 2000, Limerick, Ireland [doi>10.1145/337180.337616]
• 15: Elizabeth A. Kendall, Role model designs and implementations with aspect-oriented programming, Proceedings of the 14th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, p.353-369, November 01-05, 1999, Denver, Colorado, United States
• 16: Kiczales, G., Lamping, J., Mendhekar A., Maeda, C., Lopes, C., Loingtier, J. and Irwin, J.: Aspect-Oriented Programming, Proc. ECOOP'97, Lecture Notes in Computer Science, Springer, vol.1241, pp.220-242, 1997.
• 17: Kenneth L. McMillan, Symbolic Model Checking, Kluwer Academic Publishers, Norwell, MA, 1993
• 18: Bertrand Meyer, Object-oriented software construction (2nd ed.), Prentice-Hall, Inc., Upper Saddle River, NJ, 1997
• 19: Torsten Nelson , Donald D. Cowan , Paulo S. C. Alencar, Supporting Formal Verification of Crosscutting Concerns, Proceedings of the Third International Conference on Metalevel Architectures and Separation of Crosscutting Concerns, p.153-169, September 25-28, 2001
• 20: K. Rustan M. Leino, Greg Nelson, and James B. Saxe: ESC/Java User's Manual, 2000.
• 21: Tamai, T.: Objects and roles: modeling based on the dualistic view, Information and Software Technology, Vol.41, No.14, pp.1005-1010, 1999.
• 22: Naoyasu Ubayashi , Tetsuo Tamai, Separation of Concerns in Mobile Agent Applications, Proceedings of the Third International Conference on Metalevel Architectures and Separation of Crosscutting Concerns, p.89-109, September 25-28, 2001

INDEX TERMS

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

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.2 Design Tools and Techniques
      D.2.3 Coding Tools and Techniques

General Terms:
Design, Languages, Verification

Keywords:
checking frameworks, model checking, validation