Abstract
Software product line engineering allows large software systems to be developed and adapted for varying customer needs. The products of a software product line can be described by means of a hierarchical variability model specifying the commonalities and variabilities between the artifacts of the individual products. The number of products generated by a hierarchical model is exponential in its size, which poses a serious challenge to software product line analysis and verification. For an analysis technique to scale, the effort has to be linear in the size of the model rather than linear in the number of products it generates. Hence, efficient product line verification is only possible if compositional verification techniques are applied that allow the analysis of products to be relativized on the properties of their variation points. In this paper, we propose simple hierarchical variability models (SHVM) with explicit variation points as a novel way to describe a set of products consisting of sets of methods. SHVMs provide a trade–off between expressiveness and a clean and simple model suitable for compositional verification. We generalize a previously developed compositional technique and tool set for the automatic verification of control–flow based temporal safety properties to product lines defined by SHVMs, and prove soundness of the generalization. The desired property relativization is achieved by introducing variation point specifications. We evaluate the proposed technique on a number of test cases.
This work has been partially supported by the Deutsche Forschungsgemeinschaft (DFG) and the EU project FP7-231620 HATS.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Apel, S., Janda, F., Trujillo, S., Kästner, C.: Model Superimposition in Software Product Lines. In: Paige, R.F. (ed.) ICMT 2009. LNCS, vol. 5563, pp. 4–19. Springer, Heidelberg (2009)
Batory, D., Sarvela, J., Rauschmayer, A.: Scaling Step-Wise Refinement. IEEE Trans. Software Eng. 30(6), 355–371 (2004)
Besson, F., Jensen, T., Le Métayer, D., Thorn, T.: Model checking security properties of control flow graphs. J. of Computer Security 9(3), 217–250 (2001)
Blundell, C., Fisler, K., Krishnamurthi, S., van Hentenryck, P.: Parameterized Interfaces for Open System Verification of Product Lines. In: Automated Software Engineering (ASE 2004), pp. 258–267. IEEE, Los Alamitos (2004)
Classen, A., Heymans, P., Schobbens, P., Legay, A., Raskin, J.: Model Checking Lots of Systems: Efficient Verification of Temporal Properties in Software Product Lines. In: International Conference on Software Engineering (ICSE 2010), pp. 335–344. IEEE, Los Alamitos (2010)
Czarnecki, K., Antkiewicz, M.: Mapping Features to Models: A Template Approach Based on Superimposed Variants. In: Glück, R., Lowry, M. (eds.) GPCE 2005. LNCS, vol. 3676, pp. 422–437. Springer, Heidelberg (2005)
Czarnecki, K., Eisenecker, U.W.: Generative Programming: Methods, Tools, and Applications. Addison-Wesley, Reading (2000)
Fantechi, A., Gnesi, S.: Formal Modeling for Product Families Engineering. In: Software Product Line Conference (SPLC 2008), pp. 193–202. IEEE, Los Alamitos (2008)
Gomaa, H.: Designing Software Product Lines with UML. Addison Wesley, Reading (2004)
Gruler, A., Leucker, M., Scheidemann, K.: Modeling and model checking software product lines. In: Barthe, G., de Boer, F.S. (eds.) FMOODS 2008. LNCS, vol. 5051, pp. 113–131. Springer, Heidelberg (2008)
Grumberg, O., Long, D.: Model checking and modular verification. ACM Transactions on Programming Languages and Systems 16(3), 843–871 (1994)
Gurov, D., Huisman, M.: Reducing behavioural to structural properties of programs with procedures. In: Jones, N.D., Müller-Olm, M. (eds.) VMCAI 2009. LNCS, vol. 5403, pp. 136–150. Springer, Heidelberg (2009)
Gurov, D., Huisman, M., Sprenger, C.: Compositional verification of sequential programs with procedures. Information and Computation 206(7), 840–868 (2008)
Haugen, Ø., Møller-Pedersen, B., Oldevik, J., Olsen, G., Svendsen, A.: Adding Standardized Variability to Domain Specific Languages. In: Software Product Line Conference (SPLC 2008), pp. 139–148. IEEE, Los Alamitos (2008)
Huisman, M., Gurov, D.: CVPP: A tool set for compositional verification of control–flow safety properties. In: Beckert, B., Marché, C. (eds.) FoVeOOS 2010. LNCS, vol. 6528, pp. 107–121. Springer, Heidelberg (2011)
Kang, K., Lee, J., Donohoe, P.: Feature-Oriented Project Line Engineering. IEEE Software 19(4) (2002)
Kozen, D.: Results on the propositional μ-calculus. Theoretical Computer Science 27, 333–354 (1983)
Lauenroth, K., Pohl, K., Toehning, S.: Model checking of domain artifacts in product line engineering. In: Automated Software Engineering (ASE 2009), pp. 269–280. IEEE, Los Alamitos (2009)
Leavens, G., Poll, E., Clifton, C., Cheon, Y., Ruby, C., Cok, D., Müller, P., Kiniry, J., Chalin, P.: JML Reference Manual, Department of Computer Science, Iowa State University (February 2007), http://www.jmlspecs.org
Liu, J., Basu, S., Lutz, R.R.: Compositional model checking of software product lines using variation point obligations. Autom. Softw. Eng. 18(1), 39–76 (2011)
Noda, N., Kishi, T.: Aspect-Oriented Modeling for Variability Management. In: Software Product Line Conference (SPLC 2008), pp. 213–222. IEEE, Los Alamitos (2008)
Pérez, J., Díaz, J., Soria, C.C., Garbajosa, J.: Plastic Partial Components: A solution to support variability in architectural components. In: WICSA/ECSA, pp. 221–230 (2009)
Pohl, K., Böckle, G., van der Linden, F.: Software Product Line Engineering - Foundations, Principles, and Techniques. Springer, Heidelberg (2005)
Requirement Elicitation, Deliverable 5.1 of project FP7-231620 (HATS) (August 2009), http://www.hats-project.eu
Schwoon, S.: Model-Checking Pushdown Systems. PhD thesis, Technische Universität München (2002)
Soleimanifard, S., Gurov, D., Huisman, M.: Procedure–modular verification of control flow safety properties. In: Workshop on Formal Techniques for Java Programs, FTfJP 2010 (2010)
Soleimanifard, S., Gurov, D., Huisman, M.: Promover: Modular verification of temporal safety properties. In: Software Engineering and Formal Methods, SEFM 2011 (to appear,2011)
Stirling, C.: Modal and Temporal Logics of Processes. Springer, Heidelberg (2001)
van Ommering, R.: Software reuse in product populations. IEEE Trans. Software Eng. 31(7), 537–550 (2005)
Völter, M., Groher, I.: Product Line Implementation using Aspect-Oriented and Model-Driven Software Development. In: Software Product Line Conference (SPLC 2007), pp. 233–242. IEEE, Los Alamitos (2007)
Ziadi, T., Hëlouët, L., Jézéquel, J.-M.: Towards a UML Profile for Software Product Lines. In: van der Linden, F.J. (ed.) PFE 2003. LNCS, vol. 3014, pp. 129–139. Springer, Heidelberg (2004)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Schaefer, I., Gurov, D., Soleimanifard, S. (2011). Compositional Algorithmic Verification of Software Product Lines. In: Aichernig, B.K., de Boer, F.S., Bonsangue, M.M. (eds) Formal Methods for Components and Objects. FMCO 2010. Lecture Notes in Computer Science, vol 6957. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-25271-6_10
Download citation
DOI: https://doi.org/10.1007/978-3-642-25271-6_10
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-25270-9
Online ISBN: 978-3-642-25271-6
eBook Packages: Computer ScienceComputer Science (R0)