Modeliranje i analiza labeliranog sustava sa prijelazima alatima za provjeru modela

master's thesis

• Title (english): Labeled Transition System Modeling and Analysis with Model Checkers
• Author: Dino Božić
• Mentor: Bruno Blašković (mentor)
• Committee member: Bruno Blašković (predsjednik povjerenstva)
• Committee member: Mirko Randić (član povjerenstva)
• Committee member: Luka Humski (član povjerenstva)
• Granter: University of Zagreb; Faculty of Electrical Engineering and Computing; Zagreb
• Defense date and country: 2020-07-06, Croatia
• Scientific / art field, discipline and subdiscipline: TECHNICAL SCIENCES; Computing

Abstract

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.

Abstract (english)

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.

• Keywords: analiza procesa; analiza podataka; labelirani sustavi; provjera modela
• Keywords (english): process mining; data analyzing; labeled transition systems; model checkers
• Language: croatian
• URN:NBN: urn:nbn:hr:168:668852
• Study programme: Title: Computing; Study programme type: university; Study level: graduate; Academic / professional title: magistar/magistra inženjer/inženjerka računarstva (magistar/magistra inženjer/inženjerka računarstva)
• Type of resource: Text
• File origin: Born digital
• Access conditions: Closed access
• Created on: 2023-01-13 11:51:39