Formal verification of a mobile network handover procedure by using TLA+ Toolbox

V mobilnih komunikacijskih omrežjih mobilne postaje med komunikacijo prehajajo iz ene celice v drugo, tako da skupaj z omrežjem izvajajo predajno proceduro. Namen tega dela je formalno specificirati predajno proceduro v formalnem jeziku TLA$^+$ v okolju TLA$^+$ Toolbox in s preverjalnikom modelov TLC avtomatično preveriti, ali deluje v skladu z našimi pričakovanji. Predstavljena je temporalna logika akcij, ki je osnova za opisovanje našega sistema. Navedene so glavne značilnosti in funkcije okolja TLA$^+$ Toolbox ter jezika TLA$^+$. Sledi neformalen opis procedure in razlaga formalne specifikacije, ki smo jo pripravili na njegovi podlagi. Formalno so verificirane pomembne varnostne in živostne lastnosti specificiranega sistema.In mobile communications networks, mobile stations move from one cell to another during the communication by executing a handover procedure in cooperation with the network. The purpose of this thesis is to formally specify a handover procedure in formal language TLA$^+$ by using the TLA$^+$ Toolbox environment and to automatically verify whether the procedure works in accordance with our expectations by using model checker TLC. The temporal logic of actions, which is the basis for specifying our system, is presented. The main characteristics and functions of the TLA$^+$ Toolbox and TLA$^+$ are given. An informal description of the procedure as well as an explanation of a formal specification which we prepared based on the description are written. Important safety and liveness properties of the specified system are formally verified