Abstract
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.
This is a preview of subscription content, log in via an institution to check access.
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
Amyot, D., Logrippo, L. (eds.): Feature Interactions in Telecommunications and Software Systems VII, June 2003. IOS Press, Amsterdam (2003)
Apt, K.R., Kozen, D.C.: Limits for automatic verification of finitestate concurrent systems. Information Processing Letters 22, 307–309 (1986)
Bouma, L.G., Velthuijsen, H. (eds.): Feature Interactions in Telecommunications Systems, May 1994. IOS Press, Amsterdam (1994)
Calder, M., Magill, E. (eds.): Feature Interactions in Telecommunications and Software Systems VI. IOS Press, Amsterdam (2000)
Calder, M., Magill, E., Kolberg, S.: Reiff-Marganiec. Feature interaction: A critical review and considered forecast. Computer Networks 41/1, 115–141 (2003)
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)
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)
Calder, M., Miller, A.: Generalising feature interactions in email. In: Amyot and Logrippo [1], pp. 187–205
Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. The MIT Press, Cambridge (1999)
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)
Clarke, E.M., Grumberg, O., Long, D.: Model checking and abstraction. ACM Transactions on Programming Languages and Systems 16(5), 1512–1542 (1994)
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)
Dini, P., Boutaba, R., Logrippo, L. (eds.): Feature Interactions in Telecommunication Networks IV, June 1997. IOS Press, Amsterdam (1997)
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)
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)
German, S.M., Prasad Sistla, A.: Reasoning about systems with many processes. Journal of the ACM 39(3), 675–735 (1992)
Hall, R.J.: Feature interactions in electronic mail. In: Calder and Magill [4], pp. 67–82
Holzmann, G.J.: The model checker Spin. IEEE Transactions on Software Engineering 23(5), 279–295 (1997)
IN Distributed Functional Plane Architecture, recommmendation q.1204, ITU-T edition (March 1992)
Norris Ip, C., Dill, D.L.: Verifying systems with replicated components in Murφ. Formal Methods in System Design 14, 273–310 (1999)
Kimbler, K., Bouma, L.G. (eds.): Feature Interactions in Telecommunications and Software Systems V, September 1998. IOS Press, Amsterdam (1998)
Kolberg, M., Magill, E.H., Marples, D., Reiff, S.: Results of the second feature interaction contest. In: Calder and Magill [4], pp. 311–325
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)
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)
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)
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)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Calder, M., Miller, A. (2004). Detecting Feature Interactions: How Many Components Do We Need?. In: Ryan, M.D., Meyer, JJ.C., Ehrich, HD. (eds) Objects, Agents, and Features. Lecture Notes in Computer Science, vol 2975. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-25930-5_4
Download citation
DOI: https://doi.org/10.1007/978-3-540-25930-5_4
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-21989-7
Online ISBN: 978-3-540-25930-5
eBook Packages: Springer Book Archive