Detecting Feature Interactions: How Many Components Do We Need?

  • Muffy Calder
  • Alice Miller
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2975)


Features are a structuring mechanism for additional functionality, usually in response to changing requirements. When several features are invoked at the same time, by the same, or different components, the features may not interwork. This is known as feature interaction. We employ a property-based approach to feature interaction detection: this involves checking the validity (or not) of a temporal property against a given system model. We use the logic LTL for temporal properties and the model-checker Spin to prove properties.

To gain any real insight into feature interactions, it is important to be able to infer properties for networks of any size, regardless of the underlying communication structure. We present an inference mechanism based on abstraction. The key idea is to model-check a system consisting of a constant number (m) of components together with an abstract component representing any number of other (possibly featured) components. The approach is applied to two systems with communication which is peer to peer and client server. We outline a proof of correctness in both cases.

The techniques developed here are motivated by feature interaction analysis, but they are also applicable to reasoning about networks of other types of components with suitable notions of data abstraction.


Feature Interaction Atomic Proposition Kripke Structure Client Server Abstract Domain 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Amyot, D., Logrippo, L. (eds.): Feature Interactions in Telecommunications and Software Systems VII, June 2003. IOS Press, Amsterdam (2003)Google Scholar
  2. 2.
    Apt, K.R., Kozen, D.C.: Limits for automatic verification of finitestate concurrent systems. Information Processing Letters 22, 307–309 (1986)CrossRefMathSciNetGoogle Scholar
  3. 3.
    Bouma, L.G., Velthuijsen, H. (eds.): Feature Interactions in Telecommunications Systems, May 1994. IOS Press, Amsterdam (1994)Google Scholar
  4. 4.
    Calder, M., Magill, E. (eds.): Feature Interactions in Telecommunications and Software Systems VI. IOS Press, Amsterdam (2000)Google Scholar
  5. 5.
    Calder, M., Magill, E., Kolberg, S.: Reiff-Marganiec. Feature interaction: A critical review and considered forecast. Computer Networks 41/1, 115–141 (2003)CrossRefGoogle Scholar
  6. 6.
    Calder, M., Miller, A.: Using SPIN for feature interaction analysis - a case study. In: Dwyer, M.B. (ed.) SPIN 2001. LNCS, vol. 2057, pp. 143–162. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  7. 7.
    Calder, M., Miller, A.: Automatic verification of any number of concurrent, communicating processes. In: Proceedings of the 17th IEEE International Conference on Automated Software Engineering (ASE 2002), Edinburgh, UK, September 2002, pp. 227–230. IEEE Computer Society Press, Los Alamitos (2002)CrossRefGoogle Scholar
  8. 8.
    Calder, M., Miller, A.: Generalising feature interactions in email. In: Amyot and Logrippo [1], pp. 187–205Google Scholar
  9. 9.
    Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. The MIT Press, Cambridge (1999)Google Scholar
  10. 10.
    Clarke, E.M., Grumberg, O., Jha, S.: Verifying parameterized networks using abstraction and regular languages. In: Lee, I., Smolka, S.A. (eds.) CONCUR 1995. LNCS, vol. 962, pp. 395–407. Springer, Heidelberg (1995)Google Scholar
  11. 11.
    Clarke, E.M., Grumberg, O., Long, D.: Model checking and abstraction. ACM Transactions on Programming Languages and Systems 16(5), 1512–1542 (1994)CrossRefGoogle Scholar
  12. 12.
    Creese, S.J., Roscoe, A.W.: Data independent induction over structured networks. In: Proceedings of the International Conference on Parallel and Distributed Processing Techniques and Applications (PDPTA 2000), Las Vegas, Nevada, USA, June 2000, vol. II, CSREA Press (2000)Google Scholar
  13. 13.
    Dini, P., Boutaba, R., Logrippo, L. (eds.): Feature Interactions in Telecommunication Networks IV, June 1997. IOS Press, Amsterdam (1997)Google Scholar
  14. 14.
    Allen Emerson, E., Kahlon, V.: Reducing model checking of the many to the few. In: McAllester, D. (ed.) CADE 2000. LNCS, vol. 1831, pp. 236–254. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  15. 15.
    Allen Emerson, E., Namjoshi, K.S.: Reasoning about rings. In: Conference Record of the 22nd Annual ACM Symposium on Principles of Programming Languages (POPL 1995), San Francisco, California, January 1995, pp. 85–94. ACM Press, New York (1995)CrossRefGoogle Scholar
  16. 16.
    German, S.M., Prasad Sistla, A.: Reasoning about systems with many processes. Journal of the ACM 39(3), 675–735 (1992)zbMATHCrossRefGoogle Scholar
  17. 17.
    Hall, R.J.: Feature interactions in electronic mail. In: Calder and Magill [4], pp. 67–82Google Scholar
  18. 18.
    Holzmann, G.J.: The model checker Spin. IEEE Transactions on Software Engineering 23(5), 279–295 (1997)CrossRefMathSciNetGoogle Scholar
  19. 19.
    IN Distributed Functional Plane Architecture, recommmendation q.1204, ITU-T edition (March 1992)Google Scholar
  20. 20.
    Norris Ip, C., Dill, D.L.: Verifying systems with replicated components in Murφ. Formal Methods in System Design 14, 273–310 (1999)CrossRefGoogle Scholar
  21. 21.
    Kimbler, K., Bouma, L.G. (eds.): Feature Interactions in Telecommunications and Software Systems V, September 1998. IOS Press, Amsterdam (1998)Google Scholar
  22. 22.
    Kolberg, M., Magill, E.H., Marples, D., Reiff, S.: Results of the second feature interaction contest. In: Calder and Magill [4], pp. 311–325Google Scholar
  23. 23.
    Kurshan, R.P., McMillan, K.L.: A structural induction theorem for processes. In: Proceedings of the eighth Annual ACM Symposium on Principles of Distrubuted Computing, pp. 239–247. ACM Press, New York (1989)CrossRefGoogle Scholar
  24. 24.
    Kurshan, R.P., Merritt, M., Orda, A., Sachs, S.R.: A structural linearization principle for processes. Formal Methods in System Design 5(3), 227–244 (1994)CrossRefGoogle Scholar
  25. 25.
    Roychoudhury, A., Ramakrishnan, I.V.: Automated inductive verification of parameterized protocols. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 25–37. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  26. 26.
    Wolper, P., Lovinfosse, V.: Properties of large sets of processes with network invariants. In: Sifakis, J. (ed.) CAV 1989. LNCS, vol. 407, pp. 68–80. Springer, Heidelberg (1990) (extended abstract)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2004

Authors and Affiliations

  • Muffy Calder
    • 1
  • Alice Miller
    • 1
  1. 1.Department of Computing ScienceUniversity of GlasgowGlasgowScotland

Personalised recommendations