Thomas Thüm
Jens Meinicke
ABSTRACT
The verification of software product lines is an active research area. A challenge is to efficiently verify similar products without the need to generate and verify them individually. As solution, researchers suggest family-based verification approaches, which either transform compile-time into runtime variability or make verification tools variability-aware. Existing approaches either focus on theorem proving, model checking, or other verification techniques. For the first time, we combine theorem proving and model checking to evaluate their synergies for product-line verification. We provide tool support by connecting five existing tools, namely FeatureIDE and FeatureHouse for product-line development, as well as KeY, JPF, and OpenJML for verification of Java programs. In an experiment, we found the synergy of improved effectiveness and efficiency, especially for product lines with few defects. Further, we experienced that model checking and theorem proving are more efficient and effective if the product line contains more defects.
- J.-R. Abrial. Modeling in Event-B: System and Software Engineering. Cambridge University Press, 1st edition, 2010. Google Scholar
Digital Library
- S. Apel, D. Batory, C. Kästner, and G. Saake. Feature-Oriented Software Product Lines: Concepts and Implementation. Springer, 2013. Google ScholarDigital Library
- S. Apel, C. Kästner, and C. Lengauer. Language-Independent and Automated Software Composition: The FeatureHouse Experience. TSE, 39(1):63--79, 2013. Google ScholarDigital Library
- S. Apel, H. Speidel, P. Wendler, A. von Rhein, and D. Beyer. Detection of Feature Interactions using Feature-Aware Verification. In ASE, pages 372--375. IEEE, 2011. Google ScholarDigital Library
- S. Apel, A. von Rhein, T. Thüm, and C. Kästner. Feature-Interaction Detection Based on Feature-Based Specifications. ComNet, 57(12):2399--2409, 2013. Google ScholarDigital Library
- S. Apel, A. von Rhein, P. Wendler, A. Größlinger, and D. Beyer. Strategies for Product-Line Verification: Case Studies and Experiments. In ICSE, pages 482--491. IEEE, 2013. Google ScholarDigital Library
- L. Aversano, M. D. Penta, and I. D. Baxter. Handling Preprocessor-Conditioned Declarations. In SCAM, pages 83--92. IEEE, 2002. Google ScholarDigital Library
- M. Barnett, M. Fähndrich, K. R. M. Leino, P. Müller, W. Schulte, and H. Venter. Specification and Verification: The Spec# Experience. Comm. ACM, 54:81--91, 2011. Google ScholarDigital Library
- D. Batory. Feature Models, Grammars, and Propositional Formulas. In SPLC, pages 7--20. Springer, 2005. Google ScholarDigital Library
- D. Batory, J. N. Sarvela, and A. Rauschmayer. Scaling Step-Wise Refinement. TSE, 30(6):355--371, 2004. Google ScholarDigital Library
- B. Beckert, R. Hähnle, and P. Schmitt. Verification of Object-Oriented Software: The KeY Approach. Springer, 2007. Google ScholarDigital Library
- F. Benduhn. Contract-Aware Feature Composition. Bachelor's thesis, University of Magdeburg, Germany, 2012.Google Scholar
- E. Bodden, T. Tolêdo, M. Ribeiro, C. Brabrand, P. Borba, and M. Mezini. SPLLIFT: Statically Analyzing Software Product Lines in Minutes Instead of Years. In PLDI, pages 355--364. ACM, 2013. Google ScholarDigital Library
- C. Brabrand, M. Ribeiro, T. Tolêdo, J. Winther, and P. Borba. Intraprocedural Dataflow Analysis for Software Product Lines. TAOSD, 10:73--108, 2013. Google ScholarDigital Library
- D. Bruns, V. Klebanov, and I. Schaefer. Verification of Software Product Lines with Delta-Oriented Slicing. In FoVeOOS, pages 61--75. Springer, 2011. Google ScholarDigital Library
- L. Burdy, Y. Cheon, D. R. Cok, M. D. Ernst, J. Kiniry, G. T. Leavens, K. R. M. Leino, and E. Poll. An Overview of JML Tools and Applications. STTT, 7(3):212--232, 2005. Google ScholarDigital Library
- E. M. Clarke, O. Grumberg, and D. A. Peled. Model Checking. MIT Press, 1999. Google ScholarDigital Library
- A. Classen, P. Heymans, P.-Y. Schobbens, and A. Legay. Symbolic Model Checking of Software Product Lines. In ICSE, pages 321--330. ACM, 2011. Google ScholarDigital Library
- D. R. Cok. OpenJML: JML for Java 7 by Extending OpenJDK. In NFM, pages 472--479. Springer, 2011. Google ScholarDigital Library
- F. Damiani, O. Owe, J. Dovland, I. Schaefer, E. B. Johnsen, and I. C. Yu. A Transformational Proof System for Delta-Oriented Programming. In FMSPLE, pages 53--60. ACM, 2012. Google ScholarDigital Library
- F. Damiani and I. Schaefer. Family-Based Analysis of Type Safety for Delta-Oriented Software Product Lines. In ISOLA, pages 193--207. Springer, 2012. Google ScholarDigital Library
- P. Dybjer, Q. Haiyan, and M. Takeyama. Verifying Haskell Programs by Combining Testing, Model Checking and Interactive Theorem Proving. IST, 46(15):1011--1025, 2004.Google Scholar
- D. Fischbein, S. Uchitel, and V. Braberman. A Foundation for Behavioural Conformance in Software Product Line Architectures. In ROSATEA, pages 39--48. ACM, 2006. Google ScholarDigital Library
- A. Gondal, M. Poppleton, and M. Butler. Composing Event-B Specifications: Case-Study Experience. In SC, pages 100--115. Springer, 2011. Google ScholarDigital Library
- A. Gruler, M. Leucker, and K. Scheidemann. Modeling and Model Checking Software Product Lines. In FMOODS, pages 113--131. Springer, 2008. Google ScholarDigital Library
- R. Hähnle and I. Schaefer. A Liskov Principle for Delta-Oriented Programming. In ISOLA, pages 32--46. Springer, 2012. Google ScholarDigital Library
- J. Y. Halpern and M. Y. Vardi. Model Checking vs. Theorem Proving: A Manifesto. In V. Lifschitz, editor, Artificial Intelligence and Mathematical Theory of Computation, pages 151--176. Academic Press Professional, Inc., 1991. Google ScholarDigital Library
- J. Hatcliff, G. T. Leavens, K. R. M. Leino, P. Müller, and M. Parkinson. Behavioral Interface Specification Languages. CSUR, 44(3):16:1--16:58, 2012. Google ScholarDigital Library
- K. Havelund and T. Pressburger. Model Checking Java Programs using Java PathFinder. STTT, 2(4):366--381, 2000.Google ScholarCross Ref
- M. Ismail, O. Hasan, T. Ebi, M. Shafique, and J. Henkel. Formal Verification of Distributed Dynamic Thermal Management. In ICCAD, pages 248--255. IEEE, 2013. Google ScholarDigital Library
- Y. Jia and M. Harman. An Analysis and Survey of the Development of Mutation Testing. TSE, 37(5):649--678, 2011. Google ScholarDigital Library
- C. Kästner, S. Apel, T. Thüm, and G. Saake. Type Checking Annotation-Based Product Lines. TOSEM, 21(3):14:1--14:39, 2012. Google ScholarDigital Library
- C. Kästner, A. von Rhein, S. Erdweg, J. Pusch, S. Apel, T. Rendel, and K. Ostermann. Toward Variability-Aware Testing. In FOSD, pages 1--8. ACM, 2012. Google ScholarDigital Library
- S. Kolesnikov, A. von Rhein, C. Hunsen, and S. Apel. A Comparison of Product-based, Feature-based, and Family-based Type Checking. In GPCE, pages 115--124. ACM, 2013. Google ScholarDigital Library
- J. Liebig, A. von Rhein, C. Kästner, S. Apel, J. Dörre, and C. Lengauer. Scalable Analysis of Variable Software. In ESECFSE, pages 81--91. ACM, 2013. Google ScholarDigital Library
- J. Meinicke. JML-Based Verification for Feature-Oriented Programming. Bachelor's thesis, University of Magdeburg, Germany, 2013.Google Scholar
- J. Meinicke, T. Thüm, R. Schöter, F. Benduhn, and G. Saake. An Overview on Analysis Tools for Software Product Lines. In SPLat. ACM, 2014. To appear. Google ScholarDigital Library
- B. Meyer. Object-Oriented Software Construction. Prentice-Hall, Inc., 1st edition, 1988. Google ScholarDigital Library
- F. Nielson, H. R. Nielson, and C. Hankin. Principles of Program Analysis. Springer, 2010. Google ScholarDigital Library
- S. Owre, S. P. Rajan, J. M. Rushby, N. Shankar, and M. K. Srivas. PVS: Combining Specification, Proof Checking, and Model Checking. In R. Alur and T. A. Henzinger, editors, CAV, pages 411--414. Springer, 1996. Google ScholarDigital Library
- B. C. Pierce. Types and Programming Languages. MIT Press, 2002. Google ScholarDigital Library
- K. Pohl, G. Böckle, and F. J. van der Linden. Software Product Line Engineering: Foundations, Principles and Techniques. Springer, 2005. Google ScholarDigital Library
- M. Poppleton. Towards Feature-Oriented Specification and Development with Event-B. In REFSQ, pages 367--381. Springer, 2007. Google ScholarDigital Library
- H. Post and C. Sinz. Configuration Lifting: Software Verification meets Software Configuration. In ASE, pages 347--350. IEEE, 2008. Google ScholarDigital Library
- C. Prehofer. Feature-Oriented Programming: A Fresh Look at Objects. In ECOOP, pages 419--443. Springer, 1997.Google Scholar
- Robby, E. Rodríguez, M. B. Dwyer, and J. Hatcliff. Checking JML Specifications using an Extensible Software Model Checking Framework. STTT, 8(3):280--299, 2006. Google ScholarDigital Library
- J. Rubin and M. Chechik. A Framework for Managing Cloned Product Variants. In ICSE, pages 1233--1236. IEEE, 2013. Google ScholarDigital Library
- W. Scholz, T. Thüm, S. Apel, and C. Lengauer. Automatic Detection of Feature Interactions using the Java Modeling Language: An Experience Report. In FOSD, pages 7:1--7:8. ACM, 2011. Google ScholarDigital Library
- R. Schröter, N. Siegmund, and T. Thüm. Towards Modular Analysis of Multi Product Lines. In MultiPLE, pages 96--99. ACM, 2013. Google ScholarDigital Library
- J. Schumann. Automated Theorem Proving in Software Engineering. Springer, 2001. Google ScholarDigital Library
- J. Sorge, M. Poppleton, and M. Butler. A Basis for Feature-Oriented Modelling in Event-B. In ABZ, pages 409--409. Springer, 2010. Google ScholarDigital Library
- O. Strichman and B. Godlin. Verified Software: Theories, Tools, Experiments. In B. Meyer and J. Woodcock, editors, Regression Verification - A Practical Way to Verify Programs, pages 496--501. Springer, 2008. Google ScholarDigital Library
- P. Tarr, H. Ossher, W. Harrison, and S. M. Sutton, Jr. N Degrees of Separation: Multi-Dimensional Separation of Concerns. In ICSE, pages 107--119. ACM, 1999. Google ScholarDigital Library
- S. Thaker, D. Batory, D. Kitchin, and W. Cook. Safe Composition of Product Lines. In GPCE, pages 95--104. ACM, 2007. Google ScholarDigital Library
- T. Thüm, S. Apel, C. Kästner, I. Schaefer, and G. Saake. A Classification and Survey of Analysis Strategies for Software Product Lines. CSUR, 47(1):6:1--6:45, 2014. Google ScholarDigital Library
- T. Thüm, S. Apel, A. Zelend, R. Schröter, and B. Möller. Subclack: Feature-Oriented Programming with Behavioral Feature Interfaces. In MASPEGHI, pages 1--8. ACM, 2013. Google ScholarDigital Library
- T. Thüm, C. Kästner, F. Benduhn, J. Meinicke, G. Saake, and T. Leich. FeatureIDE: An Extensible Framework for Feature-Oriented Software Development. SCP, 79(0):70--85, 2014. Google ScholarDigital Library
- T. Thüm, I. Schaefer, S. Apel, and M. Hentschel. Family-Based Deductive Verification of Software Product Lines. In GPCE, pages 11--20. ACM, 2012. Google ScholarDigital Library
- T. Thüm, I. Schaefer, M. Kuhlemann, and S. Apel. Proof Composition for Deductive Verification of Software Product Lines. In VAST, pages 270--277. IEEE, 2011. Google ScholarDigital Library
- T. Thüm, I. Schaefer, M. Kuhlemann, S. Apel, and G. Saake. Applying Design by Contract to Feature-Oriented Programming. In FASE, pages 255--269. Springer, 2012. Google ScholarDigital Library
- D. M. Weiss. The Product Line Hall of Fame. In SPLC, page 395. IEEE, 2008. Google ScholarDigital Library
- Y. Xue, Z. Xing, and S. Jarzabek. Feature Location in a Collection of Product Variants. In WCRE, pages 145--154. IEEE, 2012. Google ScholarDigital Library
Index Terms
- Potential synergies of theorem proving and model checking for software product lines
Recommendations
A Classification and Survey of Analysis Strategies for Software Product Lines
Software-product-line engineering has gained considerable momentum in recent years, both in industry and in academia. A software product line is a family of software products that share a common set of features. Software product lines challenge ...
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 ...
Combining Theorem Proving with Model Checking through Predicate Abstraction
This article presents a procedure for proving invariants of infinite-state reactive systems using a combination of two formal verification techniques: theorem proving and model checking. This method uses term rewriting on the definition of the target ...
Comments