Modeliranje i analiza labeliranog sustava sa prijelazima alatima za provjeru modela

diplomski rad

• Naslov (engleski): Labeled Transition System Modeling and Analysis with Model Checkers
• Autor: Dino Božić
• Mentor: Bruno Blašković (mentor)
• Član povjerenstva: Bruno Blašković (predsjednik povjerenstva)
• Član povjerenstva: Mirko Randić (član povjerenstva)
• Član povjerenstva: Luka Humski (član povjerenstva)
• Ustanova koja je dodijelila akademski / stručni stupanj: Sveučilište u Zagrebu; Fakultet elektrotehnike i računarstva; Zagreb
• Datum i država obrane: 2020-07-06, Hrvatska
• Znanstveno / umjetničko područje, polje i grana: TEHNIČKE ZNANOSTI; Računarstvo

Sažetak

Kako bi se omogućila fleksibilnost modula za dubinsku analizu poslovnih procesa potrebno je pokušati dokazati izravnu povezivost formata koji se koriste u različitim tehnikama analize. U ovom radu opisan je postupak pretvorbe modela definiranog jezikom Promela u model Petrijeve mreže. Promela model jest verifikacijski jezik kojem je primarna svrha provjera modela dok je Petrijeva mreža jedan od najpoznatijih formata za prikaz i analizu dubinske analize poslovnih procesa. Implementacija algoritma koji izvršava pretvorbu sastoji se od proučavanja svojstava i specijalnosti ulaznog i izlaznog formata te valjane prilagodbe na izlazni format. Konačan rezultat jest algoritam kojem je ulaz Promela model a izlaz funkcionalna Petrijeva mreža spremna za analizu.

Sažetak (engleski)

To enable module flexibility in order to support process mining it is necessary to prove direct connectivity between formats used for different analysis techniques. This master thesis describes the process of transforming model defined in Promela verification language into the Petri net model. Promela is a verification language whose primary purpose is model checking while Petri net format is one of the most recognizable ones in process mining and process analysis. Implementation of the transformation algorithm consist of researching characteristics and specialities of both input and output formats and their adjustments for the final output. Final result is an algorithm whose input format is a Promela model and the output is a fully functional Petri Net ready for analysis.

• Ključne riječi: analiza procesa; analiza podataka; labelirani sustavi; provjera modela
• Ključne riječi (engleski): process mining; data analyzing; labeled transition systems; model checkers
• Jezik: hrvatski
• URN:NBN: urn:nbn:hr:168:668852
• Studijski program: Naziv: Računarstvo; Vrsta studija: sveučilišni; Stupanj studija: diplomski; Akademski / stručni naziv: magistar/magistra inženjer/inženjerka računarstva (mag.ing.comp.)
• Vrsta resursa: Tekst
• Način izrade datoteke: Izvorno digitalna
• Prava pristupa: Zatvoreni pristup
• Datum i vrijeme pohrane: 2023-01-13 11:51:39