Abstraction and refinement of features

  • Dominique Cansell
  • Dominique Méry

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.

Keywords

Beach Mili 

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    J.-R. Abrial. The B book-Assigning Programs to Meanings. Cambridge University Press, 1996.Google Scholar
  2. 2.
    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.Google Scholar
  3. 3.
    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.Google Scholar
  4. 4.
    K. R. Apt and E. R. Olderog. Proof rules and transformations dealing with fairness. Science of Computer Programming, 3:65–100, 1983.MathSciNetMATHCrossRefGoogle Scholar
  5. 5.
    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].Google Scholar
  6. 6.
    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].Google Scholar
  7. 7.
    L. G. Bouma and H. Velthuijsen, editors. Feature Interactions in Telecommunications Systems. IOS Press, 1994.Google Scholar
  8. 8.
    M. Calder and E. Magill, editors. Feature Interactions in Telecommunications and Software Systems VI, Glasgow, 1998. IOS Press.Google Scholar
  9. 9.
    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.Google Scholar
  10. 10.
    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.Google Scholar
  11. 11.
    K. M. Chandy and J. Misra. Parallel Program Design A Foundation. Addison-Wesley Publishing Company, 1988. ISBN 0-201-05866-9.Google Scholar
  12. 12.
    K. E. Cheng and T. Ohta, editors. Feature Interactions in Telecommunications Systems. IOS Press, 1996.Google Scholar
  13. 13.
    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].Google Scholar
  14. 14.
    P. Dini, R. Boutaba, and L. Logrippo, editors. Feature Interactions in Telecommunications Newtworks IV, Montreal, 1997. IOS Press.Google Scholar
  15. 15.
    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].Google Scholar
  16. 16.
    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].Google Scholar
  17. 17.
    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.Google Scholar
  18. 18.
    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.Google Scholar
  19. 19.
    IEEE, editor. Special Section Managing Feature Interactions in Telecommunications Sofware Systems, volume 24. IEEE Computer Society, October 1998.Google Scholar
  20. 20.
    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.CrossRefGoogle Scholar
  21. 21.
    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].CrossRefGoogle Scholar
  22. 22.
    K. Kimbler and L. G. Bouma, editors. Feature Interactions in Telecommunications and Software Systems V, Lund, 1998. IOS Press.Google Scholar
  23. 23.
    L. Lamport. A temporal logic of actions. Transactions On Programming Languages and Systems, 16(3):872–923, May 1994.CrossRefGoogle Scholar
  24. 24.
    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].CrossRefGoogle Scholar
  25. 25.
    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.Google Scholar
  26. 26.
    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.Google Scholar
  27. 27.
    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.Google Scholar
  28. 28.
    M. Plath and M. Ryan. Plug-and-play features. In K. Kimbler and W. Bouma, editors, Feature Interaction Workshop. IOS Press, 1998. In [22].Google Scholar
  29. 29.
    E. Sekerinski and K. Sere, editors. Program Development by Refinement. Springer, 1999.Google Scholar
  30. 30.
    STERIA-Technologies de l’lnformation, Aix-en-Provence (F). Atelier B, Manuel Utilisateur, 1998. Version 3.5.Google Scholar
  31. 31.
    K. Turner. Validating Architectural Feature Descriptions using LOTOS. In K. Kimbler and W. Bouma, editors, Feature Interaction Workshop. IOS Press, 1998. In [22].Google Scholar
  32. 32.
    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.Google Scholar
  33. 33.
    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].Google Scholar

Copyright information

© Springer-Verlag London Limited 2001

Authors and Affiliations

  • Dominique Cansell
    • 1
    • 2
  • Dominique Méry
    • 1
    • 3
  1. 1.LORIA UMR 7503Vandreuvre-lès-Nancy CédexFrance
  2. 2.Université de Metz, lie du SauleyMetz CédexFrance
  3. 3.Université Henri Poincaré Nancy 1Vandreuvre-lès-Nancy CédexFrance

Personalised recommendations