diplomsko delo
Rok Vogrin (Avtor), Tatjana Kapus (Mentor)

Povzetek

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;

Podatki

Jezik: Slovenski jezik
Leto izida:
Tipologija: 2.11 - Diplomsko delo
Organizacija: UM FERI - Fakulteta za elektrotehniko, računalništvo in informatiko
Založnik: R. Vogrin
UDK: 004.432.2:004.7(043.2)
COBISS: 19297046 Povezava se bo odprla v novem oknu
Št. ogledov: 1007
Št. prenosov: 93
Ocena: 0 (0 glasov)
Metapodatki: JSON JSON-RDF JSON-LD TURTLE N-TRIPLES XML RDFA MICRODATA DC-XML DC-RDF RDF

Ostali podatki

Sekundarni jezik: Angleški jezik
Sekundarni naslov: Formal verification of a mobile network handover procedure by using TLA+ Toolbox
Sekundarni povzetek: 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.
Sekundarne ključne besede: formal specification;temporal logic of actions;model checking;safety;liveness;
URN: URN:SI:UM:
Vrsta dela (COBISS): Diplomsko delo/naloga
Komentar na gradivo: Univ. v Mariboru, Fak. za elektrotehniko, računalništvo in informatiko, Telekomunikacije
Strani: IV, 41 f.
ID: 8890173