Abstract
The composition of services and features often leads to unwanted situations, because it is a non-monotonic operation over services and features. When a new service is added to an existing system, conditions have to be checked to ensure that the resulting system satisfies a list of required properties. Following the system approach of Abrial, we develop services and features in an incremental way and use refinement to model the composition of services and features. Proof obligations state the preservation or the non-preservation of properties, namely invariant or more generally safety properties. The method helps us in understanding when a service is interfering with another, and allows us to give multiple views of each service according to the level of its refinement. Finally, we validate our method with the Atelier B tool.
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.
Similar content being viewed by others
References
J.-R. Abrial. The B book-Assigning Programs to Meanings. Cambridge University Press, 1996.
J.-R. Abrial. Extending B without changing it (for developing distributed systems). In H. Habrias, editor, 1st Conference on the B method, pages 169–190, November 1996.
J.-R. Abrial and L. Mussat. Introducing dynamic constraints in B. In D. Bert, editor, B’98:Recent Advances in the Development and Use of the B Method, volume 1393 of Lecture Notes in Computer Science. Springer-Verlag, 1998.
K. R. Apt and E. R. Olderog. Proof rules and transformations dealing with fairness. Science of Computer Programming, 3:65–100, 1983.
C. Areces, W. Bouma, and M. de Rijke. Feature interaction as a satisfiability problem. In M. Calder and E. Magill, editors, Feature Interactions in Telecommunications and Software Systems VI. IOS Press, 2000. In [8].
J. Biom, B. Johnsson, and L. Kempe. Automatic detection of feature interactions in temporal logic. In K. E. Cheng and T. Ohta, editors, Feature Interactions in Telecommunications Systems, pages 1–19. IOS Press, 1996. [12].
L. G. Bouma and H. Velthuijsen, editors. Feature Interactions in Telecommunications Systems. IOS Press, 1994.
M. Calder and E. Magill, editors. Feature Interactions in Telecommunications and Software Systems VI, Glasgow, 1998. IOS Press.
D. Cansell and D. Méry. Playing with abstraction and refinement for managing features interactions-a methodological approach to feature interaction problem. In J. P. Bowen, S. Dunne, A. Galloway, and S. King, editors, ZB2000 Conference, volume 1878 of Lecture Notes in Computer Science, York, August 2000. Springer Verlag.
D. Cansell, D. Méry, and S. Merz. Predicate diagrams for the verification of reactive systems. In A. Galloway and B. Stoddart, editors, IFM2000, Saarbrücken, November 2000. Springer Verlag.
K. M. Chandy and J. Misra. Parallel Program Design A Foundation. Addison-Wesley Publishing Company, 1988. ISBN 0-201-05866-9.
K. E. Cheng and T. Ohta, editors. Feature Interactions in Telecommunications Systems. IOS Press, 1996.
P. Combes and S. Pickin. Formalisation of a user view of network and services for feature interaction detection. In L. G. Bouma and H. Velthuijsen, editors, Feature Interactions in Telecommunications Software System, pages 120–135. IOS Press, 1994. [7].
P. Dini, R. Boutaba, and L. Logrippo, editors. Feature Interactions in Telecommunications Newtworks IV, Montreal, 1997. IOS Press.
L. du Bousquet, F. Ouebdessalam, J.-L. Richier, and N. Zuanon. Incremental Feature Validation: A Synchronous Point of View. In K. Kimbler and W. Bouma, editors, Feature Interaction Workshop. IOS Press, 1998. In [22].
M. Frappier, A. Mili, and J. Desharnais. Detecting Feature Interaction on Relational Specifications. In P. Dini, R. Boutaba, and L. Logrippo, editors, Feature Interaction Workshop. IOS Press, 1997. In [14].
A. Gammelgaard and J. E. Kristensen. Interaction detection, a logical approach. In L. G. Bouma and H. Velthuijsen, editors, Feature Interactions in Telecommunications Systems, pages 178–196. IOS Press, 1994.
J.-P. Gibson, G. Hamilton, and D. Méry. Integration problems in telephone feature requirements. In A. Galloway and K. Taguchi, editors, IFM’99 Integrated Formal Methods 1999, Workshop In Computing Science, YORK, June 1999. Springer Verlag.
IEEE, editor. Special Section Managing Feature Interactions in Telecommunications Sofware Systems, volume 24. IEEE Computer Society, October 1998.
M. Jackson and P. Zave. Distributed feature composition-a virtual architecture for telecommunications services. IEEE Transactions on Software Engineering, 24(10):831–847, October 1998.
D. O. Keck and P. J. Kuehn. The feature and service interaction problem in telecommunications systems: A survey. IEEE Transactions on Software Engineering, 24(10):779–796, October 1998. In [19].
K. Kimbler and L. G. Bouma, editors. Feature Interactions in Telecommunications and Software Systems V, Lund, 1998. IOS Press.
L. Lamport. A temporal logic of actions. Transactions On Programming Languages and Systems, 16(3):872–923, May 1994.
F. J. Lin, H. Liu, and A. Ghosh. A Methodology for Feature Interaction Detection in the AIN 0.1 Framework. IEEE Transactions on Software Engineering, 24(10):797–817, October 1998. In [19].
B. Mermet and D. Méry. Incremental specification of telecommunication services. In M. Hinchey, editor, First IEEE International Conference on Formal Engineering Methods (ICFEM), Hiroshima, November 1997. IEEE.
B. Mermet and D. Méry. Safe combinations of services using B. In John McDermid, editor, SAFECOMP97 The 16th International Conference on Computer Safety, Reliability and Security, York, September 1997. Springer Verlag.
B. Mermet and D. Méry. Service specifications to B, or not to B. In Mark Ardis, editor, Second Workshop on Formal Methods in Software Practice, Clearwater Beach, Florida, March 4–5 1998. ACM Press.
M. Plath and M. Ryan. Plug-and-play features. In K. Kimbler and W. Bouma, editors, Feature Interaction Workshop. IOS Press, 1998. In [22].
E. Sekerinski and K. Sere, editors. Program Development by Refinement. Springer, 1999.
STERIA-Technologies de l’lnformation, Aix-en-Provence (F). Atelier B, Manuel Utilisateur, 1998. Version 3.5.
K. Turner. Validating Architectural Feature Descriptions using LOTOS. In K. Kimbler and W. Bouma, editors, Feature Interaction Workshop. IOS Press, 1998. In [22].
Union Internationale des Télécommunications. Introduction à l’ensemble de capacités 1 du réseau intelligent. Technical Report UIT-T Q.121l, Union Internationale des Télécommunications, March 1993. Réseau Intelligent.
T. Yoneda and T. Ohta. A Formal Approach for Definition and Detection of Feature Intercation. In K. Kimbler and W. Bouma, editors, Feature Interaction Workshop. IOS Press, 1998. In [22].
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 Springer-Verlag London Limited
About this paper
Cite this paper
Cansell, D., Méry, D. (2001). Abstraction and refinement of features. In: Gilmore, S., Ryan, M. (eds) Language Constructs for Describing Features. Springer, London. https://doi.org/10.1007/978-1-4471-0287-8_5
Download citation
DOI: https://doi.org/10.1007/978-1-4471-0287-8_5
Publisher Name: Springer, London
Print ISBN: 978-1-85233-392-8
Online ISBN: 978-1-4471-0287-8
eBook Packages: Springer Book Archive