Abstract
Software product line engineering is a paradigm to develop software applications using platforms and mass customization. Component based approaches play an important role in development of product lines: Components represent features, and different component combinations lead to different products. The number of combinations is exponential in the number of features, which makes the cost of product line model checking high. In this paper, we propose two techniques to reduce the number of component combinations that have to be verified. The first technique is using the static slicing approach to eliminate the features that do not affect the property. The second technique is analyzing the property and extracting sufficient conditions of property satisfaction/violation, to identify products that satisfy or violate the property without model checking. We apply these techniques on a vending machine case study to show the applicability and effectiveness of our approach. The results show that the number of generated states and time of model checking is reduced significantly using the proposed reduction techniques.
This research was in part supported by a grant form IPM. (No. CS1390-4-02).
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Pohl, K., Böckle, G., van der Linden, F.J.: Software Product Line Engineering: Foundations, Principles and Techniques. Springer-Verlag New York, Inc., Secaucus (2005)
Kang, K.C., Cohen, S.G., Hess, J.A., Novak, W.E., Peterson, A.S.: Feature-oriented domain analysis (FODA) feasibility study. Technical report. Carnegie-Mellon University Software Engineering Institute (November 1990)
Kästner, C., Apel, S., Kuhlemann, M.: Granularity in software product lines. In: Proceedings of the 30th International Conference on Software Engineering, ICSE 2008, pp. 311–320. ACM (2008)
Szyperski, C.: Component Software: Beyond Object-Oriented Programming. Addison-Wesley Longman Publishing Co., Inc., Boston (2002)
Kästner, C., Apel, S.: Integrating compositional and annotative approaches for product line engineering. In: Proceedings of the GPCE Workshop on Modularization, Composition and Generative Techniques for Product Line Engineering (McGPLE). University of Passau (October 2008)
Ebert, C., Jones, C.: Embedded software: Facts, figures, and future. Computer 42, 42–52 (2009)
Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. The MIT Press (2000)
Larsen, K.G., Nyman, U., Wąsowski, A.: Modal I/O Automata for Interface and Product Line Theories. In: De Nicola, R. (ed.) ESOP 2007. LNCS, vol. 4421, pp. 64–79. Springer, Heidelberg (2007)
Larsen, K.G., Nyman, U., Wasowski, A.: Modeling software product lines using color-blind transition systems. Int. J. Softw. Tools Technol. Transf. 9(5), 471–487 (2007)
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)
Muschevici, R., Clarke, D., Proenca, J.: Feature Petri nets. In: Second Proceedings of the 14th International Conference on Software Product Lines, pp. 99–106 (2010)
Classen, A., Heymans, P., Schobbens, P.Y., Legay, A., Raskin, J.F.: Model checking lots of systems: efficient verification of temporal properties in software product lines. In: Proceedings of the 32nd ACM/IEEE International Conference on Software Engineering, ICSE 2010, pp. 335–344. ACM (2010)
Sabouri, H., Khosravi, R.: An effective approach for verifying product lines in presence of variability models. In: Second Proceedings of the 14th International Conference on Software Product Lines, pp. 113–120 (2010)
Liu, J., Basu, S., Lutz, R.R.: Compositional model checking of software product lines using variation point obligations. Automated Software Engg. 18, 39–76 (2011)
Bruns, D., Klebanov, V., Schaefer, I.: Verification of Software Product Lines with Delta-Oriented Slicing. In: Beckert, B., Marché, C. (eds.) FoVeOOS 2010. LNCS, vol. 6528, pp. 61–75. Springer, Heidelberg (2011)
Weiser, M.: Program slicing. In: Proceedings of the 5th International Conference on Software Engineering, pp. 439–449 (1981)
Millett, L., Teitelbaum, T.: Issues in slicing Promela and its applications to model checking, protocol understanding, and simulation. Software Tools for Technology Transfer, 343–349 (2000)
Brückner, I., Wehrheim, H.: Slicing an Integrated Formal Method for Verification. In: Lau, K.-K., Banach, R. (eds.) ICFEM 2005. LNCS, vol. 3785, pp. 360–374. Springer, Heidelberg (2005)
Rakow, A.: Slicing Petri Nets with an Application to Workflow Verification. In: Geffert, V., Karhumäki, J., Bertoni, A., Preneel, B., Návrat, P., Bieliková, M. (eds.) SOFSEM 2008. LNCS, vol. 4910, pp. 436–447. Springer, Heidelberg (2008)
Sabouri, H., Sirjani, M.: Actor-based slicing techniques for efficient reduction of Rebeca models. Sci. Comput. Program. 75(10), 811–827 (2010)
Sabouri, H., Sirjani, M.: Slicing-based reductions for Rebeca. Electron. Notes Theor. Comput. Sci. 260, 209–224 (2010)
Dwyer, M.B., Hatcliff, J., Hoosier, M., Ranganath, V., Wallentine, T.: Evaluating the Effectiveness of Slicing for Model Reduction of Concurrent Object-Oriented Programs. In: Hermanns, H., Wallentine, T., Palsberg, J. (eds.) TACAS 2006. LNCS, vol. 3920, pp. 73–89. Springer, Heidelberg (2006)
Sirjani, M., Movaghar, A., Shali, A., de Boer, F.: Modeling and verification of reactive systems using Rebeca. Fundamenta Informaticae 63(4), 385–410 (2004)
Jaghoori, M., Movaghar, A., Sirjani, M.: Modere: The model-checking engine of Rebeca. In: ACM Symposium on Applied Computing - Software Verification Track, pp. 1810–1815 (2006)
Sirjani, M., de Boer, F., Movaghar, A.: Modular verification of a component-based actor language. Journal of Universal Computer Science 11(10), 1695–1717 (2005)
Emerson, E.A.: Temporal and modal logic. In: Handbook of Theoretical Computer Science, pp. 995–1072 (1990)
Batory, D.S.: Feature Models, Grammars, and Propositional Formulas. In: Obbink, H., Pohl, K. (eds.) SPLC 2005. LNCS, vol. 3714, pp. 7–20. Springer, Heidelberg (2005)
Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: engineering an efficient SAT solver. In: Proceedings of the 38th Annual Design Automation Conference, DAC 2001, pp. 530–535. ACM (2001)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Sabouri, H., Khosravi, R. (2012). Reducing the Model Checking Cost of Product Lines Using Static Analysis Techniques. In: Arbab, F., Ölveczky, P.C. (eds) Formal Aspects of Component Software. FACS 2011. Lecture Notes in Computer Science, vol 7253. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-35743-5_18
Download citation
DOI: https://doi.org/10.1007/978-3-642-35743-5_18
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-35742-8
Online ISBN: 978-3-642-35743-5
eBook Packages: Computer ScienceComputer Science (R0)