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.