| | SLO | ENG | Piškotki in zasebnost

Večja pisava | Manjša pisava

Izpis gradiva

Naslov:Formalna verifikacija predajne procedure mobilnega omrežja v okolju TLA+ Toolbox
Avtorji:Vogrin, Rok (Avtor)
Kapus, Tatjana (Mentor) Več o mentorju... Novo okno
Datoteke:.pdf UN_Vogrin_Rok_2015.pdf (1,95 MB)
MD5: B34F61A17B1D3D1038DD2BC83E4B4E5B
 
Jezik:Slovenski jezik
Vrsta gradiva:Diplomsko delo/naloga (mb11)
Tipologija:2.11 - Diplomsko delo
Organizacija:FERI - Fakulteta za elektrotehniko, računalništvo in informatiko
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
Leto izida:2015
Založnik:R. Vogrin
Izvor:[Maribor
UDK:004.432.2:004.7(043.2)
COBISS_ID:19297046 Novo okno
NUK URN:URN:SI:UM:DK:RA6O8COG
Število ogledov:785
Število prenosov:81
Metapodatki:XML RDF-CHPDL DC-XML DC-RDF
Področja:KTFMB - FERI
:
  
Skupna ocena:(0 glasov)
Vaša ocena:Ocenjevanje je dovoljeno samo prijavljenim uporabnikom.
Objavi na:AddThis
AddThis uporablja piškotke, za katere potrebujemo vaše privoljenje.
Uredi privoljenje...

Postavite miškin kazalec na naslov za izpis povzetka. Klik na naslov izpiše podrobnosti ali sproži prenos.

Sekundarni jezik

Jezik:Angleški jezik
Naslov:Formal verification of a mobile network handover procedure by using TLA+ Toolbox
Opis: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.
Ključne besede:formal specification, temporal logic of actions, model checking, safety, liveness


Komentarji

Dodaj komentar

Za komentiranje se morate prijaviti.

Komentarji (0)
0 - 0 / 0
 
Ni komentarjev!

Nazaj
Logotipi partnerjev Univerza v Mariboru Univerza v Ljubljani Univerza na Primorskem Univerza v Novi Gorici