1390 research outputs found
Sort by
Model checking business processes
I sistemi di Business Process Management sono spesso utilizzati per migliorare ed aumentare la produttività di organizzazioni ed aziende. Per tali sistemi è importante controllare tutte le variabili (compreso il tempo) e lo stato di tutti gli stakeholders che entrano in gioco nei processi. Questi task consentono di aumentare la soddisfazione degli operatori, consentono di migliorare le stime in termini di tempistiche, di controllare le criticità ed in genere consentono di tenere sotto controllo tutti i processi aziendali di un’organizzazione. Nonostante questo molte aziende basano le loro analisi su modelli di processi molto semplici. Questo lavoro presenta un algoritmo denominato “Semantic Timed Model Checking“ applicato ai processi aziendali. Questo algoritmo è stato impiegato in scenari differenti come la selezione, la validazione ed il monitoring dei processi. L’approccio è basato sui seguenti step:
1) rappresentazione dei processi aziendali sotto forma di “semantically annotated timed transition systems” (ATTS), 2) rappresentazione delle specifiche basate su di una rappresentazione annotata semanticamente della logica “timed computation tree logic” (AnTCTL), e 3) un efficiente algoritmo di model checking. Gli ATTS permettono di tenere in considerazione le evoluzioni nel tempo dei processi di business, con i loro vincoli temporali. Questa logica è basata sui sistemi TTS.
L’importanza della semantica è notoriamente riconosciuta, ci consente infatti di fornire significati non ambigui ai processi e alle variabili che in essi entrano in gioco. A tal fine vengono utilizzati formalismi propri della logica descrittiva.
Questo lavoro presenta un’integrazione dei sistemi TTS e della rappresentazione semantica in un modo molto efficiente. La AnTCTL premette infatti di rappresentare i tradizionali indicatori di performance con una semantica propria e ben definita. Inoltre è possibile introdurre una serie di nuovi indicatori che non sarebbero invece definibili con i modelli di processi aziendali tradizionali.
L’algoritmo di model checking è un integrzione dell’algoritmo “timed model checking” con aggiunta di notazioni semantiche.
Questo lavoro può essere considerato il primo passo verso l’utlizzo del semantic timed model checking nei problemi di analisi delle performance dei processi aziendali. Il metodo proposto è stato applicato ad un in caso di studio basato su processi aziendali reali