Formalna verifikacija predajne procedure mobilnega omrežja v okolju TLA+ ToolboxVogrin, Rok (Avtor) Kapus, Tatjana (Mentor) formalna specifikacijatemporalna logika akcijpreverjanje modelovvarnostživostV 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.R. Vogrin20152015-09-09 19:28:12Diplomsko delo/naloga54693UDK: 004.432.2:004.7(043.2)COBISS_ID: 19297046NUK URN: URN:SI:UM:DK:RA6O8COGsl