research-article

Open access

Verification Strategies for Feature-Oriented Software Product Lines

Authors:

Alexander Knüppel,

Ina SchaeferAuthors Info & Claims

VaMoS '22: Proceedings of the 16th International Working Conference on Variability Modelling of Software-Intensive Systems

Article No.: 12, Pages 1 - 9

https://doi.org/10.1145/3510466.3511272

Published: 23 February 2022 Publication History

All formats PDF

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.

References

[1]

Wolfgang Ahrendt, Bernhard Beckert, Richard Bubel, Reiner Hähnle, Peter H. Schmitt, and Mattias Ulbrich (Eds.). 2016. Deductive Software Verification – The KeY Book. Springer.

[2]

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

Digital Library

[3]

Sven Apel, Don Batory, Christian Kästner, and Gunter Saake. 2013. Feature-Oriented Software Product Lines. Springer.

Digital Library

[4]

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

Digital Library

[5]

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

Digital Library

[6]

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.

Digital Library

[7]

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

Digital Library

[8]

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_8

[9]

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_9

[10]

Paul Clements and Linda Northrop. 2002. Software Product Lines: Practices and Patterns. Addison-Wesley.

Digital Library

[11]

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

Digital Library

[12]

Ramez Elmasri and Shamkant Navathe. 2010. Fundamentals of Database Systems. Addison-Wesley.

Digital Library

[13]

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

Digital Library

[14]

David Harel. 1979. First-Order Dynamic Logic. Springer. https://doi.org/10.1007/3-540-09237-4

Digital Library

[15]

Marlen Herter-Bernier. 2021. Verifikation Evolvierender Softwareproduktlinien mittels Uninterpretierter Prädikate. Master’s thesis. Technische Universität Braunschweig.

[16]

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

Digital Library

[17]

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

Digital Library

[18]

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.

[19]

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_13

[20]

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

Digital Library

[21]

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_5

[22]

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_15

Digital Library

[23]

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

Digital Library

[24]

Elias Kuiter. 2020. Proof Repositories for Correct-by-Construction Software Product Lines. Master’s thesis. University of Magdeburg.

[25]

Gary T. Leavens and Yoonsik Cheon. 2006. Design by Contract with JML. Technical Report. University of Texas at El Paso.

[26]

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

Digital Library

[27]

Bertrand Meyer. 1992. Applying “Design by Contract”. IEEE Computer 25, 10 (1992), 40–51. https://doi.org/10.1109/2.161279

Digital Library

[28]

Maria Pelevina. 2014. Realization and Extension of Abstract Operation Contracts for Program Logic. Bachelor’s thesis. Technische Universität Darmstadt.

[29]

Klaus Pohl, Günter Böckle, and Frank van der Linden. 2005. Software Product Line Engineering: Foundations, Principles and Techniques. Springer.

Digital Library

[30]

Christian Prehofer. 1997. Feature-Oriented Programming: A Fresh Look at Objects. In European Conference on Object-Oriented Programming. Springer, 419–443.

[31]

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

Digital Library

[32]

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_20

[33]

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

Digital Library

[34]

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.044

[35]

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

Digital Library

[36]

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

Digital Library

[37]

Claes Wohlin, Per Runeson, Martin Höst, Magnus C. Ohlsson, and Björn Regnell. 2012. Experimentation in Software Engineering. Springer.

Cited By

Khosravi RKhamespanah EGhassemi FSirjani M(2024)Actors Upgraded for Variability, Adaptability, and DeterminismActive Object Languages: Current Research Trends10.1007/978-3-031-51060-1_9(226-260)Online publication date: 29-Jan-2024
https://doi.org/10.1007/978-3-031-51060-1_9
Kamburjan EScaletta MRollshausen N(2023)Deductive verification of active objects with Crowbar▪Science of Computer Programming10.1016/j.scico.2023.102928226:COnline publication date: 1-Mar-2023
https://dl.acm.org/doi/10.1016/j.scico.2023.102928

Index Terms

Verification Strategies for Feature-Oriented Software Product Lines
1. Software and its engineering
  1. Software creation and management
    1. Software verification and validation
      1. Formal software verification
  2. Software organization and properties
    1. Software functional properties
      1. Formal methods
2. Theory of computation
  1. Semantics and reasoning
    1. Program reasoning
      1. Program verification

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 Systems

Software 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 Engineering

A 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 '12

A 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

Information & Contributors

Information

Published In

cover image ACM Other conferences

VaMoS '22: Proceedings of the 16th International Working Conference on Variability Modelling of Software-Intensive Systems

February 2022

114 pages

ISBN:9781450396042

DOI:10.1145/3510466

Copyright © 2022 Owner/Author.

This work is licensed under a Creative Commons Attribution International 4.0 License.

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 23 February 2022

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article
Research
Refereed limited

Conference

VaMoS '22

VaMoS '22: 16th International Working Conference on Variability Modelling of Software-Intensive Systems

February 23 - 25, 2022

Florence, Italy

Acceptance Rates

Overall Acceptance Rate 66 of 147 submissions, 45%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

2
Total Citations
View Citations
382
Total Downloads

Downloads (Last 12 months)158
Downloads (Last 6 weeks)19

Reflects downloads up to 14 Sep 2024

Other Metrics

View Author Metrics

Citations

Cited By

Khosravi RKhamespanah EGhassemi FSirjani M(2024)Actors Upgraded for Variability, Adaptability, and DeterminismActive Object Languages: Current Research Trends10.1007/978-3-031-51060-1_9(226-260)Online publication date: 29-Jan-2024
https://doi.org/10.1007/978-3-031-51060-1_9
Kamburjan EScaletta MRollshausen N(2023)Deductive verification of active objects with Crowbar▪Science of Computer Programming10.1016/j.scico.2023.102928226:COnline publication date: 1-Mar-2023
https://dl.acm.org/doi/10.1016/j.scico.2023.102928

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

HTML Format

View this article in HTML Format.

Get Access

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

Media

Figures

Other

Tables

View Table of Contents