вход по аккаунту



код для вставкиСкачать
Received: 23 May 2016
Revised: 19 July 2017
Accepted: 10 September 2017
DOI: 10.1002/dac.3447
Formal verification of a radio network random access
Ahmed Roumane1
| Bouabdellah Kechar1 | Belkacem Kouninef2
Laboratoire en Informatique Industrielle
et Réseaux—RIIR, Département
Informatique, Faculté des Sciences Exactes
et Appliquées, Université Oran1 Ahmed
Ben Bella, BP1524 EL Mnaouer Oran,
LAboratoire de Recherche Appliquée au
TIC‐LARATIC, National Institute of
Telecommunications and ICT (INTTIC),
BP 1518 EL Mnaouer Oran, Algeria
Ahmed Roumane, Laboratoire en
Informatique Industrielle et Réseaux—
RIIR, Département Informatique, Faculté
des Sciences Exactes et Appliquées,
Université Oran1 Ahmed Ben Bella, BP
1524 EL Mnaouer Oran, Algeria.
Email: roumane.ahmed@edu.univ‐oran1.
In this paper, the random access procedure of Universal Mobile Telecommunications System network is investigated. We have proposed a model based on
communicating timed automata that represents the main functions related to
the random access procedure including the user equipment, the base station
(node B or BTS), and the channel. Then, we have used computational tree logic
formula to specify the proprieties to be verified. The model and the formulas
serve as inputs to the model checker, which is used as a verification engine,
ie, UPPAAL and SPIN. The formal verification approach shows that the
protocol has several drawbacks that may not be detected by simulation.
formal verification, model checking, random access procedure, spin, UMTS, UPPAAL
Cellular mobile networks are becoming more and more important and being a part of our everyday life. This technology
is widely used for plethora of applications that exploit the mobility and the flexibility of wireless communications. As the
number of the users/devices (eg, internet of things) grows in the network, several problems like congestion and energy
efficiency may occur, especially when the users try to access the network through a contention‐based and collision risk‐
shared channel, by executing the random access procedure that constitutes the heart of this study.
The random access procedure is the most critical and important step before establishing communication in wireless
cellular networks because it represents the last step of synchronization and the first step toward a real communication
through the network. Ensuring the correctness of this protocol is one of the main concerns for every network operator
because a small problem may prevent users from accessing and exploiting the network resources. To avoid such
unforeseen scenario, it is important to check the validity of this procedure by using a formal approach. Thus, the main
motivation of this work is to show how the formal verification technique can be used to evaluate the random access
procedure in Universal Mobile Telecommunications Service (UMTS) frequency division duplex mode.
Verification is a crucial step in software and hardware development because errors can be fixed at low cost when they
are discovered in earlier design phase. In an interconnected world, communication protocols play a central role, thus
proving that its correctness is of everyone's interests. This motivates us to study the most efficient existing verification
techniques, those which are based on formal models, to apply them for communication protocol. Model checking is
the highly recommended formal verification technique because it is fully automated and it converges to the exact
answer, although unfortunately, it suffers from state space explosion problem and its correctness depends on the
Int J Commun Syst. 2017;e3447.
Copyright © 2017 John Wiley & Sons, Ltd.
1 of 18
2 of 18
correctness of the model.1 In contrary of test and simulation, this technique explores the full state space and therefore
allows reasoning about all possible behaviors of the system.
Understanding the “model checking” technique requires some backgrounds in automata theory, automata‐based
programming, propositional logic, temporal logic, linear temporal logic (LTL), computational tree logic (CTL), complexity theory, and graphs.1 For a practical use, a model checking tool (eg, UPPAAL2 and SPIN3) and a detailed description of
the protocol to be verified are needed.
The rest of this paper is organized as follows: Section 2 presents an overview of some scientific works related to
protocol verification. Section 3 gives a general description of the random access procedure as it was specified by
3GPP.4,5 Section 4 covers UPPAAL model checking tool, and in Section 5, we introduce the formal model of the protocol
for both UPPAAL and SPIN and then investigate the verification of properties. Section 6 discusses the results; then, we
draw a conclusion in Section 7.
Recently, many researchers have applied formal verification techniques to several hardware and software systems
(eg, industrial systems6,7 and software systems8). Communication protocols have been subject to formal verification in
several recent papers, but most of them focused on security aspects9 rather than communication mechanisms. To the best
of our knowledge, this paper is the first that investigates the random access procedure of mobile cellular networks through
formal methods. This section summarizes some of the most significant and recent papers related to our study. As the
correctness of the communication mechanisms has been studied at different layers, the papers can be classified as follows:
(MAC layer,10-13 network “routing” layer,14-17 and application layer18).
Vattakunnel et al18 introduce the interactions between layers of the protocol stack at the same node in the formal
representation of the model by using PROMELA. The approach has been tested for an application layer protocol,
namely, Constrained Application Protocol, to verify properties (eg, safety, liveness, and correctness) by using SPIN model
checker. The authors conclude that their model is suitable for application layer protocols.
The well‐known ZigBee protocol (the routing part) has been studied in Rashid et al14 for smart grid application; using
UPPAAL tool, the protocol was proven to be collision free and presents a bounded delay for user to user communication.
Fehnker et al15 used the model checking technique as a diagnostic tool to rigorously analyze the behavior of Ad Hoc
On‐Demand Distance Vector routing protocol. They have derived an accurate model from the process algebra Algebra
for Wireless Networks specification of the protocol. Using UPPAAL, the authors set up scenarios and repeatedly check
3 proprieties (“a route is found,” “no suboptimal route,” and “an optimal route is found”), then they quantify the results
over the number of topologies to calculate the percentage of property satisfaction.
Chiyangwa and Kwiatkowska16 used UPPAAL to model the Ad Hoc On‐Demand Distance Vector protocol as timed
automata and verified some of its timing properties, such as timely route discovery and the ability to deliver a message
within a specified time period. By model checking this protocol, the authors have discovered an unwanted dependency
between the network size and the lifetime of the route, for which they have proposed a modification to the standard
protocol that alleviates the problem by adapting the route timeouts to the network size.
Eidgahi and Rafe17 proposed a timed automata‐based model that accurately captures the timing behavior of the
routing protocol to rigorously analyze its vulnerabilities. They have considered as a case study the route optimization
mechanism of the MIPv6 protocol.
In Hammal et al,10 a MAC protocol was studied by Mr Hammal. They used UPPAAL to check the correctness of the
AMCLM protocol, which is an enhancement of the 802.11 Carrier Sense Multiple Access with Collision Avoidance protocol. In a clear methodology, the authors started by creating the UML state machines that accurately model the abstract
behaviors of the protocol components, then they determined the corresponding timed automata that are used as formal
models. The author formulated some properties in CTL temporal logic formula, from which they concluded that the
protocol is proven to be deadlock‐free and it satisfies the safety and other reachability and liveness properties.
Ruiz et al11 proposed a formal analysis of a novel collision resolution algorithm for WSN named 2CS‐WSN, which is
designed to be employed during the contention phase. They used a discrete time Markov chain model and PRISM tool as
model checker to verify the correctness of the protocol in collision resolution time and energy consumption. Saghar
et al12 used UPPAAL to investigate a serial BUS communication protocol used for communication between embedded
system elements in a faulty environment; the verification results show that some propriety holds (eg, deadlock free),
but the authors discovered and corrected several errors such as buffer overflow.
3 of 18
In Pan et al,13 a formal model of the CAN bus protocol is proposed. A total of 11 properties have verified using
UPPAAL tool. The results show that the CAN bus suffers from deadlock, starvation, and data inconsistency problems.
The authors claim that applying dynamic priority scheduling and bus‐off recovery mechanism can partly solve the
problems in the application layer.
Model checking was widely used for studying security properties of protocols, like Sik and Bae,19,20 who used the
FDR model checker over Casper tool to formally verify some security and safety properties of their proposed protocols.
Interested readers may find further details in surveys9,21 and a helpful tutorial in Qadir and Hasan.22
To get a global look, we summarized the presented works in Table 1.
From Table 1, we can clearly observe that the UPPAAL tool has been more and more used for verification these
years, due to its simplicity, efficiency, and expressiveness power that makes the tool suitable for different domains. So,
this justifies the use of this tool in our study.
3 | T H E RA N D O M AC C E S S P R O C E D U R E
To get a clear idea of this procedure, we should understand the specific concept of channel used in modern wireless
cellular networks. In this work, we are interested in 2 physical channels,23 the Physical Random Access CHannel
(PRACH) and the Acquisition Indicator Channel. To simplify the picture, a physical channel can be seen as a repetition
of 10 ms frame, each of which is composed of 15 time slots. As can be seen from Figure 1, the PRACH and Acquisition
Indicator Channel combine 2 consecutive radio frames to define a special structure of 20 ms frame divided into 2 access
slot sets; the first group has 8 access slots (from 0 to 7), while the other has only 7.
To define a prioritized access scheme, the PRACH resources (ie, preamble signatures and access slots) are organized
in groups and attached to different access service classes (ASCs) of different priorities; this allows a service‐based
contention that protects the important traffic (eg, voice) from congestion of the less important one. Access service classes
are identified by a number i, which indicates a certain portion of the PRACH resources and a probability of persistence
Pi. The persistence value Pi is used to define a probabilistic access control of each class. The index “i” is defined in the
range of 0 to 7 to indicate the priority of the class of service requesting a PRACH access (lowest priority = 7, highest
priority = 0). The set of ASC parameters are configured by the RRC and communicated to MAC sublayer.4
The RACH transmission consists of a preamble and message part. The preamble is a sequence of 4096 chips called
access signature; it is transmitted in 1 access slot “1 ms long.” The message part can carry short user packets or an uplink
signaling and can be transmitted in 10 or 20 ms frame.24
Recent works on modeling and verification of communication protocols
Category of studied
Security analysis of network
protocol (mobile IPv6)
Real‐time automata
Formal analysis of
ZigBee‐based routing
‐Collision avoidance
‐Bounded liveness
Discrete time Markov
chains (DTMC)
Formal analysis of a collision
resolution algorithm for WSN
‐Collision resolution time
‐Energy consumption
Timed automata extracted
from UML state diagram
Verification of an enhanced
variant of DCF‐based IEEE
802.11 carrier‐sense multiple
access with collision avoidance
Timed automata
Verification of communication
protocol CAN bus
Timed automata derived
from process algebra
Algebra for Wireless
Verification of Ad Hoc
On‐Demand Distance
Vector routing protocol
Modeling approach
Timed automata
4 of 18
Timing structure of the Physical Random Access CHannel (PRACH) and Acquisition Indicator Channel (AICH)24
3.1 | Random access algorithm
The random access procedure is an access request and an uplink synchronization protocol that is invoked whenever the
user equipment (UE) wants to use the resources offered by the node B for the first time or when a synchronization of the
node B receiver is needed.
The procedure is contention based and collision risk because it may be initiated by several UEs at the same time. In
this section, we describe the random access procedure (layers 1 and 2) in UMTS frequency division duplex mode, as
described in 3GPP specifications.4,23
The UE MAC sublayer is the responsible entity for any RACH transmissions. Initially, the MAC gets the RACH
transmission parameters (eg, set of available ASC [i, Pi], backoff intervals, and maximum number of preamble ramping
cycles Mmax) from higher layers.
As mentioned in the flow chart shown in Figure 2, The MAC sublayer picks up a couple (i, Pi) from the available set
of ASCs, depending on the type of the data to be transmitted.
The UE performs a “persistency check” based on the value of Pi to decide when to start the L1 transmission procedure of the PRACH (ie, which transmission time interval TTI).23 If the persistency condition is not satisfied, the transmission is suspended and another persistency check is scheduled in the following TTI. This step is repeated until the
satisfaction of the persistency condition that gives the permission to start the RACH transmission. Once the persistency
condition is satisfied, the PRACH transmission procedure (starting by defining the transmission power of the preamble)
is initiated by the MAC sublayer that sends a PHY‐ACCESS‐REQ to the physical layer. Then, the MAC sublayer waits for
a confirmation from L1 via PHY‐ACCESS‐CNF that contains access information.
The PRACH transmission starts by sending a preamble of a specific format, 1 of 16 possible sequences, that are
orthogonal, meaning that if 16 simultaneous transmissions are detected, the node B receiver can distinguish each of
them if they were different, but if 2 or more UEs send the same sequence, there is no way to distinguish between them
and a collision is occurred. To avoid such problem, a randomized algorithm is used to select 1 of these sequences
(signatures) and an ASC scheme is defined to attribute a group of physical resources (time slots) to each type of communication (ASC) in addition to the persistency check.
So, the procedure is initiated by the UE that sends a preamble by using the PRACH, which is a shared contention
based wireless channel, then it waits for a response from the node B that sends an ACK (acknowledgment) if it has
successfully detected the preamble sequence or it sends a NACK (negative ACK) when the detection is ambiguous. If
the UE receives an ACK end story (for L1 and L2), but if it receives a NACK, it waits for a backoff timer, then it
increments the transmitting power before performing a retransmission of the preamble; in case of a NACK or neither
ACK nor NACK, the procedure is repeated again for a predefined maximum number of retransmissions. More details
can be found in the attached flowchart.
5 of 18
Random Access Channel (RACH) transmission control procedure (user equipment [UE] side)4
UPPAAL30 (model checker) is a software tool used for modeling, simulation, verification, and validation of real‐time
systems. It is easy to use because it has a friendly graphical user interface and its input language can be learned very
rapidly because it uses a syntax similar to most programming languages. The tool is suitable for verifying bounded
proprieties of systems expressed as a network of timed automata or a collection of nondeterministic process communicating through shared variables and/or shared channels with clocks of real values and control structures. It is sufficiently
expressive to model communication protocols. It supports broadcast channels,25 which are needed for our model. This
motivates us to choose this particular tool to analyze our protocol.
In UPPAAL, a system is represented by finite state machines extended with clocks and data types (bounded integers,
arrays, etc) that form a network of communicating timed automata. The tool was developed by joint effort of the Swedish
6 of 18
Uppsala University and the Danish Aalborg University. It is free for noncommercial applications in academia only and
can be downloaded easily from UPPAAL.2
The main components of UPPAAL are a description language, a simulator, and a model checker. The description
language serves as a modeling language used to describe the behavior of the system as a network of timed automata that
supports the representation of clocks, data types (eg, bounded integers and arrays), and guarded commands. Used as a
validation tool, the simulator allows examination of some possible executions of the system in the earlier design phase;
this allows an inexpensive fault detection before the operation of verification by using model checker that exhaustively
checks the dynamic system behavior. The verification engine, “model checker” explores the full state space of a system to
perform reachability analysis to check the satisfaction of properties.2
The modeling language consists of an enhanced version of finite state machines “timed automata” that support clock
variables that are evaluated to real numbers and so they use a dense‐time model. All the clocks are progressing in a
synchronous manner. A network of such timed automata running in parallel is used to model a system in UPPAAL.
A further extension of the model is achieved by adding discrete bounded variables to the state. The variables are
manipulated like in an ordinary programming language (ie, read/written and arithmetic). For the whole system, a
system state is a combination of locations of all automata, current values of the clock, and the actual values of the
variables. A new state is achieved after a transition from one state to another for each automaton; this might be
performed in synchronization with another automaton or in independence.26
5.1 | Modeling the random access procedure using UPPAAL
To the best of our knowledge, this is the first PTA model for a slotted‐base access scheme protocol. The proposed model
consists of 3 timed automata that represent the phone “UE,” the base station “BTS,” and the channel.
5.1.1 | The channel
To model the PRACH, we use an automaton that generates a repetition of 15 time slots; these slots are considered as the
access slots described above.
As shown in Figure 3, the automaton has 2 committed states that move the control of the timing to the third state.
The “j” counter is used to increment the index of the current time slot and is rest to 0 once it reaches 15. An array of 15
broadcast channels (it[ts]) is used to synchronize the other automata with the current time slot. Instruction b: int[1, 16] is
used in the selection part of the edge to randomly pick up a number from 1 to 16, then the selected number is assigned to
the element of the current index in Sig_in_ts array that is used to simulate activities of other user in the network (i.g. for
instance Sig_in_ts [3] = 1 means that the third time slot is occupied by a transmission that uses the first signature). The
clock h and the invariant h < T are used to determine the time period of a time slot.
UPPAAL automaton of the channel
7 of 18
As the automaton goes back and forth from the even state to the odd state, it increments the time slot index until it
reaches 14, then the index is reset to 0.
5.1.2 | Simulation
Initially, the automaton is at the “reset” state, which is designated as “committed,” meaning that the state cannot delay
and the next transition must be taken. Then, the automaton set the variable “j” to 0 and moves to the “even” state, which
is also committed. Committed states are used here to move the control of the timing to the third state. Next, the automaton performs the following actions:
• Draw a random number from a uniform distribution “b:int[1, 16]” and assign “b” to the element of the array
“Sig_in_ts[ts]”; this array variable “Sig_in_ts” is used to indicate which signature is transmitted in the current time
slot. The main purpose of using such variable is to simulate transmissions by other users appearing at the same time.
• Increment the “j” counter (j++) simulates the time progress in units of time slots.
• Save the new index “j − 1” in the variable “ts.”
• Sets the clock “h” to 0 (h = 0) to initialize the duration of each time slot.
• After that, the automaton moves to the next state “odd” and wait until the clock “h” is greater or equal to “T” (the
invariant “h < T”); this is to fix the duration of the time slot.
• Then, it verifies if the index “ts” does not exceed the maximum number of time slots of the frame “ts < 14”; if so, it
moves to the state “even” and synchronizes with the broadcast channel array in the last index “it[ts].” This means
that the current time slot available for transmission is the one with index equal to “ts.”
If “ts ≥ 14,” the automaton synchronizes with the broadcast channel “it[ts]”; this is for the case of the last time slot of
the frame (ts = 14), then it reenters the initial state and repeats the same procedure.
The output of this automaton is a global variable “ts” that indicates the index of the current time slot and the array
Sig_in_ts that indicates which signature is currently transmitted by other users in the current time slot. Its main role is to
synchronize the whole system by using an array of broadcast channels.
5.1.3 | The base station
The base station's role is the reception of the random access preamble and the transmission of an ACK or NACK. The
automaton checks if the received signature is different from the one in the current time slot “Sig_in_ts[ts] = !sig[0]”;
if so, it responds with an ACK, else the reception is considered ambiguous; thus, the BTS sends a NACK. The last case
simulates the loss of the message “the base station does not receive anything” (see Figure 4).
5.1.4 | Simulation
At the beginning, this automaton is at its initial state named “listen.” When it receives a preamble “preamble [0]?,” it
randomly selects a number from 2 possible values (1 or 2) “r:[1, 2]” and saves the result in the variable “rn” before
moving to the state “BTS_React.” Then, if the random number “rn” is equal to “2,” the automaton moves to its initial
state; this simulates the case of message loss. But if the selected number is equal to “1,” the automaton checks the signature in the current time slot. If it is different from the one used by the UE “Sig_in_ts[ts] = !sig[0],” it replies with
an ACK message, meaning that the reception was successful, otherwise “Sig_in_ts[ts] == sig[0]”; it sends a NACK,
meaning that the reception is ambiguous due to a collision.
base station
UPPAAL automaton of the
8 of 18
5.1.5 | The user equipment
The user equipment is considered as the most important part of the random access procedure; thus, it is the most complicated probabilistic timed automata (PTA) in our model (Figure 5).
In our study, we will omit the role of the RRC, RLC, as well as the effect of the selection of a persistence value Pi from
a set ASC parameters, so we will fix its value to 50. This simplification leads to a worst‐case analysis.
Note that UPPAAL does not support real numbers; thus, we model the random process as a selection of a number
from a small margin 0 and 100 to reduce the effect of state space explosion.
The transition from the initial state sets p to 50 and initializes the number of retransmission “m” to 0, then it moves to
the next state (Rnd_select), from which the automaton picks up a number from a uniform distribution. Based on the comparison of this number with “p,” the UE decides whether to start the transmission in the present TTI (TTI = 15 time slots)
or not. If the randomly selected number is greater than p, the automaton waits for 1 TTI before restarting a new attempt.
If p is greater than the randomly selected number, the retransmission counter “M” is incremented and the transmission
power of the preamble Pw is increased, then the control is moved to “L1_PRACH_tr”; from this state, the automaton selects
an access slot from the first set of 8 AS “As_rnd: int[0, 7]” or in the last 7 As “As_rnd: int[8, 14]”; in 3GPP specifications, the
decision is based on information from RACH subchannels for a given ASC, which is omitted in this study for the sake of
simplicity. Then, it moves to “Signature_Selection” to select 1 signature from the set of up to 16 available signature “instruction sig [id] = sig_rnd” (once again, this is a simplification of the 3GPP specifications that defines a set of signatures “less
than 16” available for a given ASC). At the selected time slot (ts == As), the UE uses this signature to send a preamble
(instruction Pream[id]!). Then, the control is passed to the state “Wait_Pream_ACK” and waits for a response (ACK/NACK)
from the base station. If an ACK is received, the automaton passes to “access_sucess_Confirme_to_higher_layer_,” then it
proceeds to send the random access message and informs higher layer that the random access was succeeded.
But if it receives a NACK, a backoff timer TBO1 = NBO1 * 15 * ts is set. NBO1 is a randomly drawn number within an
interval 0 < NBO1min < NBO1 < NBO1max. After the expiration of this timer, the control is set back to “Rnd_select” to
restart a new random access procedure. If the number of retransmission exceeds the maximum allowed, the procedure is
considered as “failed” and a notification is sent to higher layer.
If neither ACK nor NACK is received, the automaton sets a timer T2 to 0, then it waits for 1 TTI (15 time slots
“[T2 ≥ 15 * T]”) to pass the control to “Rnd_select” and restart a new random access with an increment power.
UPPAAL automaton
modeling the user equipment (UE)
random access protocol
9 of 18
5.1.6 | Simulation
This automaton starts running from its initial state named “Start_RACH_Procedure.” It sets the persistency value “p” to
50 and the maximum transmission attempts “M” to 0, then it enters the “Rnd_Select” state. This one is urgent, meaning
that the state is left immediately. The automaton randomly selects a number “r_rnd:[1, 100]” from 0 to 100, assigns it to
the variable “r,” and sets the timer “T2” to 0, then it moves to the “Persistency_Check” state to compare the selected
number “r” with the persistency value “p.” If “p < r,” the timer “T2” is set to 0 and the automaton waits in the “persist”
state until T2 exceeds 15 times the duration of a time slot “T2 ≥ 15 * T” (ie, 1 radio frame), then it reenters the
“Rnd_Select” state. But if “p ≥ r,” the number of retransmissions is incremented “M = M + 1” as well as the transmission
power “pw = pw + pw_step” and the control is moved to the “L1PRACH_tr” state. If the maximum number of
retransmissions is reached “M > Mx,” the automaton moves to the exit state and the procedure is ended (ie, it simulates
the case of reporting maximum retransmissions reached to higher layers). But if “M ≤ Mx,” the automaton selects an
access slot from either the set of the first 8 access slots “As_rnd:int[0, 7]” or the last 7 access slots “As_rnd:int[8,14]”
of the radio frame (15 slots) and saves the result to the variable “As,” before giving the control to the state
“Signature_Selection.” This state is left only if a synchronization through the broadcast channel “it[As]” occurred, meaning that the current time slot is the one with index “As,” the exact time slot chosen by the automaton, then it randomly
selects a signature from the 16 possibilities “sig_rnd:int[1,16]” and assigns it to the signature of the “id” of the current UE
“sig[id] = sig_rnd.” Next, the automaton joins the state “Send_Preamble”; it sets the timer T2 to 0 and synchronizes with
channel “Pream[id]!”; this simulates the transmission of the preamble and moves to the state “Wait_Pram_Ack.” Here,
we distinguish 3 cases:
If a synchronization through the “Ack[id]” channel is detected, meaning that the UE receives an Ack from the base
station, the automaton reaches its final state “access_success_confirme_to_higher_layer_” and the procedure is considered successful.
If a synchronization through the “NAck[id]” channel is detected, meaning that the UE receives an NAck, the automaton draws a random number between the maximum and the minimum backoff numbers “nn:int[NBO1min,
NBO1max]” saves the result in the variable “NBO1,” sets the timer “TBO1” to 0, waits for a duration of 15 time slots
“T2 == 15 * T,” and moves to the “BackOff” state, then waits until the “TBO1” timer reaches NBO1 times radio frames
“TBO1 ≥ NBO1 * 15 * T,” then the automaton reenters the state “Rnd_select” to restart another attempt.
The last case is where neither Ack nor NAck is received. Here, the automaton moves from the “Wait_Pram_Ack”
state to the “No_Reply” state and waits for a period of 15 times the duration of a time slot “T ≥ 15 * T” before entering
the state “Rnd_select” and restarts another attempt.
5.2 | Using SPIN/PROMELA
SPIN simple PROMELA interpreter27 is a model checking tool widely used for formal verification. Its input language,
PROMELA, mainly designed for protocols and concurrent processes, has a syntax similar to an ordinary programming
language like C; thus, it offers more freedom to design the system model, but it did not support any timing concept,28
which limits its expressiveness.
Modeling the random access protocol by using PROMELA is not a trivial task because of the slotted nature of this
communication protocol; ie, the protocol sends in specific time periods, whereas the modeling language did not support
any representation of the time. To solve this limitation, we have used the solution proposed in Bosnacki and Dams28 to
represent the time in PROMELA.
Our model consists of 3 processes running in parallel (see Appendix A). The first one is used to handle the timers; it
consists of a simple do‐while loop. The second represents the base station RACH‐related functions, and the last one represents the random access algorithm as implemented in the UE side. For this one, we have used a finite state machine
extended with discrete time variables to implement the same model mentioned in Figure 5.
5.3 | Model checking properties
Model checking is an automatic technique used for both software and hardware system verification. Taking the system
model as input, the model checker engine performs an automatic satisfaction test for a given set of specifications
expressed as a temporal logical formula (LTL or CTL), which are not comparable because there exists LTL formulas with
no CTL equivalent and vice versa.
10 of 18
The tool may exhaustively explore the whole state space of the system model, to check the validity of the formula for
all cases. Both the model and the properties must be expressed in formal languages.
In UPPAAL, a simple version of CTL is used. The query language contains both state and path formulae; state
formula describes individual states, whereas path formula quantify over the paths or traces of the model. Path formula
can be classified into reachability, safety, and liveness types.
The query language defines 2 path quantifiers: “E = there exists a path” for seaking if the properiety holds in at least
one execution path and “A = in all the paths” to verify the formula in all possible execution paths.
As a path is composed out of states, we can verify the satisfaction of the formula in each state of the path by using the
symbol “[]” or if it is satisfied in at least one state using “<>.”
For SPIN, on the other hand, the verification could be done by inline assertions, LTL properties, progress‐state labels,
acceptance‐state labels, end‐state labels, or never‐claims. The original tool did not accept CTL formulas, although there
exists some research efforts to enhance its capability to support CTL.29 The tool provides many options such as a
nonexhaustive search and setting a limit for the memory use; these lead to an approximative result.
5.3.1 | Reachability properties
Reachability properties are the simplest form of properties and are used to determine whether a given state formula can
be satisfied by a reachable state.
P1: Can the protocol send a message?
For this context, we want to check if the protocol can send a message at all, so we use the following formal
E<>phon:Wait Pream ACK
which means that in the “UE” automaton, there exists at least 1 execution path that leads to the “Wait_Pream_ACK”
As we can see from the model in Figure 5, the automaton reaches the state “Wait_Pream_ACK” only after a transition coming from state “Send_Preamble” that synchronizes with the channel “Pream[id]” symbolizing the transmission
of a preamble. That is, the UE reaches this state after sending a preamble.
This property was satisfied.
Note that for the SPIN case, we cannot use CTL, and there exists no equivalent representation of the “E” path quantifier in LTL, so we can use another but close LTL formula: {<> (UE@Wait_Pram_Ack)} in the global scope; the tool has
proved that this property was not violated within the space limit of the memory of our machine.
P2: Can the protocol always succeed the attempt?
Once the automaton “UE” receives an acknowledgement from the base station “Ack[id]?,” it enters the state named
“phon.access_sucess_Confirme_to_higher_layer_” and the procedure is considered as succeeded, so formally, this property is expressed as “A<> phon.access_sucess_Confirme_to_higher_layer_,” which stands for, in all paths, the state
“phon.access_sucess_Confirme_to_higher_layer” is always reachable.
This was not satisfied, meaning that the protocol cannot always guarantee the success of the attempt. This is because
of eventual collisions and/or message losses due to radio conditions, which increments the retransmission attempts that
cause the abort of the procedure in case of exceeding the maximum allowed number. This can be interpreted as a drawback because the protocol fails to do its main job, but it can be an advantage in case of congestion; ie, if the network does
not support the access of all users, some of them do not succeed the random access and became silent for a period of
time, which reduces the congestion at the cost of increasing the access time delay for a restricted group of users.
In SPIN, this was checked using the LTL formula []UE@access_success_confirme_to_higher_layer_, which gives the
same result as UPPAAL.
P3: Can the protocol eventually succeed the attempt?
In this case, we modify the path quantifier of the precedent property. We get the formula “E<>phon.
access_sucess_Confirme_to_higher_layer_,” which means that there exists a path where somewhere in the future, the
state “access_sucess_Confirme_to_higher_layer_” is reachable, meaning that the transmission was successful. This propriety was satisfied.
11 of 18
As there is no representation of the “E” quantifier in LTL, in SPIN, we can use a close LTL formula to our property:
{[]<>UE@Start_RACH_Procedure ‐ > (<>UE@access_success_confirme_to_higher_layer_)}, which means that in any
execution where the UE starts the procedure infinitely often, it will eventually succeed the attempt. This claim was not
violated within the space limit of the memory of our machine.
The protocol uses a randomized algorithm extended with repeated retransmissions; thus, the transmission of the message “preamble” is not always guaranteed; it may take several retransmissions to succeed the random access procedure.
5.3.2 | Liveness properties
“Something will eventually happen.”
P4: Is the protocol collision free?
We want to check that 2 UEs never transmit the same signature at the same access slot, thus avoiding collision.
For this propriety, we have used a configuration with 2 instances of the “UE” automaton, running in parallel to represent the contention in accessing the channel.
The propriety is formalized as follows:
A<>ðphon:As ¼¼ phon1:AsÞ imply ðsig½0! ¼ sig½1Þ
It means that in all path globally, if the selected access slots “As” for transmission by both users “phon and phon1”
are the same, their signatures must be different “sig[0] ≠ sig[1],” thus avoiding collision (ie, if 2 users transmit at the
same time slot, their preambles must be distinguishable).
This propriety was not satisfied and the protocol cannot be collision free because it is based on a randomized access
scheme that can cause a simultaneous transmission from more than one UE.
For the model expressed in PROMELA/SPIN, we have introduced to the BTS process a local Boolean variable that is set
to “true” if a collision is detected in the current time slot, so to check if the protocol is collision free, we can just add a simple
assertion in the scope that processes assert (!collision[ts]). This was violated, which confirms the result found by UPPAAL.
P5: In case of no response, does the protocol increase the transmission power?
If neither an ACK nor NACK is received after the transmission of a preamble, the UE retransmits with higher power.
This property was satisfied and can be written as, E < > (phon . pw > 2 imply phon . No_Reply).
This is to say that when never the state “phon.No_Reply” is reached, the transmission power must be incremented.
The reachability of this state means that the “UE” did not receive any response.
It means that the UE is retransmitting with higher power (pw > 2) after a no reply from the BTS. This can happen in
a normal situation where the UE is far from the base station. In this case, the increase of the transmission power might
help to reach the base station. But this can cause problems if the UE is near the BS because the rise of power is not useful
but it increases interference in the cell (case of congestion).
In SPIN, we have used the LTL formula: {[]UE@No_Reply<‐>UE:pw > 0}, which means that the UE increments its
power before retransmitting the preamble only in the case of no response from the base station. The property was satisfied.
Table 2 summarizes the results with their processing time and memory consumption by using the academic version
of UPPAAL v4.1.19 and SPIN v6.4.6 installed in Ubuntu 64 bits, running over a machine with 4 GB RAM and processor
Intel i7 2.7 GHz (4 CPUs).
Results of the verification experiments
0.001 s
53,164 KB
120 s
0.013 s
75,704 KB
~0.0 s
5.882 s
575,256 KB
28.7 s
0.011 s
76,792 KB
~0 s
662,253 KB
0.002 s
42,436 KB
~0 s
662,253 KB
3,071,991 KB
128,730 KB
3,071,921 KB
12 of 18
Although we get a reasonable execution time for certain properties, we were limited by the state space explosion problem
for other properties, eg, the dead lock which was not possible to verify for both tools.
As we can see from Table 1, SPIN consumes more memory than UPPAAL, and its input language, PROMELA, offers
more freedom for modeling the system; thus, it provides more realistic and accurate specification than that of UPPAAL,
which supports only PTAs. UPPAAL, on the other hand, is easier to learn and use because it comes with a friendly GUI,
which is an efficient way to design and check the validity of the model. It supports time and broadcast channels. This
makes it suitable for real time applications and protocols like the one discussed in this paper.
In this paper, a new PTA‐based model of the random access procedure in cellular networks has been proposed. The study
concludes that the UMTS random access procedure is still far from perfection because this protocol cannot ensure the
transmission of the message in all cases. It is a collision risk and suffers from the near far problem. In case of congestion,
the UE may fail to access the network but the protocol continues unnecessarily to send preambles even with higher
power, which increases the cell interference and thus leads to a degradation of the quality of service in the whole system.
With only 16 signatures, this protocol has a very limited number of simultaneous access; thus, it is not suitable for
large networks. Although the LTE (4G) has 64 signatures, it uses a similar random access scheme and thus suffers from
the same problems. This is why a new protocol is very necessary because the number of users will be much higher for the
next generation mobile networks (5G and beyond) where an era of the internet of things is emerging.
We conclude also that applying model checking to this kind of channels is quite challenging, due to the slotted access
scheme of the radio channels used in modern cellular technologies, which requires a careful synchronization of each
timed automaton in the model. Extending the model checker engine with such type of channel will be a good starting
point for future works.
Ahmed Roumane
1. Baier C, Katoen J‐P. Principles of Model Checking. Massachusetts London, England: The MIT Press Cambridge; 2008.
2. “UPPAAL,” [Online]. Available: [Accessed September 2015].
3. “Spin,” [Online]. Available: [Accessed 2017].
4. 3GPP TS 25.321,, “Medium Access Control (MAC) protocol specification,” V12.0.0, 2014.
5. 3GPP TS 25.214, “Physical layer procedures (FDD),” Release 12, 2014‐09.
6. Mokadem HB, Bérard B, Gourcuff V, De Smet O, Roussel J‐M. Verification of a timed multitask system with UPPAAL. IEEE Transactions
on automation science and engineering. 2010;7(4):921‐932.
7. Kartal YB, Schmidt EG, Schmidt KW. Modeling distributed real‐time systems in TIOA and UPPAAL. ACM Transactions on embedded computing systems. 2016;16(1):1‐26.
8. Chen H, Wu XN, Shao Z, Lockerman J, Gu R, “Toward compositional verification of interruptible OS kernels and device drivers,” in Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation, Santa Barbara, CA, USA, 2016.
9. Avalle M, Pironti A, Sisto R. Formal verification of security protocol implementations: a survey. Formal Aspects of Computing.
10. Hammal Y, Ben‐Othman J, Mokdad L, Abdelli A. Formal modeling and verification of an enhanced variant of the IEEE 802.11 CSMA/CA
11. Ruiz MC, Macia H, Mateo JA, Calleja J. Formal analysis of an energy‐aware collision resolution protocol for wireless sensor networks.
Procedia Computer Science. 2016;80:1191‐1201, 2.
12. Saghar M, Kashif AM, Farooq T. Application of formal methods for validation and verification of embedded system communication
protocol, in In 13th International Bhurban Conference on Applied Sciences and Technology (IBCAST), Islamabad, Pakistan, 2016.
13 of 18
13. Pan C, Guo J, Zhu L, Shi J, Zhu H, Zhou X. Modeling and verification of CAN Bus with application layer using UPPAAL. Electronic Notes
in Theoretical Computer Science. 2014;309:31‐49.
14. Rashid A, Hasan O, Saghar K. Formal analysis of a ZigBee‐based routing protocol for smart grids using UPPAAL, in 12th International
Conference on High‐Capacity Optical Networks and Enabling/Emerging Technologies (HONET), Islamabad, Pakistan, 2015.
15. Ansgar Fehnker, Rob Van Glabbeek, Peter Hofner, Annabelle McIver, Marius Portmann, Wee Lum Tan, “Automated analysis of AODV
using UPPAAL,” Tools and algorithms for the construction and analysis of systems (LNCS), vol. 7214, pp. 173‐187, 2012.
16. Chiyangwa S, Kwiatkowska M. A timing analysis of AODV. In: Formal Methods for Open Object‐Based Distributed Systems. Berlin, Heidelberg: Springer; 2005:306‐321.
17. Eidgahi ZS, Rafe V. Security analysis of network protocols through model checking: a case study on mobile IPv6. Security and
communication networks. 2016;9:1072‐1084.
18. Vattakunnel AJ, Suresh Kumar N, Santhosh Kumar G. Modelling and verification of CoAP over routing layer using SPIN model checker.
Procedia Computer Science. 2016;93:299‐308.
19. Sik BW. Formal verification of an RFID authentication protocol based on hash function and secret code. Wireless Personal
Communications, Springer. 2014;79(4):2595‐2609.
20. Bae W‐S. Designing and verifying a P2P service security protocol in M2M environment. Peer‐to‐Peer Networking and Applications, Springer.
21. Veena B, Sachin K. Survey of network protocol verification techniques. International Journal of Scientific and Research Publications.
22. Qadir J, Hasan O. Applying formal methods to networking: theory, techniques, and applications. IEEE Communications Surveys &
Tutorials. 2015;17(1):256‐291.
23. 3GPP TS 25.214, “Physical layer procedures (FDD),” V12.0.0, 2014‐09.
24. Niththiyanathan J. Performance analysis of the random access procedure in WCDMA, Nokia,” 23 November 2002. [Online]. Available: Accessed September 2015
25. Fatima T, Saghar K, Ihsan A. Evaluation of model checkers spin and Uppaal for testing wireless sensor network routing protocols, in 12th
International Bhurban Conference on Applied Sciences & Technology Islamabad,(IBCAST 2015), Islamabad, Pakistan, 2015.
26. Behrmann G, David A, Larsen KG. A tutorial on Uppaal 4.0, 28 November 2006. [Online]. Available:
anvandarfiler/filer/uppaal‐tutorial.pdf. [Accessed September 2015].
27. [Online]. Available: [Accessed 2017].
28. Bosnacki D, Dams D. Integrating real time into spin: a prototype implementation, in FORTE/PSTV XVIII Conference, Kluwer, 1998.
29. Visser W, Barringer H. CTL* model checking for SPIN, Software Tools for Technology Transfer, LNCS, 1999.
30. UPPSALA, AALBORG, [Online]. Available: [Accessed 23 march 2016].
How to cite this article: Roumane A, Kechar B, Kouninef B. Formal verification of a radio network random
access protocol. Int J Commun Syst. 2017;e3447.
/*discrete time macros*/
#define timer int
#define set(x,y) x=y
#define expire(x) (x==0)
#define tick(x) if :: x>=0->x=x-1; :: else; fi
#define ts_tick(x) if :: x==0 ‐> set(x,14); :: else if :: x>=0‐>x=x-1; :: else; fi; fi;
/* ts_tick is the function that makes the time slot progress */
14 of 18
#define on(x) (x!=-1)
#define delay(x,y) set(x,y); expire(x);
#define udelay(x) do :: delay(x,1) :: break od
#define N 4 /*The number of UE*/
#define DEBUG
#define DEBUG_MSG
chan Ack[15]
= [0] of {bit};
chan NAck[15]
= [0] of {bit};
chan Pream[15] = [0] of {byte, byte};
/*ltl p1 { < > (UE@Wait_Pram_Ack)} Can the protocol send a message?*/
/*ltl p2 {[]UE@access_success_confirme_to_higher_layer_} Can the protocol always succeed the attempt?*/
/*ltl p3 {[]< >UE@Start_RACH_Procedure ‐> (< >UE@access_success_confirme_to_higher_layer_)} In any execution
where the UE starts the procedure infinitely often, it will eventually get succeed the attempt?*/
/* ltl p4 {[]!(BTS:collision[ts])} is the protocol collision free*/
/*ltl p5 {[]UE@No_Reply<‐>UE:pw >0} In case of no response, does the protocol increase the transmission power, yes
memory = 662253KB*/
/* timers */
timer ts, tt[N], T2[N], T3[N], TBO1[N];
proctype Timers()
byte i;
:: timeout ‐>
/*Repeatdly decrement all timers by one whenever there is no executable instruction*/
#ifdef DEBUG
printf("Current Ts: %d \n" , ts);
do :: i<N ‐> tick(tt[i]); tick(T2[i]); tick(T3[i]); tick(TBO1[i]);
#ifdef DEBUG
printf("TIMERS tt[%d]: %d, T2[%d]: %d, T3[%d]: %d, TBO1[%d]: %d \n", i, tt[i], i, T2[i], i, T3[i], i, TBO1[i] );
:: else; break; od;
active [N] proctype UE()
/* The User Equipment model*/
/* A finite state machine is used*/
#ifdef DEBUG
printf("\n \n ....... UE N° %d is running at ts: %d ", _pid, ts);
byte p,M,Mx=3, pw=0, pw_step=1, pw_max=4, r, As, sig, NBO1;
bool succeeded=false;
#ifdef DEBUG
printf("\n \n ....... UE N°: %d is in state : Start_RACH_Procedure at %d", _pid, ts);
p= 5;
goto ChooseRnd;
if :: M>Mx ‐> goto exit; :: else skip; fi;
#ifdef DEBUG
printf("\n \n ....... UE N°: %d is in state : ChooseRnd at %d", _pid, ts);
select(r : 1 .. 10);
set(T2[_pid], 15);
goto Persistency_Check;
if :: M>Mx ‐> goto exit; :: else skip; fi;
#ifdef DEBUG
printf("\n \n ....... UE N°: %d is in state : Persistency_Check at %d", _pid, ts);
if :: p<r ‐> goto Persist;
:: p >= r ‐> M=M+1;
goto L1PRACH_tr;
#ifdef DEBUG
printf("\n \n ....... UE N°: %d is in state : Persist at %d T2 : %d", _pid, ts, T2[_pid]);
if :: (expire(T2[_pid])) ‐> goto ChooseRnd; else; fi;
#ifdef DEBUG
printf("\n \n ....... UE N°: %d is in state : L1PRACH_tr at %d", _pid, ts);
if :: M>Mx ‐> goto exit;
:: else ‐>
:: select(As : 0..7); break;
:: select(As : 8 .. 14); break;
goto Signature_Selection;
#ifdef DEBUG
printf("\n \n ....... UE N°: %d is in state : Signature_Selection at %d", _pid, ts);
select(sig : 1..16);
goto Send_Preamble;
#ifdef DEBUG
printf("\n \n ....... UE N°: %d is in state : Send_Preamble at %d", _pid, ts);
printf("\n \n ....... UE N°: %d ts: %d, As: %d", _pid, ts, As);
if :: ts>As ‐> set(tt[_pid],ts-As);
:: ts<As ‐> set(tt[_pid], ts+15-As);
:: else ‐> set(tt[_pid],0);
15 of 18
16 of 18
#ifdef DEBUG
printf("tt is set to %d \n", tt[_pid] );
#ifdef DEBUG
printf(" \n expire tt, ts: %d = As: %d", ts, As);
printf("\n \n ....expire(tt: %d)... UE N°: %d ts: %d, As: %d", tt[_pid], _pid, ts, As);
Pream[As]!sig, _pid;
#ifdef DEBUG_MSG
printf("\n \n ....... UE N°:%d Sends the preamble: %d at ts: %d, = As: %d", _pid, sig, ts, As);
goto Wait_Pram_Ack;
#ifdef DEBUG
printf("\n \n ....... UE N°: %d is in state : Wait_Pram_Ack at %d", _pid, ts);
if :: Ack[_pid]?1 ‐>
#ifdef DEBUG_MSG
printf("\n \n ....... UE N°: %d is receiving Ack at %d", _pid, ts);
goto access_success_confirme_to_higher_layer_;
:: NAck[_pid]?1 ‐> select(NBO1 : 2..3);
#ifdef DEBUG_MSG
printf("\n \n ....... UE N°: %d is receiving NAck at %d \n T3 is %d ", _pid, ts, T3[_pid]);
delay(T3[_pid], 15);
set (TBO1[_pid], NBO1*15);
goto BackOff;
else ‐>
#ifdef DEBUG_MSG
printf("\n \n ....... UE N°: %d didn't get NAck or Ack at %d", _pid, ts);
if ::pw< pw_max ‐> pw=pw+pw_step; else skip; fi;
goto No_Reply;
delay(T3[_pid], 15);
goto ChooseRnd;
#ifdef DEBUG
printf("\n \n ....... UE N°: %d is in state : BackOff at %d", _pid, ts);
goto ChooseRnd;
#ifdef DEBUG
printf("\n \n ....... UE N°: %d is in state : exit at %d", _pid, ts);
goto Start_RACH_Procedure;
17 of 18
#ifdef DEBUG
printf("\n \n ....... UE N°: %d is in state : access_success_confirme_to_higher_layer_ at %d", _pid, ts);
goto Start_RACH_Procedure;
active [1] proctype BTS()
byte id, seq, i=0, j=0, k;
bool collision[15]=false;
#ifdef DEBUG
printf("\n \n ::::::::::: BTS N° %d is running at ts: %d", _pid, ts);
i=0; j=0; k=0;
:: k<14 ‐> collision[k]=false; k++;
/* printf("\n \n ************* BTS N° %d is init collision at ts: %d", _pid, ts);*/
:: else ‐> break;
#ifdef DEBUG
printf("\n \n :::::::::::: BTS N° %d is waiting for preamble at ts: %d", _pid, ts);
:: Pream[ts]?seq, id ->
#ifdef DEBUG_MSG
printf("\n \n ::::::::::: BTS N° : %d is receiving Preamble: %d from UE: %d at \n ts: %d", _pid, seq, id, ts);
/*Detecting collision in each time slot*/
:: j<N ‐> i=0;
::(i<j) ‐> collision[UE[i]:As] = collision[UE[i]:As] || ((UE[i]:As == UE[j]:As)
#ifdef DEBUG
printf("\n \n :*****#:#:#:#:#*** \n i: %d, j: %d :::::: Collision is %d, at ts: %d \n , UE[i]:As : %d , UE[j]:As %d,
UE[i]:sig %d, UE[j]:sig %d \n ", i, j, collision[UE[i]:As], ts, UE[i]:As, UE[j]:As, UE[i]:sig, UE[i]:sig);
:: else ‐> break;
:: else ‐> break;
#ifdef DEBUG
printf("\n \n ::::::::::: Collision is %d, at ts: %d \n",collision[ts], ts );
if :: collision[ts] ‐> NAck[id]!1;
#ifdef DEBUG_MSG
printf("\n \n :::::::::::: BTS N° %d is sending NAck to UE: %d at ts: %d", _pid, id, ts);
18 of 18
goto s;
:: !collision[ts] ‐> Ack[id]!1;
#ifdef DEBUG_MSG
printf("\n \n :::::::::::: BTS N° %d is sending Ack to UE: %d at ts: %d", _pid, id, ts);
goto s;
goto s;
init {
run Timers();
Без категории
Размер файла
590 Кб
3447, dac
Пожаловаться на содержимое документа