Skip to main content
SpringerLink
Log in

Detecting Feature Interactions in FORML Models

  • Chapter
  • First Online:
From Software Engineering to Formal Methods and Tools, and Back

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 11865))

  • 1165 Accesses

Abstract

Requirement engineers must know how features (units of functionality) interact, in order to resolve undesired interactions. Model checking has been proposed as an effective method for detecting feature interactions. We propose a method for (1) modelling features as distinct modules (explicating intended interactions with other features), (2) composing feature modules into a system model that preserves intended interactions, (3) translating this rich model into the input language of a model checker, and (4) automatically generating correctness properties whose violations reveal unintended feature interactions.

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.

    An overriding transition implicitly has the same enabling conditions as the transition it override, whereas a prioritized transition has unique enabling conditions.

  2. 2.

    Although bounds may need to be specified, this is for the purpose of analysis alone; the bounds do not reflect the specified size of the model.

  3. 3.

    The order of the branch conditions in an SMV case statement matters. The branch conditions are considered in sequential order. Thus, branches should be ordered such than no branch condition is a subcase of a subsequent branch condition. In the next(ws.E_v) assignment in Fig. 5, where the branch conditions are the possible subsets of executing transitions, the branches are listed in decreasing size of the set of executing transitions.

  4. 4.

    Note that current and next values in the current world state are previous and current values in the next world state AX().

References

  1. Alur, R., Courcoubetis, C., Dill, D.: Model checking for real-time systems. In: Proceedings of the 5th Annual Symposium on Logic in Computer Science, pp. 414–425 (1990)

    Google Scholar 

  2. Apel, S., Kästner, C., Lengauer, C.: FeatureHouse: language-independent, automated software composition. In: International Conference on Software Engineering, pp. 221–231 (2009)

    Google Scholar 

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

    Google Scholar 

  4. Asirelli, P., ter Beek, M.H., Fantechi, A., Gnesi, S.: A logical framework to deal with variability. In: Méry, D., Merz, S. (eds.) IFM 2010. LNCS, vol. 6396, pp. 43–58. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-16265-7_5

    Chapter  Google Scholar 

  5. Basile, D., Di Giandomenico, F., Gnesi, S.: FMCAT: supporting dynamic service-based product lines. In: International Systems and Software Product Line Conference, SPLC 2017, vol. B, pp. 3–8 (2017)

    Google Scholar 

  6. ter Beek, M.H., Fantechi, A., Gnesi, S., Mazzanti, F.: A state/event-based model-checking approach for the analysis of abstract system properties. Sci. Comput. Program. 76(2), 119–135 (2011)

    Article  Google Scholar 

  7. ter Beek, M.H., Gnesi, S., Montangero, C., Semini, L.: Detecting policy conflicts by model checking UML state machines. In: International Conference on Feature Interactions (2009)

    Google Scholar 

  8. ter Beek, M.H., Mazzanti, F., Sulova, A.: VMC: a tool for product variability analysis. In: Giannakopoulou, D., Méry, D. (eds.) FM 2012. LNCS, vol. 7436, pp. 450–454. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-32759-9_36

    Chapter  Google Scholar 

  9. Beidu, S., Atlee, J.M., Shaker, P.: Incremental and commutative composition of state-machine models of features. In: International Workshop on Modeling in Software Engineering (MiSE 2015), (ICSE Workshop), pp. 13–18, May 2015

    Google Scholar 

  10. Bowen, T.F., Dworack, F.S., Chow, C.H., Griffeth, N., Herman, G.E., Lin, Y.-J.: The feature interaction problem in telecommunication systems. In: International Conference on Software Engineering for Telecommunication Switching Systems, pp. 59–62 (1989)

    Google Scholar 

  11. Cimatti, A., Clarke, E., Giunchiglia, F., Roveri, M.: NUSMV: a new symbolic model checker. Int. J. Softw. Tools Technol. Transf. 2(4), 410–425 (2000)

    Article  Google Scholar 

  12. Esmaeilsabzali, S., Day, N.A., Atlee, J.M., Niu, J.: Deconstructing the semantics of big-step modelling languages. Requirements Eng. J. 15(2), 235–265 (2010)

    Article  Google Scholar 

  13. Faghih, F.: Model translations among big-step modeling languages. In: International Conference on Software Engineering, Doc. Sym., pp. 1555–1558 (2012)

    Google Scholar 

  14. Fantechi, A., Gnesi, S.: Formal modeling for product families engineering. In: International Software Product Line Conference, pp. 193–202 (2008)

    Google Scholar 

  15. Fantechi, A., Gnesi, S.: A behavioural model for product families. In: European Software Engineering Conference/Foundations of Software Engineering: Companion Papers, pp. 521–524 (2007)

    Google Scholar 

  16. Hay, J.D., Atlee, J.M.: Composing features and resolving interactions. In: Foundations of Software Engineering, pp. 110–119 (2000)

    Google Scholar 

  17. Jackson, D., Damon, C.A.: Elements of style: analyzing a software design feature with a counterexample detector. IEEE Trans. Softw. Eng. 22(7), 484–495 (1996)

    Article  Google Scholar 

  18. Kang, K.C., Cohen, S.G., Hess, J.A., Novak, W.E., Peterson, A.S.: Feature-Oriented Domain Analysis (FODA) Feasibility Study. Technical report CMU/SEI-90-TR-21, Carnegie-Mellon University Software Engineering Institute (1990)

    Google Scholar 

  19. Nhlabatsi, A., Laney, R., Nuseibeh, B.: Feature interaction as a context sharing problem. In: International Conference on Feature Interaction, pp. 133–148 (2009)

    Google Scholar 

  20. Rumbaugh, J., Jacobson, I., Booch, G.: Unified Modeling Language Reference Manual, The, 2nd edn. Pearson Higher Education, Boston (2004)

    Google Scholar 

  21. Shaker, P.: A feature-oriented modelling language and a feature-interaction taxonomy for product-line requirements. Ph.D. thesis, University of Waterloo (2013)

    Google Scholar 

  22. Shaker, P., Atlee, J.M., Wang, S.: A feature-oriented requirements modelling language. In: International Requirements Engineering Conference, pp. 151–160 (2012)

    Google Scholar 

  23. Weiss, D., Lai, R.: Software Product Line Engineering: A Family Based Development Process. Addison Wesley, Boston (1999)

    Google Scholar 

  24. Zave, P.: Requirements for evolving systems: a telecommunications perspective. In: International Symposium on Requirements Engineering, pp. 2–9 (2001)

    Google Scholar 

Download references

Acknowledgement

We are grateful to Stefania Gnesi in whose honour this Festschrift is held, not only for her pioneering work on modelling and analysis of behaviour models of software product lines (which inspired our work in this area), but also for her service and leadership in the formal methods and SPL communities, for many thought-provoking technical discussions, and for her friendship.

Author information

Authors and Affiliations

  1. University of Waterloo, Waterloo, ON, N2L 3G1, Canada

    Sandy Beidu & Joanne M. Atlee

Authors
  1. Sandy Beidu
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Joanne M. Atlee
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Sandy Beidu .

Editor information

Editors and Affiliations

  1. Consiglio Nazionale delle Ricerche, Pisa, Italy

    Maurice H. ter Beek

  2. Università degli Studi di Firenze, Florence, Italy

    Alessandro Fantechi

  3. Università di Pisa, Pisa, Italy

    Laura Semini

Rights and permissions

Reprints and permissions

Copyright information

© 2019 Springer Nature Switzerland AG

About this chapter

Check for updates. Verify currency and authenticity via CrossMark

Cite this chapter

Beidu, S., Atlee, J.M. (2019). Detecting Feature Interactions in FORML Models. In: ter Beek, M., Fantechi, A., Semini, L. (eds) From Software Engineering to Formal Methods and Tools, and Back. Lecture Notes in Computer Science(), vol 11865. Springer, Cham. https://doi.org/10.1007/978-3-030-30985-5_14

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-30985-5_14

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-30984-8

  • Online ISBN: 978-3-030-30985-5

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation