Document Open Access Logo

Mutation-Based Lifted Repair of Software Product Lines

Author Aleksandar S. Dimovski

PDF
Thumbnail PDF

File

LIPIcs.ECOOP.2024.12.pdf
  • Filesize: 1.06 MB
  • 24 pages

Document Identifiers

Author Details

Aleksandar S. Dimovski
  • Mother Teresa University, Skopje, North Macedonia

Cite AsGet BibTex

Aleksandar S. Dimovski. Mutation-Based Lifted Repair of Software Product Lines. In 38th European Conference on Object-Oriented Programming (ECOOP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 313, pp. 12:1-12:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
https://doi.org/10.4230/LIPIcs.ECOOP.2024.12

Abstract

This paper presents a novel lifted repair algorithm for program families (Software Product Lines - SPLs) based on code mutations. The inputs of our algorithm are an erroneous SPL and a specification given in the form of assertions. We use variability encoding to transform the given SPL into a single program, called family simulator, which is translated into a set of SMT formulas whose conjunction is satisfiable iff the simulator (i.e., the input SPL) violates an assertion. We use a predefined set of mutations applied to feature and program expressions of the given SPL. The algorithm repeatedly mutates the erroneous family simulator and checks if it becomes (bounded) correct. Since mutating an expression corresponds to mutating a formula in the set of SMT formulas encoding the family simulator, the search for a correct mutant is reduced to searching an unsatisfiable set of SMT formulas. To efficiently explore the huge state space of mutants, we call SAT and SMT solvers in an incremental way. The outputs of our algorithm are all minimal repairs in the form of minimal number of (feature and program) expression replacements such that the repaired SPL is (bounded) correct with respect to a given set of assertions. We have implemented our algorithm in a prototype tool and evaluated it on a set of #ifdef-based C programs (i.e., annotative SPLs). The experimental results show that our approach is able to successfully repair various interesting SPLs.

Subject Classification

ACM Subject Classification
  • Software and its engineering → Software product lines
  • Theory of computation → Abstraction
Keywords
  • Program repair
  • Software Product Lines
  • Code mutations
  • Variability encoding

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Supplementary Materials

References

  1. Rui Abreu, Peter Zoeteweij, and Arjan J. C. van Gemund. Spectrum-based multiple fault localization. In ASE 2009, 24th IEEE/ACM International Conference on Automated Software Engineering, Auckland, New Zealand, November 16-20, 2009, pages 88-99. IEEE Computer Society, 2009. URL: https://doi.org/10.1109/ASE.2009.25.
  2. Sven Apel, Don S. Batory, Christian Kästner, and Gunter Saake. Feature-Oriented Software Product Lines - Concepts and Implementation. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-37521-7.
  3. Sven Apel, Hendrik Speidel, Philipp Wendler, Alexander von Rhein, and Dirk Beyer. Detection of feature interactions using feature-aware verification. In 26th IEEE/ACM Int. Conf. on Automated Software Engineering (ASE 2011), pages 372-375, 2011. URL: https://doi.org/10.1109/ASE.2011.6100075.
  4. Sven Apel, Alexander von Rhein, Philipp Wendler, Armin Größlinger, and Dirk Beyer. Strategies for product-line verification: case studies and experiments. In 35th Inter. Conference on Software Engineering, ICSE '13, pages 482-491, 2013. URL: https://doi.org/10.1109/ICSE.2013.6606594.
  5. Aitor Arrieta, Sergio Segura, Urtzi Markiegi, Goiuria Sagardui, and Leire Etxeberria. Spectrum-based fault localization in software product lines. Inf. Softw. Technol., 100:18-31, 2018. URL: https://doi.org/10.1016/J.INFSOF.2018.03.008.
  6. Eric Bodden, Társis Tolêdo, Márcio Ribeiro, Claus Brabrand, Paulo Borba, and Mira Mezini. Spl^lift: statically analyzing software product lines in minutes instead of years. In ACM SIGPLAN Conference on PLDI '13, pages 355-364, 2013. Google Scholar
  7. Sheng Chen, Martin Erwig, and Eric Walkingshaw. An error-tolerant type system for variational lambda calculus. In ACM SIGPLAN International Conference on Functional Programming, ICFP'12, pages 29-40, 2012. URL: https://doi.org/10.1145/2364527.2364535.
  8. Edmund M. Clarke, Daniel Kroening, and Flavio Lerda. A tool for checking ANSI-C programs. In Tools and Algorithms for the Construction and Analysis of Systems, 10th International Conference, TACAS 2004, Proceedings, volume 2988 of LNCS, pages 168-176. Springer, 2004. URL: https://doi.org/10.1007/978-3-540-24730-2_15.
  9. Andreas Classen, Maxime Cordy, Pierre-Yves Schobbens, Patrick Heymans, Axel Legay, and Jean-François Raskin. Featured transition systems: Foundations for verifying variability-intensive systems and their application to LTL model checking. IEEE Trans. Software Eng., 39(8):1069-1089, 2013. URL: https://doi.org/10.1109/TSE.2012.86.
  10. Loris D'Antoni, Roopsha Samanta, and Rishabh Singh. Qlose: Program repair with quantitative objectives. In Computer Aided Verification - 28th International Conference, CAV 2016, Proceedings, Part II, volume 9780 of LNCS, pages 383-401. Springer, 2016. URL: https://doi.org/10.1007/978-3-319-41540-6_21.
  11. Leonardo Mendonça de Moura and Nikolaj Bjørner. Z3: an efficient SMT solver. In C. R. Ramakrishnan and Jakob Rehof, editors, Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, TACAS 2008. Proceedings, volume 4963 of LNCS, pages 337-340. Springer, 2008. URL: https://doi.org/10.1007/978-3-540-78800-3_24.
  12. Vidroha Debroy and W. Eric Wong. Using mutation to automatically suggest fixes for faulty programs. In Third International Conference on Software Testing, Verification and Validation, ICST 2010, pages 65-74. IEEE Computer Society, 2010. URL: https://doi.org/10.1109/ICST.2010.66.
  13. Aleksandar Dimovski and Danilo Gligoroski. Generating highly nonlinear boolean functions using a genetic algorithm. In 6th Int. Conference on Telecommunications in Modern Satellite, Cable and Broadcasting Service, TELSIKS 2003, volume 2 of IEEE, pages 604-607, 2003. URL: https://doi.org/10.1109/TELSKS.2003.1246297.
  14. Aleksandar S. Dimovski. Symbolic game semantics for model checking program families. In Model Checking Software - 23nd International Symposium, SPIN 2016, Proceedings, volume 9641 of LNCS, pages 19-37. Springer, 2016. Google Scholar
  15. Aleksandar S. Dimovski. Lifted static analysis using a binary decision diagram abstract domain. In Proceedings of the 18th ACM SIGPLAN International Conference on GPCE 2019, pages 102-114. ACM, 2019. URL: https://doi.org/10.1145/3357765.3359518.
  16. Aleksandar S. Dimovski. Ctl^⋆ family-based model checking using variability abstractions and modal transition systems. Int. J. Softw. Tools Technol. Transf., 22(1):35-55, 2020. URL: https://doi.org/10.1007/s10009-019-00528-0.
  17. Aleksandar S. Dimovski. Error invariants for fault localization via abstract interpretation. In Static Analysis - 30th International Symposium, SAS 2023, Proceedings, volume 14284 of LNCS, pages 190-211. Springer, 2023. URL: https://doi.org/10.1007/978-3-031-44245-2_10.
  18. Aleksandar S. Dimovski. Generalized program sketching by abstract interpretation and logical abduction. In Static Analysis - 30th International Symposium, SAS 2023, Proceedings, volume 14284 of LNCS, pages 212-230. Springer, 2023. URL: https://doi.org/10.1007/978-3-031-44245-2_11.
  19. Aleksandar S. Dimovski. Quantitative program sketching using decision tree-based lifted analysis. J. Comput. Lang., 75:101206, 2023. URL: https://doi.org/10.1016/J.COLA.2023.101206.
  20. Aleksandar S. Dimovski and Sven Apel. Lifted static analysis of dynamic program families by abstract interpretation. In 35th European Conference on Object-Oriented Programming, ECOOP 2021, volume 194 of LIPIcs, pages 14:1-14:28. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. URL: https://doi.org/10.4230/LIPIcs.ECOOP.2021.14.
  21. Aleksandar S. Dimovski, Sven Apel, and Axel Legay. Program sketching using lifted analysis for numerical program families. In NASA Formal Methods - 13th International Symposium, NFM 2021, Proceedings, volume 12673 of LNCS, pages 95-112. Springer, 2021. URL: https://doi.org/10.1007/978-3-030-76384-8_7.
  22. Aleksandar S. Dimovski, Sven Apel, and Axel Legay. Several lifted abstract domains for static analysis of numerical program families. Sci. Comput. Program., 213:102725, 2022. URL: https://doi.org/10.1016/J.SCICO.2021.102725.
  23. Aleksandar S. Dimovski, Claus Brabrand, and Andrzej Wasowski. Finding suitable variability abstractions for lifted analysis. Formal Aspects Comput., 31(2):231-259, 2019. URL: https://doi.org/10.1007/s00165-019-00479-y.
  24. Aleksandar S. Dimovski and Ranko Lazic. Compositional software verification based on game semantics and process algebra. Int. J. Softw. Tools Technol. Transf., 9(1):37-51, 2007. URL: https://doi.org/10.1007/S10009-006-0005-Y.
  25. Aleksandar S. Dimovski and Andrzej Wasowski. From transition systems to variability models and from lifted model checking back to UPPAAL. In Models, Algorithms, Logics and Tools, volume 10460 of LNCS, pages 249-268. Springer, 2017. URL: https://doi.org/10.1007/978-3-319-63121-9_13.
  26. Niklas Eén and Niklas Sörensson. An extensible sat-solver. In Theory and Applications of Satisfiability Testing, 6th International Conference, SAT 2003, volume 2919 of LNCS, pages 502-518. Springer, 2003. URL: https://doi.org/10.1007/978-3-540-24605-3_37.
  27. Paul Gazzillo and Robert Grimm. Superc: parsing all of C by taming the preprocessor. In Jan Vitek, Haibo Lin, and Frank Tip, editors, ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI '12, Beijing, China - June 11 - 16, 2012, pages 323-334. ACM, 2012. URL: https://doi.org/10.1145/2254064.2254103.
  28. Claire Le Goues, ThanhVu Nguyen, Stephanie Forrest, and Westley Weimer. Genprog: A generic method for automatic software repair. IEEE Trans. Software Eng., 38(1):54-72, 2012. URL: https://doi.org/10.1109/TSE.2011.104.
  29. Todd L. Graves, Mary Jean Harrold, Jung-Min Kim, Adam A. Porter, and Gregg Rothermel. An empirical study of regression test selection techiques. ACM Trans. Softw. Eng. Methodol., 10(2):184-208, 2001. URL: https://doi.org/10.1145/367008.367020.
  30. Alexandru F. Iosif-Lazar, Ahmad Salim Al-Sibahi, Aleksandar S. Dimovski, Juha Erik Savolainen, Krzysztof Sierszecki, and Andrzej Wasowski. Experiences from designing and validating a software modernization transformation (E). In 30th IEEE/ACM International Conference on Automated Software Engineering, ASE 2015, pages 597-607, 2015. URL: https://doi.org/10.1109/ASE.2015.84.
  31. Manu Jose and Rupak Majumdar. Cause clue clauses: error localization using maximum satisfiability. In Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2011, pages 437-446. ACM, 2011. URL: https://doi.org/10.1145/1993498.1993550.
  32. Christian Kästner. Virtual Separation of Concerns: Toward Preprocessors 2.0. PhD thesis, University of Magdeburg, Germany, May 2010. Google Scholar
  33. Christian Kästner, Sven Apel, Thomas Thüm, and Gunter Saake. Type checking annotation-based product lines. ACM Trans. Softw. Eng. Methodol., 21(3):14, 2012. Google Scholar
  34. Christian Kästner, Paolo G. Giarrusso, Tillmann Rendel, Sebastian Erdweg, Klaus Ostermann, and Thorsten Berger. Variability-aware parsing in the presence of lexical macros and conditional compilation. In OOPSLA'11, pages 805-824. ACM, 2011. Google Scholar
  35. Christian Kästner, Alexander von Rhein, Sebastian Erdweg, Jonas Pusch, Sven Apel, Tillmann Rendel, and Klaus Ostermann. Toward variability-aware testing. In FOSD '12, pages 1-8, 2012. Google Scholar
  36. Etienne Kneuss, Manos Koukoutos, and Viktor Kuncak. Deductive program repair. In Computer Aided Verification - 27th International Conference, CAV 2015, Proceedings, Part II, volume 9207 of LNCS, pages 217-233. Springer, 2015. URL: https://doi.org/10.1007/978-3-319-21668-3_13.
  37. Robert Könighofer and Roderick Bloem. Repair with on-the-fly program analysis. In 8th International Haifa Verification Conference, HVC 2012, volume 7857 of LNCS, pages 56-71. Springer, 2012. URL: https://doi.org/10.1007/978-3-642-39611-3_11.
  38. Jeff Kramer, Jeff Magee, Morris Sloman, and A. Lister. Conic: An integrated approach to distributed computer control systems. IEE Proc., 130(1):1-10, 1983. Google Scholar
  39. Mark H. Liffiton and Jordyn C. Maglalang. A cardinality solver: More expressive constraints for free - (poster presentation). In Theory and Applications of Satisfiability Testing - SAT 2012 - 15th International Conference, Proceedings, volume 7317 of LNCS, pages 485-486. Springer, 2012. URL: https://doi.org/10.1007/978-3-642-31612-8_47.
  40. Fan Long and Martin C. Rinard. Staged program repair with condition synthesis. In Proceedings of the 2015 10th Joint Meeting on ESEC/FSE 2015, pages 166-178. ACM, 2015. URL: https://doi.org/10.1145/2786805.2786811.
  41. Sergey Mechtaev, Manh-Dung Nguyen, Yannic Noller, Lars Grunske, and Abhik Roychoudhury. Semantic program repair using a reference implementation. In Proceedings of the 40th International Conference on Software Engineering, ICSE 2018, pages 129-139. ACM, 2018. URL: https://doi.org/10.1145/3180155.3180247.
  42. Sergey Mechtaev, Jooyong Yi, and Abhik Roychoudhury. Angelix: scalable multiline program patch synthesis via symbolic analysis. In Proceedings of the 38th International Conference on Software Engineering, ICSE 2016, pages 691-701. ACM, 2016. URL: https://doi.org/10.1145/2884781.2884807.
  43. Jan Midtgaard, Aleksandar S. Dimovski, Claus Brabrand, and Andrzej Wasowski. Systematic derivation of correct variability-aware program analyses. Sci. Comput. Program., 105:145-170, 2015. URL: https://doi.org/10.1016/j.scico.2015.04.005.
  44. Kien-Tuan Ngo, Thu-Trang Nguyen, Son Nguyen, and Hieu Dinh Vo. Variability fault localization: a benchmark. In SPLC '21: 25th ACM International Systems and Software Product Line Conference, Leicester, United Kingdom, September 6-11, 2021, Volume A, pages 120-125. ACM, 2021. URL: https://doi.org/10.1145/3461001.3473058.
  45. Hoang Duong Thien Nguyen, Dawei Qi, Abhik Roychoudhury, and Satish Chandra. Semfix: program repair via semantic analysis. In 35th International Conference on Software Engineering, ICSE '13, pages 772-781. IEEE Computer Society, 2013. URL: https://doi.org/10.1109/ICSE.2013.6606623.
  46. Thanh-Toan Nguyen, Quang-Trung Ta, and Wei-Ngan Chin. Automatic program repair using formal verification and expression templates. In Verification, Model Checking, and Abstract Interpretation - 20th International Conference, VMCAI 2019, Proceedings, volume 11388 of LNCS, pages 70-91. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-11245-5_4.
  47. Thu-Trang Nguyen, Kien-Tuan Ngo, Son Nguyen, and Hieu Dinh Vo. A variability fault localization approach for software product lines. IEEE Trans. Software Eng., 48(10):4100-4118, 2022. URL: https://doi.org/10.1109/TSE.2021.3113859.
  48. Yuhua Qi, Xiaoguang Mao, Yan Lei, Ziying Dai, and Chengsong Wang. The strength of random search on automated program repair. In 36th International Conference on Software Engineering, ICSE '14, pages 254-265. ACM, 2014. URL: https://doi.org/10.1145/2568225.2568254.
  49. Urmas Repinski, Hanno Hantson, Maksim Jenihhin, Jaan Raik, Raimund Ubar, Giuseppe Di Guglielmo, Graziano Pravadelli, and Franco Fummi. Combining dynamic slicing and mutation operators for ESL correction. In 17th IEEE European Test Symposium, ETS 2012, pages 1-6. IEEE Computer Society, 2012. URL: https://doi.org/10.1109/ETS.2012.6233020.
  50. Bat-Chen Rothenberg and Orna Grumberg. Sound and complete mutation-based program repair. In FM 2016: Formal Methods - 21st International Symposium, Proceedings, volume 9995 of LNCS, pages 593-611, 2016. URL: https://doi.org/10.1007/978-3-319-48989-6_36.
  51. Bat-Chen Rothenberg and Orna Grumberg. Must fault localization for program repair. In Computer Aided Verification - 32nd International Conference, CAV 2020, Proceedings, Part II, volume 12225 of LNCS, pages 658-680. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-53291-8_33.
  52. Armando Solar-Lezama. Program sketching. STTT, 15(5-6):475-495, 2013. URL: https://doi.org/10.1007/s10009-012-0249-7.
  53. Shin Hwei Tan, Jooyong Yi, Yulis, Sergey Mechtaev, and Abhik Roychoudhury. Codeflaws: a programming competition benchmark for evaluating automated program repair tools. In Proceedings of the 39th International Conference on Software Engineering, ICSE 2017 - Companion Volume, pages 180-182. IEEE Computer Society, 2017. URL: https://doi.org/10.1109/ICSE-C.2017.76.
  54. Thomas Thüm, Ina Schaefer, Martin Hentschel, and Sven Apel. Family-based deductive verification of software product lines. In Generative Programming and Component Engineering, GPCE'12, pages 11-20. ACM, 2012. URL: https://doi.org/10.1145/2371401.2371404.
  55. Alexander von Rhein, Jörg Liebig, Andreas Janker, Christian Kästner, and Sven Apel. Variability-aware static analysis at scale: An empirical study. ACM Trans. Softw. Eng. Methodol., 27(4):18:1-18:33, 2018. URL: https://doi.org/10.1145/3280986.
  56. Alexander von Rhein, Thomas Thüm, Ina Schaefer, Jörg Liebig, and Sven Apel. Variability encoding: From compile-time to load-time variability. J. Log. Algebraic Methods Program., 85(1):125-145, 2016. URL: https://doi.org/10.1016/j.jlamp.2015.06.007.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact