Detecting Feature Interactions: How Many Components Do We Need?
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.
KeywordsFeature Interaction Atomic Proposition Kripke Structure Client Server Abstract Domain
Unable to display preview. Download preview PDF.
- 1.Amyot, D., Logrippo, L. (eds.): Feature Interactions in Telecommunications and Software Systems VII, June 2003. IOS Press, Amsterdam (2003)Google Scholar
- 3.Bouma, L.G., Velthuijsen, H. (eds.): Feature Interactions in Telecommunications Systems, May 1994. IOS Press, Amsterdam (1994)Google Scholar
- 4.Calder, M., Magill, E. (eds.): Feature Interactions in Telecommunications and Software Systems VI. IOS Press, Amsterdam (2000)Google Scholar
- 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.Calder, M., Miller, A.: Generalising feature interactions in email. In: Amyot and Logrippo , pp. 187–205Google Scholar
- 9.Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. The MIT Press, Cambridge (1999)Google Scholar
- 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
- 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.Dini, P., Boutaba, R., Logrippo, L. (eds.): Feature Interactions in Telecommunication Networks IV, June 1997. IOS Press, Amsterdam (1997)Google Scholar
- 17.Hall, R.J.: Feature interactions in electronic mail. In: Calder and Magill , pp. 67–82Google Scholar
- 19.IN Distributed Functional Plane Architecture, recommmendation q.1204, ITU-T edition (March 1992)Google Scholar
- 21.Kimbler, K., Bouma, L.G. (eds.): Feature Interactions in Telecommunications and Software Systems V, September 1998. IOS Press, Amsterdam (1998)Google Scholar
- 22.Kolberg, M., Magill, E.H., Marples, D., Reiff, S.: Results of the second feature interaction contest. In: Calder and Magill , pp. 311–325Google Scholar
- 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