1.
Formalna verifikacija predajne procedure mobilnega omrežja v okolju TLA+ ToolboxRok Vogrin, 2015, undergraduate thesis
Abstract: 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.
Keywords: formalna specifikacija, temporalna logika akcij, preverjanje modelov, varnost, živost
Published in DKUM: 14.10.2015; Views: 1670; Downloads: 121
Full text (1,95 MB)
