| Title: | Formalna verifikacija predajne procedure mobilnega omrežja v okolju TLA+ Toolbox |
|---|
| Authors: | ID Vogrin, Rok (Author)
ID Kapus, Tatjana (Mentor) More about this mentor...  |
|---|
| Files: |  UN_Vogrin_Rok_2015.pdf (1,95 MB)
MD5: B34F61A17B1D3D1038DD2BC83E4B4E5B
|
|---|
| Language: | Slovenian |
|---|
| Work type: | Bachelor thesis/paper |
|---|
| Typology: | 2.11 - Undergraduate Thesis |
|---|
| Organization: | FERI - Faculty of Electrical Engineering and Computer Science
|
|---|
| 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 |
|---|
| Place of publishing: | [Maribor |
|---|
| Publisher: | R. Vogrin |
|---|
| Year of publishing: | 2015 |
|---|
| PID: | 20.500.12556/DKUM-54693 |
|---|
| UDC: | 004.432.2:004.7(043.2) |
|---|
| COBISS.SI-ID: | 19297046 |
|---|
| NUK URN: | URN:SI:UM:DK:RA6O8COG |
|---|
| Publication date in DKUM: | 14.10.2015 |
|---|
| Views: | 1857 |
|---|
| Downloads: | 133 |
|---|
| Metadata: |    |
|---|
| Categories: | KTFMB - FERI
|
|---|
|
:
|
Copy citation |
|---|
| | | | Average score: | (0 votes) |
|---|
| Your score: | Voting is allowed only for logged in users. |
|---|
| Share: |  |
|---|
Hover the mouse pointer over a document title to show the abstract or click
on the title to get all document metadata. |
