Skip to main content
SpringerLink
Log in

Detecting Feature Interactions in the Terrestrial Trunked Radio (TETRA) Network Using Promela and Xspin

  • Conference paper
  • First Online:
Theoretical and Practical Aspects of SPIN Model Checking (SPIN 1999)

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

Included in the following conference series:

  • 428 Accesses

Abstract

The problem caused by feature interactions serve to delay and increase the costs of introducing features to existing networks. We introduce a three stage technique that detects interactions in the TETRA network. Promela is used to model the network and features and its requirements are specified using linear temporal logic. The Xspin toolkit is used to verify and validate the model against its requirements.

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 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.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. European Telecommunications Standards Institute. Radio Equipment and Systems (RES); Trans-European Trunked Radio (TETRA); Voice plus Data (V+D); Part 10: Supplementary Services Stage 1; Part 10-04: Call Diversion. ETS 300 392-10-04.

    Google Scholar 

  2. European Telecommunications Standards Institute. Radio Equipment and Systems (RES); Trans-European Trunked Radio (TETRA); Voice plus Data (V+D); Part 11: Supplementary Services (SS) Stage 2; Part 11-19: Barring of Incoming Calls (BIC). ETS 300 392-11-19.

    Google Scholar 

  3. Gerard J. Holzmann. Design and validation of computer protocols. Prentice Hall, 1990. ISBN 0-13-539925-4.

    Google Scholar 

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

    Article  Google Scholar 

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

    Article  Google Scholar 

  6. F. Joe Lin and Yow-Jian Lin. A Building Block Approach to Detecting and Resolving Feature Interaction. In W. Bouma and H. Velthuijsen editors, Feature Interactions in Telecommunication Systems, chapter 6, pages 86–119. IOS Press, 1994.

    Google Scholar 

  7. Zohar Manna and Amir Pnueli. The Temporal logic of Reactive and Concurrent Systems Specification. Springer-Verlag, 1991. ISBN 0-387-97664-7 (v. 1).

    Google Scholar 

  8. S. Tsang and E.H. Magill. Learning To Detect and Avoid Run-Time Feature Interactions in Intelligent Networks. IEEE Transactions on Software Engineering, 24(10):818–830, October 1998.

    Article  Google Scholar 

  9. ETSI TC-RES. Radio Equipement and Systems (RES); Trans-European Trunked Radio (TETRA); Voice plus Data (V+D) Part 2: Air Interface (AI). European Telecommunications Standard, 1995. ETS 300 392-2.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, Royal Holloway, University of London, Egham Hill Egham, Surrey, TW20 0EX, UK

    Carl B. Adekunle & Steve Schneider

Authors
  1. Carl B. Adekunle
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Steve Schneider
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Electrical Engineering and Department of Mathematics and Computer Science, Eindhoven University of Technology, 5600, MB Eindhoven, The Netherlands

    Dennis Dams

  2. Intel Microprocessor Products Group, Strategic CAD Laboratories, 5200 NE Elam Young Parkway, JFT-104, Hillsboro, OR, 97124-6497, USA

    Rob Gerth

  3. Department of Electrical and Computer Engineering, University of Waterloo, Waterloo, Ontario, N2L 3G1, Canada

    Stefan Leue

  4. C.N.R.-Ist., CNUCE via Santa Maria 36, 56126, Pisa, Italy

    Mieke Massink

Rights and permissions

Reprints and permissions

Copyright information

© 1999 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Adekunle, C.B., Schneider, S. (1999). Detecting Feature Interactions in the Terrestrial Trunked Radio (TETRA) Network Using Promela and Xspin. In: Dams, D., Gerth, R., Leue, S., Massink, M. (eds) Theoretical and Practical Aspects of SPIN Model Checking. SPIN 1999. Lecture Notes in Computer Science, vol 1680. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48234-2_10

Download citation

  • DOI: https://doi.org/10.1007/3-540-48234-2_10

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-66499-4

  • Online ISBN: 978-3-540-48234-5

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation