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

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;

Data

Language: Slovenian
Year of publishing:
Typology: 2.11 - Undergraduate Thesis
Organization: UM FERI - Faculty of Electrical Engineering and Computer Science
Publisher: R. Vogrin
UDC: 004.432.2:004.7(043.2)
COBISS: 19297046 Link will open in a new window
Views: 1007
Downloads: 93
Average score: 0 (0 votes)
Metadata: JSON JSON-RDF JSON-LD TURTLE N-TRIPLES XML RDFA MICRODATA DC-XML DC-RDF RDF

Other data

Secondary language: English
Secondary title: Formal verification of a mobile network handover procedure by using TLA+ Toolbox
Secondary abstract: 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.
Secondary keywords: formal specification;temporal logic of actions;model checking;safety;liveness;
URN: URN:SI:UM:
Type (COBISS): Bachelor thesis/paper
Thesis comment: Univ. v Mariboru, Fak. za elektrotehniko, računalništvo in informatiko, Telekomunikacije
Pages: IV, 41 f.
ID: 8890173