Formalna verifikacija softvera metodom provjere modela

master's thesis

• Author: Klara Lešić
• Mentor: Robert Manger (mentor)
• Committee member: Robert Manger (predsjednik povjerenstva)
• Committee member: Eduard Marušić-Paloka (član povjerenstva)
• Committee member: Goran Igaly (član povjerenstva)
• Committee member: Goran Radunović (član povjerenstva)
• Granter: University of Zagreb; Faculty of Science; (Department of Mathematics); Zagreb
• Defense date and country: 2019-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: provjera modela; linearna temporalna logika; NuSMV
• Keywords (english): model checking; linear temporal logic; NuSMV
• Language: croatian
• URN:NBN: urn:nbn:hr:217:098202
• Study programme: Title: 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 resource: Text
• File origin: Born digital
• Access conditions: Open access
• Created on: 2020-07-09 10:31:39