A Formal Property Verification for Aspect-Oriented Programs in Software Development

Authors: Moustapha Bande, Hakima Ould-Slimane, Hanifa Boucheneb

Abstract:

Software development for complex systems requires efficient and automatic tools that can be used to verify the satisfiability of some critical properties such as security ones. With the emergence of Aspect-Oriented Programming (AOP), considerable work has been done in order to better modularize the separation of concerns in the software design and implementation. The goal is to prevent the cross-cutting concerns to be scattered across the multiple modules of the program and tangled with other modules. One of the key challenges in the aspect-oriented programs is to be sure that all the pieces put together at the weaving time ensure the satisfiability of the overall system requirements. Our paper focuses on this problem and proposes a formal property verification approach for a given property from the woven program. The approach is based on the control flow graph (CFG) of the woven program, and the use of a satisfiability modulo theories (SMT) solver to check whether each property (represented par one aspect) is satisfied or not once the weaving is done.

Keywords: Aspect-oriented programming, control flow graph, satisfiability modulo theories, property verification.

Digital Object Identifier (DOI): doi.org/10.5281/zenodo.1474658

References:

[1] Roger T Alexander, James M Bieman, and Anneliese A Andrews. Towards the systematic testing of aspect-oriented programs. Rapport technique, Colorado State University, 2004.
[2] Chitra Babu and Harshini Ramnath Krishnan. Fault model and test-case generation for the composition of aspects. ACM SIGSOFT Software Engineering Notes, 34(1):1–6, 2009.
[3] Mourad Badri, Linda Badri, and Maxime Bourque-Fortin. Generating unit test sequences for aspect-oriented programs: towards a formal approach using uml state diagrams. In Information and Communications Technology, 2005. Enabling Technologies for the New Knowledge Society: ITI 3rd International Conference on, pages 237–253. IEEE, 2005.
[4] Clark W Barrett, Roberto Sebastiani, Sanjit A Seshia, Cesare Tinelli, et al. Satisfiability modulo theories. Handbook of satisfiability, 185:825–885, 2009.
[5] Mario L Bernardi. Reverse engineering of aspect oriented systems to support their comprehension, evolution, testing and assessment. In Software Maintenance and Reengineering, 2008. CSMR 2008. 12th European Conference on, pages 290–293. IEEE, 2008.
[6] Juliana KF Bowles, Behzad Bordbar, and Mohammed Alwanain. Weaving true-concurrent aspects using constraint solvers. In Application of Concurrency to System Design (ACSD), 2016 16th International Conference on, pages 35–44. IEEE, 2016.
[7] Mariano Ceccato, Paolo Tonella, and Filippo Ricca. Is aop code easier or harder to test than oop code. In First Workshop on Testing Aspect-Oriented Program (WTAOP), Chicago, Illinois, 2005.
[8] Leonardo De Moura and Nikolaj Bjørner. Z3: An efficient smt solver. In International conference on Tools and Algorithms for the Construction and Analysis of Systems, pages 337–340. Springer, 2008.
[9] Giovanni Denaro and Mattia Monga. An experience on verification of aspect properties. In Proceedings of the 4th international workshop on Principles of software evolution, pages 186–189. ACM, 2001.
[10] Tzilla Elrad, Mehmet Aksit, Gregor Kiczales, Karl Lieberherr, and Harold Ossher. Discussing aspects of aop. Communications of the ACM, 44(10):33–38, 2001.
[11] Pascal Fradet and St´ephane Hong Tuan Ha. Aspects of availability: Enforcing timed properties to prevent denial of service. Science of Computer Programming, 75(7):516–542, 2010.
[12] Ivan Gustavo Franchin, Ot´avio Augusto Lazzarini Lemos, and Paulo Cesar Masiero. Pairwise structural testing of object and aspect-oriented java programs. In The 21th Software Engineering Brazilian Symposium, Joao Pessoa, PB, Brazil, 2007.
[13] Yujian Fu, Junhua Ding, and Phil Bording. An approach for modeling and analyzing crosscutting concerns. In Service Operations, Logistics and Informatics, 2009. SOLI’09. IEEE/INFORMS International Conference on, pages 91–97. IEEE, 2009.
[14] Kevin W Hamlen and Micah Jones. Aspect-oriented in-lined reference monitors. In Proceedings of the third ACM SIGPLAN workshop on Programming languages and analysis for security, pages 11–20. ACM, 2008.
[15] Md Nour Hossain, Wolfram Kahl, and Tom Maibaum. A graph transformation approach to introducing aspects into software architectures.
[16] Gregor Kiczales, Erik Hilsdale, Jim Hugunin, Mik Kersten, Jeffrey Palm, and William G Griswold. An overview of aspectj. In ECOOP 2001Object-Oriented Programming, pages 327–354. Springer, 2001.
[17] Gregor Kiczales, John Lamping, Anurag Mendhekar, Chris Maeda, Cristina Lopes, Jean-Marc Loingtier, and John Irwin. Aspect-oriented programming. Springer, 1997.
[18] Ot´avio Augusto Lazzarini Lemos and Paulo Cesar Masiero. A pointcut-based coverage analysis approach for aspect-oriented programs. Information Sciences, 181(13):2721–2746, 2011.
[19] Ot´avio Augusto Lazzarini Lemos, Auri Marcelo Rizzo Vincenzi, Jos´e Carlos Maldonado, and Paulo Cesar Masiero. Control and data flow structural testing criteria for aspect-oriented programs. Journal of Systems and Software, 80(6):862–882, 2007.
[20] Philippe Massicotte, Mourad Badri, and Linda Badri. Generating aspects-classes integration testing sequences a collaboration diagram based strategy. In Software Engineering Research, Management and Applications, 2005. Third ACIS International Conference on, pages 30–37. IEEE, 2005.
[21] Reza Meimandi Parizi and Abdul Azim Abdul Ghani. Ajcfgraph-aspectj control flow graph builder for aspect-oriented software. International Journal of Computer Science, 3:170–181, 2008.
[22] Volker Stolz and Eric Bodden. Temporal assertions using aspectj. Electronic Notes in Theoretical Computer Science, 144(4):109–124, 2006.
[23] Yasuyuki Tahara, Akihiko Ohsuga, and Shinichi Honiden. Formal verification of dynamic evolution processes of uml models using aspects. In Software Engineering for Adaptive and Self-Managing Systems (SEAMS), 2017 IEEE/ACM 12th International Symposium on, pages 152–162. IEEE, 2017.
[24] Naoyasu Ubayashi and Tetsuo Tamai. Aspect-oriented programming with model checking. In Proceedings of the 1st international conference on Aspect-oriented software development, pages 148–154. ACM, 2002.
[25] Fadi Wedyan and Sudipto Ghosh. A dataflow testing approach for aspect-oriented programs. In High-Assurance Systems Engineering (HASE), 2010 IEEE 12th International Symposium on, pages 64–73. IEEE, 2010.
[26] Dianxiang Xu, Izzat Alsmadi, and Weifeng Xu. Model checking aspect-oriented design specification. In Computer Software and Applications Conference, 2007. COMPSAC 2007. 31st Annual International, volume 1, pages 491–500. IEEE, 2007.
[27] Dianxiang Xu, Omar El-Ariss,Weifeng Xu, and Linzhang Wang. Testing aspect-oriented programs with finite state machines. Software Testing, Verification and Reliability, 22(4):267–293, 2012.
[28] Jianjun Zhao. Data-flow-based unit testing of aspect-oriented programs. In Computer Software and Applications Conference, 2003. COMPSAC 2003. Proceedings. 27th Annual International, pages 188–197. IEEE, 2003.