prikaz prve stranice dokumenta Formalna verifikacija softvera metodom provjere modela
  Download
PDF 1.8 MB
master's thesis
Formalna verifikacija softvera metodom provjere modela
Zagreb: University of Zagreb, Faculty of Science, 2019. urn:nbn:hr:217:098202
Lešić, Klara
University of Zagreb
Faculty of Science
Department of Mathematics

Institutional repository: Repository of the Faculty of Science

Cite this document

Lešić, K. (2019). Formalna verifikacija softvera metodom provjere modela (Master's thesis). Zagreb: University of Zagreb, Faculty of Science. Retrieved from https://urn.nsk.hr/urn:nbn:hr:217:098202

Lešić, Klara. "Formalna verifikacija softvera metodom provjere modela." Master's thesis, University of Zagreb, Faculty of Science, 2019. https://urn.nsk.hr/urn:nbn:hr:217:098202

Lešić, Klara. "Formalna verifikacija softvera metodom provjere modela." Master's thesis, University of Zagreb, Faculty of Science, 2019. https://urn.nsk.hr/urn:nbn:hr:217:098202

Lešić, K. (2019). 'Formalna verifikacija softvera metodom provjere modela', Master's thesis, University of Zagreb, Faculty of Science, accessed 08 July 2024, https://urn.nsk.hr/urn:nbn:hr:217:098202

Lešić K. Formalna verifikacija softvera metodom provjere modela [Master's thesis]. Zagreb: University of Zagreb, Faculty of Science; 2019 [cited 2024 July 08] Available at: https://urn.nsk.hr/urn:nbn:hr:217:098202

K. Lešić, "Formalna verifikacija softvera metodom provjere modela", Master's thesis, University of Zagreb, Faculty of Science, Zagreb, 2019. Available at: https://urn.nsk.hr/urn:nbn:hr:217:098202

Metadata
TitleFormalna verifikacija softvera metodom provjere modela
AuthorKlara Lešić
MentorRobert Manger (mentor)
Committee memberRobert Manger (predsjednik povjerenstva)
Committee memberEduard Marušić-Paloka (član povjerenstva)
Committee memberGoran Igaly (član povjerenstva)
Committee memberGoran Radunović (član povjerenstva)
GranterUniversity of Zagreb
Faculty of Science
(Department of Mathematics)
Zagreb
Defense date and country2019-11-27, Croatia
Scientific / art field,
discipline and subdiscipline		NATURAL SCIENCES
Mathematics
Abstract
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.
Abstract (english)
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.
Keywords
Keywords (english)
Languagecroatian
URN:NBNurn:nbn:hr:217:098202
Study programmeTitle: Computer Science and Mathematics
Study programme type: university
Study level: graduate
Academic / professional title: magistar/magistra računarstva i matematike (magistar/magistra računarstva i matematike)
Type of resourceText
File originBorn digital
Access conditionsOpen access
Terms of useLicence In copyright icon
Created on2020-07-09 10:31:39