The Specification and Verification of an Experimental ATM Signalling Protocol
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.
KeywordsATM Signalling Formal Specification Temporal Logic Model Checking.
- Birrell, A. and Nelson, G. (1984) Implementing RPC. ACM Transactions on Computer Systems, 2 (1).Google Scholar
- 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
- Chandy, K.M. and Misra, J. (1988) Parallel Program Design - A Foundation. Addison-Wesley, Reading, Massachusetts.Google Scholar
- 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
- 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
- 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
- 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
- Holzmann, G.J. (1991) Design and Validation of Computer Protocols. Software. Prentice-Hall, London, 1991.Google Scholar
- Lamport, L. (1991) The Temporal Logic of Actions. Technical Report 79, Digital Systems Research Center, Palo Alto, California.Google Scholar
- 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
- McAuley, D. (1990) Protocol Design for High Speed Networks. PhD thesis, University of Cambridge Computer Laboratory, Pembroke Street, Cambridge, CB2 3QG.Google Scholar
- 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
- 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