Radni okvir za vizualno modeliranje i formalnu verifikaciju izvršavanja poslovnoga procesa temeljen na modelima s dvosmjernim preslikavanjem : doktorski rad - Matković, Jelena (J. Matković ; Fakultet elektrotehnike i računarstva, 2019)
Web Service Business Process Execution Language (WS-BPEL) je dominantan standard za integraciju postojećih web usluga u cjelinu kojom se podupire izvršavanje poslovnog procesa. Cilj integracije nije samo omogućiti razmjenu poruka između učesnika poslovnog procesa, nego razmjenu poruka realizirati tako da se ona izvršava točno u trenutcima i na način kako bi se odvijali koraci stvarnog poslovnog procesa. WS-BPEL koristi na XML-u zasnovan jezik koji podržava web tehnologije. Budući da WS-BPEL specifikacija ne određuje službeni standard za vizualno modeliranje procesa, javila se ideja za razvojem vlastitog modela za vizualno modeliranje procesa. Osim vizualnog modeliranja, kao potrebna pokazala se formalna verifikacija izvršavanja budući da se unutar WS-BPEL procesa mogu pojaviti paralelna izvršavanja čime ponašanje sustava zbog brzine paralelnih komponenti postaje potencijalno nesigurno. Ovaj doktorski rad razradio je korake modela faznog modeliranja WS-BPEL poslovnog procesa na način da su ključne faze razvoja WS-BPEL procesa vezane za vizualno modeliranje i formalnu verifikaciju, a tu je i faza statičke provjere izvršnog modela procesa prema pravilima definiranim WS-BPEL specifikacijom. Za vizualno modeliranje predložen je standard Business Process Model and Notation (BPMN) koji je u pozadini također zasnovan na jeziku XML. Definiran je algoritam za dvosmjerno automatsko preslikavanje između standarda BPMN i WS-BPEL. Za prikazivanje formalnog modela odabrana je sintaksa Process Meta Language (Promela). Cilj formalne verifikacije je provjera rukovanja varijablama kao ključnim elementima poslovnog procesa. Osim predloženog faznog modela za razvoj WS-BPEL procesa i pripadajućih algoritama, u doktorskom radu je definiran i radni okvir s prijedlozima konkretnih alata koji su korišteni za realizaciju modela i pripadnih algoritama. Verifikacija algoritama korištenih u modelu i radnom okviru je izvršena nad hipotetičkim poslovnim procesima. Ključne riječi: uslužno orijentirane arhitekture, WS-BPEL, integracija usluga, faze razvoja poslovnog procesa, vizualno modeliranje, formalna verifikacija sustava, BPMN, konačni automati.