Automatska verifikacija protokola s vremenskim ograničenjima

završni rad

• Naslov (engleski): Model Checking of Protocols with Time Constraints
• Autor: Davor Lisjak
• Mentor: Dario Krešić (mentor); MBZ: 306050
• Član povjerenstva: Nikola Ivković; MBZ: 306480
• Ustanova koja je dodijelila akademski / stručni stupanj: Sveučilište u Zagrebu; Fakultet organizacije i informatike; (Katedra za informatičke tehnologije i računarstvo); Varaždin
• Datum i država obrane: 2012-09-27, Hrvatska
• Znanstveno / umjetničko područje, polje i grana: DRUŠTVENE ZNANOSTI; Informacijske i komunikacijske znanosti; Organizacija i informatika

Sažetak

Automatska verifikacija protokola podrazumijeva algoritamski definiran postupak provjere da li zadani model protokola ispunjava neko traženo svojstvo (npr. "Svaka poslana poruka mora biti potvrđena"). Budući da komunikacijski protokoli u pravilu uključuju i vremenski aspekt (npr. "Primatelj poruke treba poslati potvrdu o primitku poruke unutar vremena t"), prikladno je protokole modelirati pomoću tzv. vremenskih automata (engl. timed automata) koji omogućuju direktnu specifikaciju vremenskih parametara. Za automatsku verifikaciju vremenskih automata korišten je Uppaal, verifikator razvijen na Swedish Institute of Computer Science (SICS). U ovom („praktično“ usmjerenom) radu model Go-Back-N ARQ protokol preveden je u Uppaal-ov specifikacijski jezik te analiziran s obzirom na različita svojstva.

• Ključne riječi: vremenski automati; automatska verifikacija; protokoli; uppaal
• Jezik: hrvatski
• URN:NBN: urn:nbn:hr:211:244198
• Studijski program: Naziv: Informacijski sustavi; Vrsta studija: sveučilišni; Stupanj studija: preddiplomski; Akademski / stručni naziv: sveučilišni/a prvostupnik/prvostupnica (baccalaureus/baccalaurea) informatike (univ.bacc.inf.)
• Vrsta resursa: Tekst
• Način izrade datoteke: Izvorno digitalna
• Prava pristupa: Pristup korisnicima matične ustanove
• Datum i vrijeme pohrane: 2017-01-26 11:16:00