| Naslov: | Formalna verifikacija predajne procedure mobilnega omrežja v okolju TLA+ Toolbox |
|---|
| Avtorji: | ID Vogrin, Rok (Avtor)
ID Kapus, Tatjana (Mentor) Več o mentorju...  |
|---|
| Datoteke: |  UN_Vogrin_Rok_2015.pdf (1,95 MB)
MD5: B34F61A17B1D3D1038DD2BC83E4B4E5B
|
|---|
| Jezik: | Slovenski jezik |
|---|
| Vrsta gradiva: | Diplomsko delo/naloga |
|---|
| 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 |
|---|
| Kraj izida: | [Maribor |
|---|
| Založnik: | R. Vogrin |
|---|
| Leto izida: | 2015 |
|---|
| PID: | 20.500.12556/DKUM-54693 |
|---|
| UDK: | 004.432.2:004.7(043.2) |
|---|
| COBISS.SI-ID: | 19297046 |
|---|
| NUK URN: | URN:SI:UM:DK:RA6O8COG |
|---|
| Datum objave v DKUM: | 14.10.2015 |
|---|
| Število ogledov: | 1854 |
|---|
| Število prenosov: | 133 |
|---|
| Metapodatki: |    |
|---|
| Področja: | KTFMB - FERI
|
|---|
|
:
|
Kopiraj citat |
|---|
| | | | Skupna ocena: | (0 glasov) |
|---|
| Vaša ocena: | Ocenjevanje je dovoljeno samo prijavljenim uporabnikom. |
|---|
| Objavi na: |  |
|---|
Postavite miškin kazalec na naslov za izpis povzetka. Klik na naslov izpiše
podrobnosti ali sproži prenos. |
