Verifying Reliable Data Transmission over UMTS Radio Interface with High Level Petri Nets
Standard specifications of telecommunication protocols are mainly written using informal language. Therefore testing the standard, i.e. the definition of the core functionality, requires formal modelling of the protocol. In this article we describe the modelling and verification of a third generation mobile telecommunication protocol. We take the SDL description of the protocol as a starting point for our High Level Petri Net model. Since the size of the real-life protocols is enormous, we apply various abstraction techniques in the modelling phase. Basing on these and our previous experience, we introduce several heuristics for intelligent protocol modelling. Next we describe in detail the verification and modelling task, and derivation of the properties to be verified from the protocol specification.We are able to verify the most essential properties for reliable data transmission. Before executing the actual verification task, we plan a verification strategy, where for example the verification order of the properties and the appropriate configurations for the protocol and channel components for each run are considered.
KeywordsUser Process Radio Link Control Reliable Data Transmission Acknowledge Mode Test Automaton
- 2.Yifei Dong, Xiaoqun Du, Y.S. Ramakrishna, C.R. Ramakrishnan and I.V. Ramakrishnan, Scott A. Smolka, Oleg Sokolsky, and Eugene W. Stark and David S. Warren. Fighting Livelock in the i-Protocol: A Comparative Study of Verification Tools. In TACAS’99, 1999.Google Scholar
- 3.J. Ellesberg, D. Hogrefe, and A. Sarma. SDL: Formal Object-Oriented Language for Communicating Systems. Prentice Hall, 1997.Google Scholar
- 4.Juana Helovuo and Sari Leppänen.Exploration Testing. In ICACSD 2001, 2nd International Conference on Application of Concurrency to System Design, pages 201–210, 2001.Google Scholar
- 5.International Standards Organization. High-level Petri Nets–Concepts, Definitions and Graphical Notation. Final Draft International Standard ISO/IEC 15909, Version 4.7.1, 2000. The standard is available on the web, http://www.daimi.au.dk/PetriNets/st andardisation.
- 6.H. Kaaranan, A. Ahtiainen, L. Laitinen, S. Naghian, and V. Niemi. UMTS Networks: Architecture, Mobility and Services. Wiley amp Sons Ltd, 2001.Google Scholar
- 7.R. Kaivola. Equivalences, Preorders and Compositional Verification for Linear Time Temporal Logic and Concurrent Systems. PhD thesis, Helsingin yliopisto. Tietojenkäsittelytieteen laitos, 1996.Google Scholar
- 8.Sari Leppänen and Matti Luukkainen. CompositionalVerification of a Third Generation Mobile Communication Protocl. In InternationalWorkshop on Distributed SystemValidation and Verfication, ICDCS 2000 Workshop. IEEE Computer Society, 2000.Google Scholar
- 9.Marko Mäkelä. A Reachability Analyzer for Algebraic System Nets. Research Report A69, Helsinki University of Technology, Laboratory for Theoretical Computer Science, 2001.Google Scholar
- 10.Markus Malmqvist. Methodology of Dynamical Analysis of SDL Programs Using Predicate/ Transition Nets. Technical report B16, Helsinki University of Technology, Digital Systems Laboratory, April 1997.Google Scholar
- 12.A. Toskala and H. Holma. WCDMA for UMTS, Radio Access for Third Generation Mobile Communications. Wiley amp Sons Ltd, 2000.Google Scholar
- 13.Pierre Wolper. Expressing Interesting Properties of Programs in Propositional Temporal Logic. In Proceedings of the 13thACMSymposium on Principles of Programming Languages, 1986.Google Scholar