Thomas Thüm
Ina Schaefer
Sven Apel
ABSTRACT
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 if human effort is required (e.g., as in interactive theorem proving). We present a family-based approach of deductive verification to prove the correctness of a software product line efficiently. We illustrate and evaluate our approach for software product lines written in a feature-oriented dialect of Java and specified using the Java Modeling Language. We show that the theorem prover KeY can be used off-the-shelf for this task, without any modifications. Compared to the individual verification of each product, our approach reduces the verification time needed for our case study by more than 85%.
- S. Agostinho, A. Moreira, and P. Guerreiro. Contracts for Aspect-Oriented Design. In Proc. Workshop Software Engineering Properties of Languages and Aspect Technologies (SPLAT), pages 1:1--1:6, New York, NY, USA, 2008. ACM. Google Scholar
Digital Library
- S. Apel, C. Kästner, A. Größlinger, and C. Lengauer. Type Safety for Feature-Oriented Product Lines. Automated Software Engineering, 17(3): 251--300, 2010. Google ScholarDigital Library
- S. Apel, C. Kästner, and C. Lengauer. Language-Independent and Automated Software Composition: The FeatureHouse Experience. IEEE Trans. Software Engineering (TSE), 2012. To appear. Google ScholarDigital Library
- S. Apel, S. S. Kolesnikov, J. Liebig, C. Kästner, M. Kuhlemann, and T. Leich. Access Control in Feature-Oriented Programming. Science of Computer Programming (SCP), 77(3): 174--187, 2012. Google ScholarDigital Library
- S. Apel, T. Leich, and G. Saake. Aspectual Feature Modules. IEEE Trans. Software Engineering (TSE), 34(2): 162--180, 2008. Google ScholarDigital Library
- S. Apel, H. Speidel, P. Wendler, A. von Rhein, and D. Beyer. Detection of Feature Interactions using Feature-Aware Verification. In Proc. Int'l Conf. Automated Software Engineering (ASE), pages 372--375, Washington, DC, USA, 2011. IEEE. Google ScholarDigital Library
- D. Batory. Feature Models, Grammars, and Propositional Formulas. In Proc. Int'l Software Product Line Conference (SPLC), pages 7--20, Berlin, Heidelberg, New York, London, 2005. Springer. Google ScholarDigital Library
- D. Batory, J. N. Sarvela, and A. Rauschmayer. Scaling Step-Wise Refinement. IEEE Trans. Software Engineering (TSE), 30(6): 355--371, 2004. Google ScholarDigital Library
- B. Beckert, R. Hähnle, and P. Schmitt, editors. Verification of Object-Oriented Software: The KeY Approach. Springer, Berlin, Heidelberg, New York, London, 2007. Google ScholarDigital Library
- D. Bruns, V. Klebanov, and I. Schaefer. Verification of Software Product Lines with Delta-Oriented Slicing. In Proc. Int'l Conf. Formal Verification of Object-Oriented Software (FoVeOOS), pages 61--75, Berlin, Heidelberg, New York, London, 2011. Springer. Google ScholarDigital Library
- L. Burdy, Y. Cheon, D. R. Cok, M. D. Ernst, J. R. Kiniry, G. T. Leavens, K. R. M. Leino, and E. Poll. An Overview of JML Tools and Applications. Int'l J. Software Tools for Technology Transfer (STTT), 7(3): 212--232, 2005. Google ScholarDigital Library
- A. Classen, P. Heymans, P.-Y. Schobbens, and A. Legay. Symbolic Model Checking of Software Product Lines. In Proc. Int'l Conf. Software Engineering (ICSE), pages 321--330, New York, NY, USA, 2011. ACM. Google ScholarDigital Library
- P. Clements and L. Northrop. Software Product Lines: Practices and Patterns. Addison-Wesley, Boston, MA, USA, 2001. Google ScholarDigital Library
- K. Czarnecki and U. W. Eisenecker. Generative Programming: Methods, Tools, and Applications. ACM/Addison-Wesley, New York, NY, USA, 2000. Google ScholarDigital Library
- A. Fantechi and S. Gnesi. Formal Modeling for Product Families Engineering. In Proc. Int'l Software Product Line Conference (SPLC), pages 193--202, Washington, DC, USA, 2008. IEEE. Google ScholarDigital Library
- A. Gruler, M. Leucker, and K. Scheidemann. Modeling and Model Checking Software Product Lines. In Proc. IFIP Int'l Conf. Formal Methods for Open Object-based Distributed Systems (FMOODS), pages 113--131, Berlin, Heidelberg, New York, London, 2008. Springer. Google ScholarDigital Library
- R. Hähnle and I. Schaefer. A Liskov Principle for Delta-oriented Programming. In Proc. Int'l Conf. Formal Verification of Object-Oriented Software (FoVeOOS), pages 190--207, Karlsruhe, Germany, 2011. Technical Report 2011-26, Department of Informatics, Karlsruhe Institute of Technology.Google Scholar
- R. Hirschfeld, M. Perscheid, C. Schubert, and M. Appeltauer. Dynamic Contract Layers. In Proc. ACM Symposium on Applied Computing (SAC), pages 2169--2175, New York, NY, USA, 2010. ACM. Google ScholarDigital Library
- J.-M. Jézéquel and B. Meyer. Design by Contract: The Lessons of Ariane. IEEE Computer, 30(1): 129--130, 1997. Google ScholarDigital Library
- K. C. Kang, S. G. Cohen, J. A. Hess, W. E. Novak, and A. S. Peterson. Feature-Oriented Domain Analysis (FODA) Feasibility Study. Technical Report CMU/SEI-90-TR-21, Software Engineering Institute, 1990.Google ScholarCross Ref
- C. Kästner, S. Apel, T. Thüm, and G. Saake. Type Checking Annotation-Based Product Lines. Trans. Software Engineering and Methodology (TOSEM), 21(3), 2012. To appear. Google ScholarDigital Library
- S. Katz. Aspect Categories and Classes of Temporal Properties. In Trans. Aspect-Oriented Software Development, pages 106--134, Berlin, Heidelberg, New York, London, 2006. Springer. Google ScholarDigital Library
- H. Klaeren, E. Pulvermueller, A. Rashid, and A. Speck. Aspect Composition Applying the Design by Contract Principle. In Proc. Int'l Symposium Generative and Component-Based Software Engineering (GCSE), pages 57--69, Berlin, Heidelberg, New York, London, 2001. Springer. Google ScholarDigital Library
- K. Lauenroth, K. Pohl, and S. Toehning. Model Checking of Domain Artifacts in Product Line Engineering. In Proc. Int'l Conf. Automated Software Engineering (ASE), pages 269--280, Washington, DC, USA, 2009. IEEE. Google ScholarDigital Library
- G. T. Leavens, A. L. Baker, and C. Ruby. Preliminary Design of JML: A Behavioral Interface Specification Language for Java. SIGSOFT Softw. Eng. Notes, 31(3): 1--38, 2006. Google ScholarDigital Library
- D. H. Lorenz and T. Skotiniotis. Extending Design by Contract for Aspect-Oriented Programming. Computing Research Repository (CoRR), abs/cs/0501070, 2005.Google Scholar
- B. Meyer. Applying Design by Contract. IEEE Computer, 25(10): 40--51, 1992. Google ScholarDigital Library
- H. Post and C. Sinz. Configuration Lifting: Software Verification meets Software Configuration. In Proc. Int'l Conf. Automated Software Engineering (ASE), pages 347--350, Washington, DC, USA, 2008. IEEE. Google ScholarDigital Library
- C. Prehofer. Feature-Oriented Programming: A Fresh Look at Objects. In Proc. Europ. Conf. Object-Oriented Programming (ECOOP), pages 419--443, Berlin, Heidelberg, New York, London, 1997. Springer.Google ScholarCross Ref
- W. Scholz, T. Thüm, S. Apel, and C. Lengauer. Automatic Detection of Feature Interactions using the Java Modeling Language: An Experience Report. In Proc. Int'l Workshop Feature-Oriented Software Development (FOSD), pages 7: 1--7:8, New York, NY, USA, 2011. ACM. Google ScholarDigital Library
- R. Tartler, D. Lohmann, J. Sincero, and W. Schröder-Preikschat. Feature Consistency in Compile-Time-Configurable System Software: Facing the Linux 10,000 Feature Problem. In Proc. Europ. Conf. Computer Systems (EuroSys), pages 47--60, New York, NY, USA, 2011. ACM. Google ScholarDigital Library
- T. Thüm. Verification of Software Product Lines Using Contracts. In Magdeburger Informatik Tage (MIT), 2012. To appear.Google Scholar
- T. Thüm, S. Apel, C. Kästner, M. Kuhlemann, I. Schaefer, and G. Saake. Analysis Strategies for Software Product Lines. Technical Report FIN-004-2012, School of Computer Science, University of Magdeburg, Germany, 2012.Google Scholar
- T. Thüm, I. Schaefer, M. Kuhlemann, and S. Apel. Proof Composition for Deductive Verification of Software Product Lines. In Proc. Int'l Workshop Variability-intensive Systems Testing, Validation and Verification (VAST), pages 270--277, Washington, DC, USA, 2011. IEEE. Google ScholarDigital Library
- T. Thüm, I. Schaefer, M. Kuhlemann, S. Apel, and G. Saake. Applying Design by Contract to Feature-Oriented Programming. In Proc. Int'l Conf. Fundamental Approaches to Software Engineering (FASE), pages 255--269, Berlin, Heidelberg, New York, London, 2012. Springer. Google ScholarDigital Library
- J. Zhao and M. C. Rinard. Pipa: A Behavioral Interface Specification Language for AspectJ. In Proc. Int'l Conf. Fundamental Approaches to Software Engineering (FASE), pages 150--165, Berlin, Heidelberg, New York, London, 2003. Springer. Google ScholarDigital Library
Index Terms
- Family-based deductive verification of 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 ...
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 ...
Comments