A Formal Property Verification for Aspect-Oriented Programs in Software Development
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.
[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.
[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.
@article{"International Journal of Information, Control and Computer Sciences:77955", author = "Moustapha Bande and Hakima Ould-Slimane and Hanifa Boucheneb", title = "A Formal Property Verification for Aspect-Oriented Programs in Software Development", 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.", volume = "12", number = "9", pages = "769-8", }
