Model checking business processes

Business Process Management systems are often used to improve the productivity of organizations and companies. For such systems, it is important to control all the variables (among them the time) and the status of all the stakeholders that are involved into the processes. This task aims at improving the employee satisfaction, the estimation of time and criticalities, and the control of business processes of an organization. In spite of this important task, most of the companies base their analysis on very simple process models. This work presents a Semantic Timed Model Checking algorithm for Business Processes. It has been used as a basic tool in several scenarios such as process selection, process validation, and process monitoring. The approach relies on: 1) a representation of business processes based on semantically annotated timed transition systems (ATTS), 2) a representation of specifications based on a semantically annotated version of timed computation tree logic (AnTCTL), and 3) an efficient model checking algorithm. The ATTS allows us to take into account the temporal evolution of a business process, with its temporal constraints. This is based on Timed Transition Systems. The importance of semantics is also widely recognized. Indeed, semantics allows us to provide a non-ambiguous meaning to process activities and variables. According to the mainstream, the semantics relies on Description Logic. As a consequence, this work presents an integration of timed transition systems and semantic representation technologies in an efficient way. The AnTCTL allows us to represent the traditional performance indicators with a well-founded semantics. Furthermore, it is possible to define a new set of indicators that it is not possible to define with the traditional business process models. The model checking algorithm is an integration of traditional timed model checking techniques with semantic reasoning. This algorithm has been proved to be sound and complete and PSPACE-Complete. This work can be considered the first step towards the use of semantic timed model checking in problems of performance analysis for Business Processes. The proposed approach has been applied to real world case studies.

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.