prikaz prve stranice dokumenta Formalna verifikacija softvera metodom provjere modela
  Preuzmi
PDF 1.8 MB
diplomski rad
Formalna verifikacija softvera metodom provjere modela
Zagreb: Sveučilište u Zagrebu, Prirodoslovno-matematički fakultet, 2019. urn:nbn:hr:217:098202
Lešić, Klara
Sveučilište u Zagrebu
Prirodoslovno-matematički fakultet
Matematički odsjek

Institucijski repozitorij: Repozitorij Prirodoslovno-matematičkog fakulteta

Citirajte ovaj rad

Lešić, K. (2019). Formalna verifikacija softvera metodom provjere modela (Diplomski rad). Zagreb: Sveučilište u Zagrebu, Prirodoslovno-matematički fakultet. Preuzeto s https://urn.nsk.hr/urn:nbn:hr:217:098202

Lešić, Klara. "Formalna verifikacija softvera metodom provjere modela." Diplomski rad, Sveučilište u Zagrebu, Prirodoslovno-matematički fakultet, 2019. https://urn.nsk.hr/urn:nbn:hr:217:098202

Lešić, Klara. "Formalna verifikacija softvera metodom provjere modela." Diplomski rad, Sveučilište u Zagrebu, Prirodoslovno-matematički fakultet, 2019. https://urn.nsk.hr/urn:nbn:hr:217:098202

Lešić, K. (2019). 'Formalna verifikacija softvera metodom provjere modela', Diplomski rad, Sveučilište u Zagrebu, Prirodoslovno-matematički fakultet, citirano: 11.01.2025., https://urn.nsk.hr/urn:nbn:hr:217:098202

Lešić K. Formalna verifikacija softvera metodom provjere modela [Diplomski rad]. Zagreb: Sveučilište u Zagrebu, Prirodoslovno-matematički fakultet; 2019 [pristupljeno 11.01.2025.] Dostupno na: https://urn.nsk.hr/urn:nbn:hr:217:098202

K. Lešić, "Formalna verifikacija softvera metodom provjere modela", Diplomski rad, Sveučilište u Zagrebu, Prirodoslovno-matematički fakultet, Zagreb, 2019. Dostupno na: https://urn.nsk.hr/urn:nbn:hr:217:098202

Za citiranje koristite ovu mrežnu adresu: https://urn.nsk.hr/urn:nbn:hr:217:098202
Podaci o radu
NaslovFormalna verifikacija softvera metodom provjere modela
AutorKlara Lešić
MentorRobert Manger (mentor)
Član povjerenstvaRobert Manger (predsjednik povjerenstva)
Član povjerenstvaEduard Marušić-Paloka (član povjerenstva)
Član povjerenstvaGoran Igaly (član povjerenstva)
Član povjerenstvaGoran Radunović (član povjerenstva)
Ustanova koja je dodijelila
akademski / stručni stupanj		Sveučilište u Zagrebu
Prirodoslovno-matematički fakultet
(Matematički odsjek)
Zagreb
Datum i država obrane2019-11-27, Hrvatska
Znanstveno / umjetničko
područje, polje i grana		PRIRODNE ZNANOSTI
Matematika
Sažetak
Ovaj rad obrađuje teoriju o provjeri modela, jednoj od metoda formalne verifikacije softvera. Opisan je način modeliranja promatranog sustava u vidu tranzicijskih sustava, te način specificiranja svojstava pomoću formula linearne temporalne logike. Glavni cilj bio je predstaviti algoritam koji provjerava zadovoljava li tranzicijski sustav kojim je opisan promatrani softver LTL formulu koja opisuje željeno svojstvo. U tu svrhu, prvo je bilo potrebno uvesti pojmove nedeterminističkog Büchijevog automata (NBA), produkta tranzicijskog sustava i NBA, te svojstva perzistencije. Nadalje, opisana su neka važna svojstva koja se često ispituju provjerom modela. Na kraju je na primjerima dva poznata problema demonstriran rad model checkera NuSMV-a.
Sažetak (engleski)
This thesis addresses the theory of model checking, one of the formal software verification methods. It describes a way of modeling a software under consideration in terms of transition systems, and a way to specify properties using linear temporal logic formulae. The main goal was to present the algorithm that checks whether the transition system describing the software that needs to be verified satisfies the LTL formula that specifies a desired property. For this purpose, it was necessary to introduce the concepts of the nondeterministic Büchi automata (NBA), product of transition system and NBA, and persistence property. Furthermore, some important properties, that are often checked by model checking method, are described. Finally, on examples of two well-known problems, it is demonstrated how model checker NuSMV operates.
Ključne riječi
Ključne riječi (engleski)
Jezikhrvatski
URN:NBNurn:nbn:hr:217:098202
Studijski programNaziv: Računarstvo i matematika
Vrsta studija: sveučilišni
Stupanj studija: diplomski
Akademski / stručni naziv: magistar/magistra računarstva i matematike (mag. inf. et math.)
Vrsta resursaTekst
Način izrade datotekeIzvorno digitalna
Prava pristupaOtvoreni pristup
Uvjeti korištenjaIkona licence Zaštićeno autorskim pravom.
Datum i vrijeme pohrane2020-07-09 10:31:39