Advertisement

The Specification and Verification of an Experimental ATM Signalling Protocol

  • Dieter Barnard
  • Simon Crosby
Chapter
Part of the IFIP Advances in Information and Communication Technology book series (IFIPAICT)

Abstract

In this paper we present a formal specification of an experimental ATM signalling protocol using Temporal Logic of Transitions (TLT). The protocol allows users to request network services from an ATM-Master, which is responsible for control and management in a particular network domain. Robust and correct operation of the protocol is essential due to the use of unreliable RPC for communication and the instability of the underlying network. This was achieved by specifying the protocol compositionally, in terms of TLT programs with interfaces. This permitted each component to be verified individually using a temporal logic model checker, which releaved important errors in early versions of the specification. The paper includes a list of verified properties, eg. the absence of livelock and correct call termination, together with their verification times, to support this approach.

Keywords

ATM Signalling Formal Specification Temporal Logic Model Checking. 

References

  1. Birrell, A. and Nelson, G. (1984) Implementing RPC. ACM Transactions on Computer Systems, 2 (1).Google Scholar
  2. Black, R., Leslie, I. and McAuley, D. (1994) Experiences of building an ATM switch for the Local Area. In Communications Architectures, Protocols and Applications volume 24(4) of Computer Communications Review. ACM SIGCOMM, ACM Press.Google Scholar
  3. Bryant, R.E. (1992) Symbolic boolean manipulation with ordered binary-decision diagrams. ACM Computing Surveys, 24 (3): 293–318.CrossRefGoogle Scholar
  4. Burch, J.R., Clarke E.M., McMillan K.L., Dill D.L. and Hwang, L.J. (1992) Symbolic model checking: 1020 states and beyond. Information and Computation, 98: 142–170.MathSciNetCrossRefzbMATHGoogle Scholar
  5. Chandy, K.M. and Misra, J. (1988) Parallel Program Design - A Foundation. Addison-Wesley, Reading, Massachusetts.Google Scholar
  6. Cuéllar, J., Barnard, D. and Crosby, S. (1994a) A Tutorial Introduction to TLT. Part III: Case Study - an ATM signalling protocol. Siemens Corporate Research and Development, ZFE T SE 1, D-81730 Munich, Germany.Google Scholar
  7. Cuéllar, J. and Huber, M. (1994b) The FZI Production Cell Case Study: A distributed solution using TLT. In Proc. of the FZI volume 891 of LNCS. Springer-Verlag.Google Scholar
  8. Cuéllar, J., Wildgruber, I. and Barnard, D. (1994c) Combining the Design of Industrial Systems with Effective Verification Techniques. In Naftalin, Denvir, and Betran, editors, Proc. of FME’94, volume 873 of LNCS, pages 639–658, Barcelona, Spain, October 1994. Springer-Verlag.Google Scholar
  9. Filkorn, T., Schneider, H.A., Scholz, A., Strasser, A. and Warkentin, P. (1994) SVE User’s Guide. Technical report, Siemens AG, ZFE T SE 1, D-81730 München, Germany.Google Scholar
  10. Holzmann, G.J. (1991) Design and Validation of Computer Protocols. Software. Prentice-Hall, London, 1991.Google Scholar
  11. Lamport, L. (1991) The Temporal Logic of Actions. Technical Report 79, Digital Systems Research Center, Palo Alto, California.Google Scholar
  12. Lampson, B.W., Lynch, N.A. and Sorgaard-Andersen, J.F. (1993) Correctness of atmost-once message delivery protocols. In R.L. Tenney, P.D. Amer, and M.U. Uyar, editors, Proc. of FORTE’93, volume VI of FDT, pages 385–400, Boston, MA. IFIP.Google Scholar
  13. McAuley, D. (1990) Protocol Design for High Speed Networks. PhD thesis, University of Cambridge Computer Laboratory, Pembroke Street, Cambridge, CB2 3QG.Google Scholar
  14. Naik, V.G. and Sistla, A.P. (1994) Modeling and verification of a real life protocol using symbolic model checking. In David L. Dill, editor, Proc. of CAV’9j, volume 818 of LNCS, pages 194–206, Stanford, CA. Springer-Verlag.Google Scholar
  15. University of Cambridge Systems Research Group. (1994) ATM document collection. Technical note, University of Cambridge Computer Laboratory, Pembroke Street, Cambridge, CB2 3QG, UK. available as: http://www.cl.cam.ac.uk/Research/SRG/bluebook.html
  16. Wolper, P.L. (1985) The tableau method for temporal logic: An overview. Logique et Analyse, 28: 119–136.MathSciNetzbMATHGoogle Scholar

Copyright information

© IFIP International Federation for Information Processing 1996

Authors and Affiliations

  • Dieter Barnard
    • 1
  • Simon Crosby
    • 2
  1. 1.ZFE T SE 1Siemens AGMunichGermany
  2. 2.Computer LaboratoryUniv. of CambridgeCambridgeUK

Personalised recommendations