Skip to main content
SpringerLink
Log in

Validated Test Models for Software Product Lines: Featured Finite State Machines

  • Conference paper
  • First Online:
Formal Aspects of Component Software (FACS 2016)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 10231))

Included in the following conference series:

Abstract

Variants of the finite state machine (FSM) model have been extensively used to describe the behaviour of reactive systems. In particular, several model-based testing techniques have been developed to support test case generation and test case executions from FSMs. Most such techniques require several validation properties to hold for the underlying test models. In this paper, we propose an extension of the FSM test model for software product lines (SPLs), named featured finite state machine (FFSM). As the first step towards using FFSMs as test models, we define feature-oriented variants of basic test model validation criteria. We show how the high-level validation properties coincide with the necessary properties on the product FSMs. Moreover, we provide a mechanised tool prototype for checking the feature-oriented properties using satisfiability modulo theory (SMT) solver tools. We investigate the applicability of our approach by applying it to both randomly generated FFSMs as well as those from a realistic case study (the Body Comfort System). The results of our study show that for random FFSMs over 16 independent non-mandatory features, our technique provides substantial efficiency gains for the set of proposed validity checks.

The work of V. Hafemann has been partially supported by the Science Without Borders project number 201694/2015-8.

The work of M.R. Mousavi has been partially supported by the Swedish Research Council award number: 621-2014-5057 and the Swedish Knowledge Foundation project number 20140312.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Notes

  1. 1.

    Due to space limitation proof sketches are provided below; detailed proofs of correctness for these properties is available at http://ceres.hh.se/mediawiki/Vanderson_Hafemann.

  2. 2.

    The experiment package for Eclipse IDE can be found in http://ceres.hh.se/mediawiki/Vanderson_Hafemann.

References

  1. Asirelli, P., ter Beek, M.H., Gnesi, S., Fantechi, A.: Formal description of variability in product families. In: Proceedings of the 15th International Software Product Line Conference (SPLC), pp. 130–139. IEEE (2011)

    Google Scholar 

  2. Batory, D.: Feature models, grammars, and propositional formulas. In: Proceedings of the 9th International Software Product Line Conference (SPLC), pp. 7–20. IEEE (2005)

    Google Scholar 

  3. Benduhn, F., Thüm, T., Lochau, M., Leich, T., Saake, G.: A survey on modeling techniques for formal behavioral verification of software product lines. In: Proceedings of the 9th International Workshop on Variability Modelling of Software-intensive Systems (VaMoS 2015), p. 80. ACM (2015). http://dl.acm.org/citation.cfm?id=2701319

  4. Beohar, H., Mousavi, M.R.: Input-output conformance testing based on featured transition systems. In: Proceedings of the Symposium on Applied Computing (SAC 2014), pp. 1272–1278. ACM (2014). http://dl.acm.org/citation.cfm?id=2554850

  5. Beohar, H., Mousavi, M.R.: Spinal test suites for software product lines. In: Proceedings of the 9th Workshop on Model-Based Testing (MBT 2014), EPTCS, vol. 141, pp. 44–55 (2014). http://dx.doi.org/10.4204/EPTCS.141

  6. Beohar, H., Varshosaz, M., Mousavi, M.R.: Basic behavioral models for software product lines: expressiveness and testing pre-orders. Sci. Comput. Program. 123, 42–60 (2016). http://dx.doi.org/10.1016/j.scico.2015.06.005

    Article  Google Scholar 

  7. Broy, M., Jonsson, B., Katoen, J.-P., Leucker, M., Pretschner, A. (eds.): Model-Based Testing of Reactive Systems. LNCS, vol. 3472. Springer, Heidelberg (2005)

    MATH  Google Scholar 

  8. Classen, A., Cordy, M., Schobbens, P.Y., Heymans, P., Legay, A., Raskin, J.F.: Featured transition systems: foundations for verifying variability-intensive systems and their application to LTL model checking. IEEE Trans. Softw. Eng. 39(8), 1069–1089 (2013)

    Article  Google Scholar 

  9. Classen, A., Heymans, P., Schobbens, P.Y., Legay, A.: Symbolic model checking of software product lines. In: Proceeding of the 33rd International Conference on Software Engineering (ICSE), p. 321. ACM Press (2011)

    Google Scholar 

  10. 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). doi:10.1007/11561347_28

    Chapter  Google Scholar 

  11. Czarnecki, K., Grünbacher, P., Rabiser, R., Schmid, K., Wasowski, A.: Cool features and tough decisions. In: Proceedings of the Sixth International Workshop on Variability Modeling of Software-Intensive Systems (VaMoS), pp. 173–182. ACM Press (2012)

    Google Scholar 

  12. Czarnecki, K., Wasowski, A.: Feature diagrams and logics: there and back again. In: Proceedings of SPLC 2007, pp. 23–34. IEEE (2007)

    Google Scholar 

  13. Devroey, X., Perrouin, G., Papadakis, M., Legay, A., Schobbens, P., Heymans, P.: Featured model-based mutation analysis. In: Proceedings of the 38th International Conference on Software Engineering (ICSE 2016), pp. 655–666. ACM (2016). http://doi.acm.org/10.1145/2884781

  14. Edwards, S.A.: Languages for Digital Embedded Systems. Springer, New York (2000)

    Book  Google Scholar 

  15. Grönninger, H., Krahn, H., Pinkernell, C., Rumpe, B.: Modeling variants of automotive systems using Views. In: Tagungsband Modellierungs-Workshop MBEFF: Modellbasierte Entwicklung von eingebetteten Fahrzeugfunktionen, p. 14. TU Braunschweig (2008)

    Google Scholar 

  16. Hierons, R.M., Bogdanov, K., Bowen, J.P., Cleaveland, R., Derrick, J., Dick, J., Gheorghe, M., Harman, M., Kapoor, K., Krause, P., et al.: Using formal specifications to support testing. ACM Comput. Surv. (CSUR) 41(2), 9 (2009)

    Article  Google Scholar 

  17. Kamischke, J., Lochau, M., Baller, H.: Conditioned model slicing of feature-annotated state machines. In: Proceedings of the 4th International Workshop on Feature-Oriented Software Development (FODS), pp. 9–16. ACM (2012)

    Google Scholar 

  18. Lee, D., Yannakakis, M.: Principles and methods of testing finite state machines - a survey. Proc. IEEE 84(8), 1090–1123 (1996)

    Article  Google Scholar 

  19. Linden, F., Schmif, K., Rommes, E.: Software Product Lines in Action. Springer, New York (2007)

    Book  Google Scholar 

  20. Lity, S., Lachmann, R., Lochau, M., Schaefer, I.: Delta-oriented software product line test models - the body comfort system case study. Technical report (2013)

    Google Scholar 

  21. Liu, J., Dehlinger, J., Lutz, R.: Safety analysis of software product lines using state-based modeling. J. Syst. Softw. 80(11), 1879–1892 (2007)

    Article  Google Scholar 

  22. Lochau, M., Lity, S., Lachmann, R., Schaefer, I., Goltz, U.: Delta-oriented model-based integration testing of large-scale systems. J. Syst. Softw. 91, 63–84 (2014). http://dx.doi.org/10.1016/j.jss.2013.11.1096

    Article  Google Scholar 

  23. Lochau, M., Schaefer, I., Kamischke, J., Lity, S.: Incremental model-based testing of delta-oriented software product lines. In: Brucker, A.D., Julliand, J. (eds.) TAP 2012. LNCS, vol. 7305, pp. 67–82. Springer, Heidelberg (2012). doi:10.1007/978-3-642-30473-6_7

    Chapter  Google Scholar 

  24. Luna, C., Gonzalez, A.: Behavior specification of product lines via feature models and UML statecharts with variabilities. In: Chilean Computer Science Society (SCCC), pp. 9–16. IEEE (2008)

    Google Scholar 

  25. Moura, L., Bjørner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008). doi:10.1007/978-3-540-78800-3_24

    Chapter  Google Scholar 

  26. Oster, S., Wubbeke, A., Engels, G., Schurr, A.: A survey of model-based software product lines testing. In: Zander, J., Schieferdecker, I., Mosterman, P.J. (eds.) Model-Based Testing for Embedded Systems, pp. 338–381. CRC Press, Boca Raton (2012)

    Google Scholar 

  27. Petrenko, A., Bochmann, G.v., Luo, G.: Selecting test sequences for partially specified nondeterministic finite state machines. In: International Workshop on Protocol Test Systems (IWPTS), pp. 95–110. Chapman & Hall (1995)

    Google Scholar 

  28. Schaefer, I., Rabiser, R., Clarke, D., Bettini, L., Benavides, D., Botterweck, G., Pathak, A., Trujillo, S., Villela, K.: Software diversity: state of the art and perspectives. Int. J. Softw. Tools. Technol. Transf. 14(5), 477–495 (2012)

    Article  Google Scholar 

  29. Schobbens, P.Y., Heymans, P., Trigaux, J.C.: Feature diagrams: a survey and a formal semantics. In: Proceedings of the 14th IEEE International Requirements Engineering Conference (RE), pp. 139–148. IEEE (2006)

    Google Scholar 

  30. SEI: A framework for software product line practice (2011). http://www.sei.cmu.edu/productlines/tools/framework/

  31. Simao, A., Petrenko, A.: Fault coverage-driven incremental test generation. Comput. J. 53(9), 1508–1522 (2010)

    Article  Google Scholar 

  32. Thüm, T., Kästner, C., Benduhn, F., Meinicke, J., Saake, G., Leich, T.: Featureide: an extensible framework for feature-oriented software development. Sci. Comput. Program. 79, 70–85 (2014)

    Article  Google Scholar 

  33. Varshosaz, M., Beohar, H., Mousavi, M.R.: Delta-oriented FSM-based testing. In: Butler, M., Conchon, S., Zaïdi, F. (eds.) ICFEM 2015. LNCS, vol. 9407, pp. 366–381. Springer, Cham (2015). doi:10.1007/978-3-319-25423-4_24

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Institute of Mathematics and Computer Sciences - ICMC, University of São Paulo, São Paulo, Brazil

    Vanderson Hafemann Fragal & Adenilso Simao

  2. Centre for Research on Embedded Systems - CERES, Halmstad University, Halmstad, Sweden

    Mohammad Reza Mousavi

Authors
  1. Vanderson Hafemann Fragal
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Adenilso Simao
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Mohammad Reza Mousavi
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Vanderson Hafemann Fragal .

Editor information

Editors and Affiliations

  1. Université Bourgogne Franche-Comté, Besançon, France

    Olga Kouchnarenko

  2. University of Tehran , Tehran, Iran

    Ramtin Khosravi

Rights and permissions

Reprints and permissions

Copyright information

© 2017 Springer International Publishing AG

About this paper

Cite this paper

Hafemann Fragal, V., Simao, A., Mousavi, M.R. (2017). Validated Test Models for Software Product Lines: Featured Finite State Machines. In: Kouchnarenko, O., Khosravi, R. (eds) Formal Aspects of Component Software. FACS 2016. Lecture Notes in Computer Science(), vol 10231. Springer, Cham. https://doi.org/10.1007/978-3-319-57666-4_13

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-57666-4_13

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-57665-7

  • Online ISBN: 978-3-319-57666-4

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation