Skip to main content
SpringerLink
Log in

Formal Modelling of Services for Getting a Better Understanding of the Feature Interaction Problem

A Multi-view Approach

  • Conference paper
  • First Online:
Perspectives of System Informatics (PSI 1999)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 1755))

Abstract

We report results of a joint project with France Telecom on the modelling of telephone services (features) using formal methodologies such as OO ACT ONE, B and TLA+. We show how we formalise the feature interaction problem in a multi-view model, and we examine issues such as animation, validation, proof and verification.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 109.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. J.-R. Abrial. The B book-Assigning Programs to Meanings. Cambridge University Press, 1996.

    Google Scholar 

  2. J. Blom. Formalisation of requirements with emphasis on feature interaction detection. In Feature Interactions In Telecommunications IV, Montreal, Canada, June 1997. IOS Press.

    Google Scholar 

  3. J. Blom, 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. [9].

    Google Scholar 

  4. J. Blom, B. Jonsson, and L. Kempe. Using temporal logic for modular specification of telephone services. In L. G. Bouma and H. Velthuijsen, editors, Feature Interactions in Telecommunications Systems, pages 197–216. IOS Press, 1994.

    Google Scholar 

  5. G. Booch. Object oriented design with applications. Benjamin Cummings, 1991.

    Google Scholar 

  6. L. G. Bouma and H. Velthuijsen, editors. Feature Interactions in Telecommunications Systems. IOS Press, 1994.

    Google Scholar 

  7. R. Boumezbeur and L. Logrippo. Specifying telephone systems in LOTOS. IEEE Communications Magazine, 31(8):38–45, 1993.

    Article  Google Scholar 

  8. Ed. Brinksma, Giuseppe Scollo, and Chris Steenbergen. LOTOS specifications, their implementation and their tests. In Sixth International Symposium on Protocol Testing, Specification and Verification, Montreal, June 1986.

    Google Scholar 

  9. K. E. Cheng and T. Ohta, editors. Feature Interactions in Telecommunications Systems. IOS Press, 1996.

    Google Scholar 

  10. P. Coad and E. Yourdon. Object oriented design. Prentice-Hall (Yourdon Press), 1990.

    Google Scholar 

  11. 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. [6].

    Google Scholar 

  12. L. Constantine. Beyond the madness of methods: System structure methods and converging design. In Software Development 1989. Miller-Freeman, 1989.

    Google Scholar 

  13. Dan Craigen, Susan Gerhart, and Ted Ralston. An international survey of industrial applications of formal methods. Nistgcr 93/626, U.S. Department of Commerce, Technology Administration, National Institute of Standards and Technology, Computer Systems Lab., Gaithersburg, MD 20899, 1993.

    Google Scholar 

  14. Geoff Cutts. Structured system analysis and design method. Blackwell Scientific Publishers, 1991.

    Google Scholar 

  15. P. Dini, R. Boutaba, and L. Logrippo, editors. Feature Interactions in Telecommunications Newtworks IV, Montreal, 1997. IOS Press.

    Google Scholar 

  16. H. Ehrig and Mahr B. Fundamentals of Algebraic Specification I. Springer-Verlag, Berlin, 1985. EATCS Monographs on Theoretical Computer Science (6).

    Google Scholar 

  17. M. Faci and L. Logrippo. Specifying features and analysing their interactions in a lotos environment. In L. G. Bouma and H. Velthuijsen, editors, Feature Interactions in Telecommunications Software System, pages 136–151. IOS Press, 1994. [6].

    Google Scholar 

  18. M. Faci, L. Logrippo, and B. Stepien. Formal specification of telephone systems in lotos: constraint-oriented style approach. Computer Networks and ISDN Systems, 21:53–67, 1991.

    Article  Google Scholar 

  19. 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 

  20. J.-P. Gibson. Formal Object Oriented Development of Software Systems Using LOTOS. Tech. report CSM-114, Stirling University, August 1993.

    Google Scholar 

  21. J.-P. Gibson. Formal object based design in LOTOS. Tr-113, University of Stirling, Computing Science Department, Stirling, Scotland, 1994.

    Google Scholar 

  22. J.-P. Gibson. Feature Requirements Models: Understanding Interactions. In Feature Interaction Workshop 1997, Montreal, Canada, Feature Interaction Workshop. IOS Press, June 1997.

    Google Scholar 

  23. J.-P. Gibson, B. Mermet, and D. Méry. Feature interactions: A mixed semantic model approach. In Gerard O’Regan and Sharon Flynn, editors, 1st Irish Workshop on Formal Methods, Dublin, Ireland, July 1997. Irish Formal Methods Special Interest Group (IFMSIG), Springer Verlag. http://ewic.springer.co.uk/.

  24. J.-P. Gibson, B. Mermet, D. Méry, and Y. Mokhtari. Spécification de services dans une logique temporelle compositionnelle. Rapport de fin du lot1 du marché no96 1B CNET-CNRS-CRIN, Centre de Recherche en Informatique de Nancy, décembre 1996.

    Google Scholar 

  25. J.-P. Gibson and D. Méry. A unifying framework for multi-semantic software development. In Max Mühlhäuser, editor, Special Issues in Object-Oriented Programming. Dpunkt, 1997.

    Google Scholar 

  26. C.A.R Hoare. Communicating Sequential Processes. Prentice-Hall International, 1985.

    Google Scholar 

  27. IEE. Special Collection On Requirements Analysis. IEE Transactions on Software Engineering, 1977.

    Google Scholar 

  28. ISO. LOTOS — a formal description technique based on the temporal ordering of observed behaviour. Technical report, International Organisation for Standardisation IS 8807, 1988.

    Google Scholar 

  29. B. Kelly, M. Crowther, and J. King. Feature interaction detection using sdl models. In GLOBECOM. Communications: The Global Bridge. Conference Record, pages 1857–61. IEEE, 1994.

    Google Scholar 

  30. B. Kelly, M. Crowther, J. King, R. Masson, and J. Delapeyre. Service validation and testing. In K. E. Cheng and T. Ohta, editors, Feature Interactions in Telecommunications Systems, pages 173–184. IOS Press, 1996. [9].

    Google Scholar 

  31. L. Lamport. A temporal logic of actions. Transactions On Programming Languages and Systems, 16(3):872–923, May 1994.

    Article  Google Scholar 

  32. B. Liskov and Zilles S. Programming with abstract data types. In ACM SIGPLAN Notices, volume 9, pages 50–59, 1974.

    Article  Google Scholar 

  33. 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 

  34. 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 

  35. D. Méry. Requirements for a temporal B: Assigning Temporal Meaning to Abstract Machines... and to Abstract Systems. In A. Galloway and K. Taguchi, editors, IFM’99 Integrated Formal Methods 1999, Workshop In Computing Science, YORK, June 1999.

    Google Scholar 

  36. C. A. Middleburg. A simple language for expressing properties of telecommunications services and features. Technical report PU-94-356, KPN Research, Network and Service Control department, 1994.

    Google Scholar 

  37. R. Milner. A Calculus of Communicating Systems. Springer-Verlag, 1980.

    Google Scholar 

  38. D. T. Ross. Structured analysis (SA): A language for communicating ideas. In IEE Transactions on Software Engineering. IEE, 1977.

    Google Scholar 

  39. Steria Méditerrannée. Atelier B, Version 3.2, Manuel de Référence du Langage B. GEC Alsthom Transport and Steria Méediterrannéee and SNCF and INRETS and RATP, 1997.

    Google Scholar 

  40. Kenneth J. Turner. Using Formal Description Techniques-An Introduction to ESTELLE, LOTOS and SDL. John Wiley, New York, January 1993.

    Google Scholar 

  41. K.J. Turner. SPLICE I: Specification using LOTOS for an interactive customer environment — phase 1. University of Stirling SPLICE Internal Technical Document, 1992.

    Google Scholar 

  42. K.J.T. Turner. Using FDTS: An Introduction To ESTELLE, LOTOS and SDL. John Wiley and Sons, 1993.

    Google Scholar 

  43. P. Zave. Feature interactions and formal specifications in telecommunications. Computer, August 1993.

    Google Scholar 

  44. Pamela Zave. The operational versus the conventional approach to software development. Comm. ACM, 27:104–118, 1984.

    Article  Google Scholar 

  45. Pamela Zave. Feature interactions and formal specifications in telecommunications. IEEE Computer Magazine, pages 18–23, August 1993.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. NUI, Maynooth, Ireland

    Paul Gibson

  2. Université Henri Poincaré-Nancy 1 & LORIA UMR 7503 CNRS, Campus Scientifique, BP 239, 54506, Vandœuvre-lès-Nancy, France

    Dominique Méry

Authors
  1. Paul Gibson
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Dominique Méry
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Information Technology, Technical University of Denmark, Bldg. 244, 2800, Lyngby, Denmark

    Dines Bjøner

  2. Computer Science Department, Technical University of Munich, Arcisstr. 21, 80290, Munich, Germany

    Manfred Broy

  3. A.P. Ershov Institute of Informatics Systems, av. Ac. Lavrentyev 6, Novosibirsk, 630090, Russia

    Alexandre V. Zamulin

Rights and permissions

Reprints and permissions

Copyright information

© 2000 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Gibson, P., Méry, D. (2000). Formal Modelling of Services for Getting a Better Understanding of the Feature Interaction Problem. In: Bjøner, D., Broy, M., Zamulin, A.V. (eds) Perspectives of System Informatics. PSI 1999. Lecture Notes in Computer Science, vol 1755. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-46562-6_14

Download citation

  • DOI: https://doi.org/10.1007/3-540-46562-6_14

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-67102-2

  • Online ISBN: 978-3-540-46562-1

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation