1.
Formalna verifikacija predajne procedure mobilnega omrežja v okolju TLA+ ToolboxRok Vogrin, 2015, diplomsko delo
Opis: 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.
Ključne besede: formalna specifikacija, temporalna logika akcij, preverjanje modelov, varnost, živost
Objavljeno: 14.10.2015; Ogledov: 785; Prenosov: 81
Celotno besedilo (1,95 MB)
