Elias Kuiter
Alexander Knüppel
ABSTRACT
Highly-customizable software systems in form of software product lines are becoming increasingly relevant for safety-critical systems, in which the correctness of software is a major concern. To ensure the correct behavior of a software product line, each product can be verified in isolation—however, this strategy quickly becomes infeasible for a large number of products.
In this paper, we propose proof plans, a novel strategy for verifying feature-oriented software product lines based on partial proofs. Our technique splits the verification task into small proofs that can be reused across method variants, which gives rise to a wider spectrum of verification strategies for software product lines. We describe applications of our technique and evaluate one of them on a case study by comparing it with established verification strategies.
- Wolfgang Ahrendt, Bernhard Beckert, Richard Bubel, Reiner Hähnle, Peter H. Schmitt, and Mattias Ulbrich (Eds.). 2016. Deductive Software Verification – The KeY Book. Springer.Google Scholar
- Sofia Ananieva, Sandra Greiner, Thomas Kühn, Jacob Krüger, Lukas Linsbauer, Sten Grüner, Timo Kehrer, Heiko Klare, Anne Koziolek, Henrik Lönn, Sebastian Krieter, Christoph Seidl, S. Ramesh, Ralf Reussner, and Bernhard Westfechtel. 2020. A Conceptual Model for Unifying Variability in Space and Time. In Proceedings of the 24th ACM Conference on Systems and Software Product Line: Volume A - Volume A(Montreal, Quebec, Canada) (SPLC ’20). Association for Computing Machinery, New York, NY, USA, Article 15, 12 pages. https://doi.org/10.1145/3382025.3414955 Google ScholarDigital Library
- Sven Apel, Don Batory, Christian Kästner, and Gunter Saake. 2013. Feature-Oriented Software Product Lines. Springer. Google ScholarDigital Library
- Sven Apel, Christian Kästner, and Christian Lengauer. 2009. FeatureHouse: Language-Independent, Automated Software Composition. In Proceedings of the International Conference on Software Engineering. IEEE. https://doi.org/10.1109/icse.2009.5070523 Google ScholarDigital Library
- Sven Apel, Hendrik Speidel, Philipp Wendler, Alexander von Rhein, and Dirk Beyer. 2011. Detection of Feature Interactions using Feature-Aware Verification. In Proceedings of the International Conference on Automated Software Engineering. IEEE, 372–375. https://doi.org/10.1109/ase.2011.6100075 Google ScholarDigital Library
- Sven Apel, Alexander von Rhein, Thomas Thüm, and Christian Kästner. 2013. Feature-interaction detection based on feature-based specifications. Computer Networks 57, 12 (2013), 2399–2409. https://doi.org/10.1016/j.comnet.2013.02.025 Feature Interaction in Communications and Software Systems. Google ScholarDigital Library
- Don Batory, Jacob Neal Sarvela, and Axel Rauschmayer. 2004. Scaling Step-Wise Refinement. IEEE Transactions on Software Engineering 30, 6 (2004), 355–371. https://doi.org/10.1109/TSE.2004.23 Google ScholarDigital Library
- Richard Bubel, Ferruccio Damiani, Reiner Hähnle, Einar Broch Johnsen, Olaf Owe, Ina Schaefer, and Ingrid Chieh Yu. 2016. Proof Repositories for Compositional Verification of Evolving Software Systems. In Transactions on Foundations for Mastering Change I, Bernhard Steffen (Ed.). Springer, 130–156. https://doi.org/10.1007/978-3-319-46508-1_8Google Scholar
- Richard Bubel, Reiner Hähnle, and Maria Pelevina. 2014. Fully Abstract Operation Contracts. In Proceedings of the International Symposium On Leveraging Applications of Formal Methods, Verification and Validation, Tiziana Margaria and Bernhard Steffen (Eds.). Springer, 120–134. https://doi.org/10.1007/978-3-662-45231-8_9Google ScholarCross Ref
- Paul Clements and Linda Northrop. 2002. Software Product Lines: Practices and Patterns. Addison-Wesley.Google ScholarDigital Library
- Edsger W. Dijkstra. 1975. Guarded Commands, Nondeterminacy and Formal Derivation of Programs. Commun. ACM 18, 8 (1975), 453–457. https://doi.org/10.1145/360933.360975 Google ScholarDigital Library
- Ramez Elmasri and Shamkant Navathe. 2010. Fundamentals of Database Systems. Addison-Wesley. Google ScholarDigital Library
- Shannon Fischer, Lukas Linsbauer, Roberto E. Lopez-Herrejon, and Alexander Egyed. 2014. Enhancing Clone-and-Own with Systematic Reuse for Developing Software Variants. In Proceedings of the International Conference on Software Maintenance and Evolution. IEEE, 391–400. https://doi.org/10.1109/ICSME.2014.61 Google ScholarDigital Library
- David Harel. 1979. First-Order Dynamic Logic. Springer. https://doi.org/10.1007/3-540-09237-4 Google ScholarDigital Library
- Marlen Herter-Bernier. 2021. Verifikation Evolvierender Softwareproduktlinien mittels Uninterpretierter Prädikate. Master’s thesis. Technische Universität Braunschweig.Google Scholar
- C. A. R. Hoare. 1969. An Axiomatic Basis for Computer Programming. Commun. ACM 12, 10 (1969), 576–580. https://doi.org/10.1145/363235.363259 Google ScholarDigital Library
- Reiner Hähnle, Ina Schaefer, and Richard Bubel. 2013. Reuse in Software Verification by Abstract Method Calls. In Proceedings of the International Conference on Automated Deduction. Springer, 300–314. https://doi.org/10.1007/978-3-642-38574-2_21 Google ScholarDigital Library
- Kyo C. Kang, Sholom G. Cohen, James A. Hess, William E. Novak, and A. Spencer Peterson. 1990. Feature-Oriented Domain Analysis (FODA) Feasibility Study. Technical Report CMU/SEI-90-TR-21. Software Engineering Institute, Carnegie Mellon University.Google Scholar
- Vladimir Klebanov. 2007. Proof Reuse. In Verification of Object-Oriented Software. The KeY Approach, Bernhard Beckert, Reiner Hähnle, and Peter H. Schmitt (Eds.). Springer, 507–529. https://doi.org/10.1007/978-3-540-69061-0_13Google Scholar
- Peter Knauber, Jesús Bermejo Muñoz, Günter Böckle, Julio Cesar Sampaio do Prado Leite, Frank van der Linden, Linda Northrop, Michael Stark, and David M. Weiss. 2001. Quantifying Product Line Benefits. In Proceedings of the International Workshop on Software Product-Family Engineering. Springer, 155–163. https://doi.org/10.1007/3-540-47833-7_15 Google ScholarDigital Library
- Alexander Knüppel, Stefan Krüger, Thomas Thüm, Richard Bubel, Sebastian Krieter, Eric Bodden, and Ina Schaefer. 2020. Using Abstract Contracts for Verifying Evolving Features and Their Interactions. Springer, 122–148. https://doi.org/10.1007/978-3-030-64354-6_5Google Scholar
- Alexander Knüppel, Thomas Thüm, Carsten Padylla, and Ina Schaefer. 2018. Scalability of Deductive Verification Depends on Method Call Treatment. In Proceedings of the International Symposium On Leveraging Applications of Formal Methods, Verification and Validation. Springer, 159–175. https://doi.org/10.1007/978-3-030-03427-6_15Google ScholarDigital Library
- Derrick G. Kourie and Bruce W. Watson. 2012. The Correctness-by-Construction Approach to Programming. Springer. https://doi.org/10.1007/978-3-642-27919-5 Google ScholarDigital Library
- Elias Kuiter. 2020. Proof Repositories for Correct-by-Construction Software Product Lines. Master’s thesis. University of Magdeburg.Google Scholar
- Gary T. Leavens and Yoonsik Cheon. 2006. Design by Contract with JML. Technical Report. University of Texas at El Paso.Google Scholar
- Jing Liu, Josh Dehlinger, and Robyn Lutz. 2007. Safety Analysis of Software Product Lines using State-Based Modeling. In Proceedings of the International Symposium on Software Reliability Engineering. IEEE, 10–30. https://doi.org/10.1109/issre.2005.36 Google ScholarDigital Library
- Bertrand Meyer. 1992. Applying “Design by Contract”. IEEE Computer 25, 10 (1992), 40–51. https://doi.org/10.1109/2.161279 Google ScholarDigital Library
- Maria Pelevina. 2014. Realization and Extension of Abstract Operation Contracts for Program Logic. Bachelor’s thesis. Technische Universität Darmstadt.Google Scholar
- Klaus Pohl, Günter Böckle, and Frank van der Linden. 2005. Software Product Line Engineering: Foundations, Principles and Techniques. Springer. Google ScholarDigital Library
- Christian Prehofer. 1997. Feature-Oriented Programming: A Fresh Look at Objects. In European Conference on Object-Oriented Programming. Springer, 419–443.Google ScholarCross Ref
- Yannis Smaragdakis and Don Batory. 2002. Mixin Layers: An Object-Oriented Implementation Technique for Refinements and Collaboration-Based Designs. ACM Transactions on Software Engineering and Methodology 11, 2(2002), 215–255. https://doi.org/10.1145/505145.505148 Google ScholarDigital Library
- Dominic Steinhöfel and Reiner Hähnle. 2019. Abstract Execution. In Proceedings of the International Symposium on Formal Methods. Springer, 319–336. https://doi.org/10.1007/978-3-030-30942-8_20Google Scholar
- Thomas Thüm, Sven Apel, Christian Kästner, Ina Schaefer, and Gunter Saake. 2014. A Classification and Survey of Analysis Strategies for Software Product Lines. Comput. Surveys 47, 1 (2014), 1–45. https://doi.org/10.1145/2580950 Google ScholarDigital Library
- Thomas Thüm, Alexander Knüppel, Stefan Krüger, Stefanie Bolle, and Ina Schaefer. 2019. Feature-Oriented Contract Composition. Journal of Systems and Software 152 (2019), 83–107. https://doi.org/10.1016/j.jss.2019.01.044Google ScholarCross Ref
- Thomas Thüm, Ina Schaefer, Sven Apel, and Martin Hentschel. 2012. Family-Based Deductive Verification of Software Product Lines. In Proceedings of the International Conference on Generative Programming: Concepts & Experiences. ACM, 11–20. https://doi.org/10.1145/2371401.2371404 Google ScholarDigital Library
- Thomas Thüm, Ina Schaefer, Martin Kuhlemann, and Sven Apel. 2011. Proof Composition for Deductive Verification of Software Product Lines. In Proceedings of the International Conference on Software Testing, Verification and Validation. IEEE, 270–277. https://doi.org/10.1109/icstw.2011.48 Google ScholarDigital Library
- Claes Wohlin, Per Runeson, Martin Höst, Magnus C. Ohlsson, and Björn Regnell. 2012. Experimentation in Software Engineering. Springer. Google ScholarCross Ref
Index Terms
- Verification Strategies for Feature-Oriented Software Product Lines
Index terms have been assigned to the content through auto-classification.
Recommendations
Partial Proofs to Optimize Deductive Verification of Feature-Oriented Software Product Lines
VaMoS '24: Proceedings of the 18th International Working Conference on Variability Modelling of Software-Intensive SystemsSoftware product lines (SPLs) are a technique to efficiently develop families of software products. Code is implemented in functional features which are composed to individual software variants. SPLs are oftentimes used in safety-critical systems, which ...
Family-based deductive verification of software product lines
GPCE '12: Proceedings of the 11th International Conference on Generative Programming and Component EngineeringA software product line is a set of similar software products that share a common code base. While software product lines can be implemented efficiently using feature-oriented programming, verifying each product individually does not scale, especially ...
Family-based deductive verification of software product lines
GPCE '12A software product line is a set of similar software products that share a common code base. While software product lines can be implemented efficiently using feature-oriented programming, verifying each product individually does not scale, especially ...
Comments