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.
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. Blom. Formalisation of requirements with emphasis on feature interaction detection. In Feature Interactions In Telecommunications IV, Montreal, Canada, June 1997. IOS Press.
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].
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.
G. Booch. Object oriented design with applications. Benjamin Cummings, 1991.
L. G. Bouma and H. Velthuijsen, editors. Feature Interactions in Telecommunications Systems. IOS Press, 1994.
R. Boumezbeur and L. Logrippo. Specifying telephone systems in LOTOS. IEEE Communications Magazine, 31(8):38–45, 1993.
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.
K. E. Cheng and T. Ohta, editors. Feature Interactions in Telecommunications Systems. IOS Press, 1996.
P. Coad and E. Yourdon. Object oriented design. Prentice-Hall (Yourdon Press), 1990.
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].
L. Constantine. Beyond the madness of methods: System structure methods and converging design. In Software Development 1989. Miller-Freeman, 1989.
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.
Geoff Cutts. Structured system analysis and design method. Blackwell Scientific Publishers, 1991.
P. Dini, R. Boutaba, and L. Logrippo, editors. Feature Interactions in Telecommunications Newtworks IV, Montreal, 1997. IOS Press.
H. Ehrig and Mahr B. Fundamentals of Algebraic Specification I. Springer-Verlag, Berlin, 1985. EATCS Monographs on Theoretical Computer Science (6).
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].
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.
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. Formal Object Oriented Development of Software Systems Using LOTOS. Tech. report CSM-114, Stirling University, August 1993.
J.-P. Gibson. Formal object based design in LOTOS. Tr-113, University of Stirling, Computing Science Department, Stirling, Scotland, 1994.
J.-P. Gibson. Feature Requirements Models: Understanding Interactions. In Feature Interaction Workshop 1997, Montreal, Canada, Feature Interaction Workshop. IOS Press, June 1997.
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/.
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.
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.
C.A.R Hoare. Communicating Sequential Processes. Prentice-Hall International, 1985.
IEE. Special Collection On Requirements Analysis. IEE Transactions on Software Engineering, 1977.
ISO. LOTOS — a formal description technique based on the temporal ordering of observed behaviour. Technical report, International Organisation for Standardisation IS 8807, 1988.
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.
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].
L. Lamport. A temporal logic of actions. Transactions On Programming Languages and Systems, 16(3):872–923, May 1994.
B. Liskov and Zilles S. Programming with abstract data types. In ACM SIGPLAN Notices, volume 9, pages 50–59, 1974.
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.
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.
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.
R. Milner. A Calculus of Communicating Systems. Springer-Verlag, 1980.
D. T. Ross. Structured analysis (SA): A language for communicating ideas. In IEE Transactions on Software Engineering. IEE, 1977.
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.
Kenneth J. Turner. Using Formal Description Techniques-An Introduction to ESTELLE, LOTOS and SDL. John Wiley, New York, January 1993.
K.J. Turner. SPLICE I: Specification using LOTOS for an interactive customer environment — phase 1. University of Stirling SPLICE Internal Technical Document, 1992.
K.J.T. Turner. Using FDTS: An Introduction To ESTELLE, LOTOS and SDL. John Wiley and Sons, 1993.
P. Zave. Feature interactions and formal specifications in telecommunications. Computer, August 1993.
Pamela Zave. The operational versus the conventional approach to software development. Comm. ACM, 27:104–118, 1984.
Pamela Zave. Feature interactions and formal specifications in telecommunications. IEEE Computer Magazine, pages 18–23, August 1993.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights 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