Abstract
The problem of detecting feature interactions in telephone systems design is addressed. The method proposed involves specification of the features in LOTOS, and uses an analysis technique called backward reasoning. This is is implemented in LOTOS by a combination of backward and forward execution. A tool to help carry out backward execution is presented. A detailed example of the use of the technique is given, involving the three-way-calling and call-waiting features.
Chapter PDF
Similar content being viewed by others
Keyword codes
Keywords
References
Brinksma, E., and Eertink, H. Goal-Driven LOTOS Execution. To appear in: A. Danthine, G. Leduc, and P.Wolper (eds). Protocol Specification, Testing and Verification, XIII. North-Holland
Boumezbeur, R., and Logrippo, L. Specifying telephone systems in LOTOS. IEEE Communications Magazine, Aug. 1993, 38–45.
The suspend and resume operator. Canadian contribution to ISO TC97/ SC21, WG 1, November 1994 (available from authors).
Cameron, E.J., Griffeth, N., Lin, Y.-J., Nilson, M.E., Schnure, W.K.,Velthuijsen, H. A Feature Interaction Benchmark for IN and Beyond. IEEE Communication Magazine, 31, 3, 64–69, 1993.
Danthine, A., and Bremer, J. Modeling and Verification of End-to-End Transport Protocols. Computer Networks, 2 (1978), 381–395.
Faci, M. and Logrippo, L. Specifying Features and Analyzing their Interactions in a LOTOS Environment. To appear in the Proc. of the 2nd International Workshop on Feature Interaction in Telephone Systems, Amsterdam, 1994.
Haj-Hussein, M., Logrippo, L., and Sincennes, J. Goal-oriented Execution of LOTOS Specifications. In: M. Diaz and R. Groz (Eds.) Formal Description Techniques, V. North-Holland, 1993, 311–327.
Holzmann, G.J. Backward Symbolic Execution of Protocols. In: Y.Yemini, R. Strom, and S. Yemini (eds.) Protocol Specification, Testing, and Verification, IV. North-Holland, 1985, 19–27.
Lin,Y.J. Analyzing Service Specifications Based upon the Logic Programming Paradigm. IEEE GLOBECOMM `90, vol. 1, 611–655.
Dahl, O.C. and Najm E. Specification and Detection of IN Service Interference using LOTOS. To appear in: R. Tenney, P.D. Amer, M. Ü. Uyar (eds) Formal Description Techniques, VI, North-Holland, 1994.
Quemada, J., Larrabeiti, D., and Pavon, S. Compressing the state space representation, To appear in: R. Tenney, P.D. Amer, M. Ü. Uyar (eds) Formal Description Techniques, VI, North-Holland, 1994.
Stepien, B. and Logrippo, L. Status-Oriented Telephone Service Specification. To appear in: T. Rus and C. Rattray (eds.) Theories and Experiences for Real-Time System Development, 1994.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1995 Springer Science+Business Media Dordrecht
About this chapter
Cite this chapter
Stepien, B., Logrippo, L. (1995). Feature Interaction Detection using Backward Reasoning with LOTOS. In: Vuong, S.T., Chanson, S.T. (eds) Protocol Specification, Testing and Verification XIV. IFIP Advances in Information and Communication Technology. Springer, Boston, MA. https://doi.org/10.1007/978-0-387-34867-4_5
Download citation
DOI: https://doi.org/10.1007/978-0-387-34867-4_5
Publisher Name: Springer, Boston, MA
Print ISBN: 978-1-4757-6308-9
Online ISBN: 978-0-387-34867-4
eBook Packages: Springer Book Archive