Bakalářská práce

Verifikace protokolu AMQP

Verification of AMQP Protocol

Barbora Vaššová
Anotace

Cieľom tejto práce je formálne verifikovať niektoré vlastnosti AMQP protokolu. Tento protokol je formálne popísaný a modelovaný v jazyku DVE. Požadované vlastnosti, zamerané na spoľahlivosť protokolu, sú formulované pomocou lineárnej temporálnej logiky. Pri samotnej verfikácii bol použitý DiVinE model checker, keďže plne podporuje verifikácu modelov napísaných v jazyku DVE aj verifikáciu vlastností napísaných v LTL.

Abstract

The aim of this thesis is to formally verify some properties of the AMQP protocol. This protocol is formally described and modeled in DVE language. The required properties, focused on reliability of the protocol, are formulated with the help of linear temporal logic. In order to verify the created model, the DiVinE model checker is used, since it fully suports both verification of models written in DVE language and verification of properties written in LTL.

Klíčová slova
AMQP model checking verification DVE DiVinE linear temporal logic
Zadání práce
Práce má za cíl provést formální verifikaci protokolu AMQP 1.0 (www.amqp.org). Tento protokol se stává standardním otevřeným protokolem aplikační vrstvy pro zasílání zpráv mezi distribuovanými systémy (Message-Oriented Middleware). Protokol nabízí některé zajímavé vlastnosti, jako je například garance doručení zprávy právě jednou, které ale nikdy nebyly formálně dokázány. V rámci své práce student formálně popíše protokol ve vhodném modelovacím jazyce, popíše vybrané vlastnosti protokolu ve vhodné temporální logice typu LTL, a ověří platnost vlastností na daném modelu ve zvoleném nástroji pro formální verifikaci.
Administrativní informace
Práce zkontrolována:
19. 5. 2015 11:24, prof. RNDr. Jiří Barnat, Ph.D., učo 3496
Plný text práce
431,6 KB / soubor PDF
Přílohy (2)
Jazyk práce
angličtina angličtina
Termín obhajoby
19. 6. 2015
Práce byla úspěšně obhájena

Vedoucí

prof. RNDr. Jiří Barnat, Ph.D., učo 3496
KTP FI MU

Oponent

prof. RNDr. Luboš Brim, CSc.
abs PřF MU

Konzultant

Mgr. Pavel Moravec, Ph.D., učo 39589
abs FI MU
Citovat tuto práci
Masarykova univerzita Fakulta informatiky
Studijní program
Informatika
Obor

Práce na příbuzné téma

Seznam prací, které mají shodná klíčová slova.

Podobné práce
 
Název
Vložil
Vloženo
Práva
Archiv závěrečné práce Barbora Vaššová FI B-IN PSK ook9k/8
Pekárková, L.
8. 4. 2015
Složky
Soubory
Anotace anglicky annotation_english.txt
Vaššová, B.
17. 5. 2015
Anotace česky annotation.txt
Vaššová, B.
17. 5. 2015
Klíčová slova keywords.txt
Vaššová, B.
17. 5. 2015
Plný text práce BachelorThesis.pdf
Vaššová, B.
17. 5. 2015
Posudek oponenta r_vassova.pdf
Brim, L.
2. 6. 2015
Posudek vedoucího vassova.pdf
Barnat, J.
28. 5. 2015
Příloha model.dve
Vaššová, B.
17. 5. 2015
Příloha model.ltl
Vaššová, B.
17. 5. 2015

  • Přidání souboru

    Soubor nebo složku lze nahrát pomocí tlačítka Přidat.

  • Další operace se soubory

    Podrobnosti lze zjistit označením příslušného řádku.

  • Pohled pro experty

    Pro častou práci je možné zvolit režim Více možností.

  • Vyhledávání souborů

    Vyhledávaný výraz můžete zadat přímo do adresního řádku.

  • Rychlý přístup k souborům

    Pomocí funkce Nedávné je možné se rychle vrátit k právě prohlíženým souborům. Oblíbené soubory je také možné označit Hvězdičkou.