Formal methods for semantic case management

During the years, Business Process Management (BPM) has emerged as the go-to approach for handling routine work. As a result, business processes can be structured and therefore automated since characterized by a certain level of repeatability. Case Management (CM) and, more recently, Adaptive Case Management (ACM) were coined for more dynamic approaches taking into account knowledge work. Unlike the first, CM and ACM fit in managing processes characterized by a certain degree of uncertainty. Even if the principles of scientific management propose a clear distinction between routine and knowledge work, organizations cannot do the same: almost all work that people do consists of routine work and non-routine work. In this thesis project we propose a systematization of the aspects involved to represent knowledge-intensive processes. The overall goal is to integrate BPM and (A)CM features and formalize, through behavioral and semantic aspects, the elements taking part in the design and the execution of business processes. The ability to represent processes with defined and undefined paths of execution is achieved through a new modeling language based on Business Process Modeling Notation (BPMN). In conjunction with the graphical notation, we also provide its operational semantics. Business processes are described through parametric and annotated state-based systems that can be executed in specific enactment engines. Furthermore, formal methods based on Model Checking techniques can be applied to introduce verification and selection functionalities both at design-time and run-time. While the verification allow to verify and monitor properties of the systems under consideration, the latter enable to reuse process fragments and improve collaboration among different actors. All this with the aim to provide support and guidance to users. To evaluate the proposed approach, a case study taken from the Healthcare scenario is considered. In particular, taking into account how radiological visits are performed within Hospitals, it is possible to analyze the main results achieved in our approach.

Durante gli ultimi anni il Business Process Management (BPM) si è affermato come la metodologia principe per gestire attività di routine. Poiché caratterizzati da attività ripetibili, i processi aziendali possono essere strutturati e dunque automatizzati. Al contrario, il Case Management (CM) e, più recentemente, l’Adaptive Case Management (ACM) sono stati introdotti per affrontare tutte quelle situazioni in cui le attività da svolgere non possono essere definite a priori in quanto caratterizzate da un certo grado di incertezza. Anche se i principi del Taylorismo affermano che è possibile effettuare una netta distinzione tra il lavoro di routine e il lavoro della conoscenza, molto spesso le organizzazioni si trovano ad affrontare situazioni in cui le attività eseguite non appartengono ne all’uno ne all’altro: sono semplicemente un mix tra le due. In questo lavoro viene proposta una sistematizzazione degli aspetti utilizzati per rappresentare i cosiddetti processi knowledge-intensive, ossia processi basati sulla conoscenza. L’obiettivo è quello di integrare le caratteristiche del BPM e dell’(A)CM e formalizzare, attraverso aspetti procedurali e tecnologie semantiche, gli elementi utilizzati per modellare ed eseguire simili processi. La possibilità di rappresentare processi caratterizzati da percorsi di esecuzione già definiti assieme ad altri non definiti avviene grazie all’introduzione un nuovo linguaggio di modellazione basato su Business Process Modeling Notation (BPMN). A partire da una rappresentazione grafica del processo (il modello), ne viene fornita una semantica operazionale. Il risultato consiste in sistemi parametrici basati su transizioni di stato e annotati semanticamente che possono essere eseguiti all’interno di un qualsiasi motore di esecuzione. Tale rappresentazione permette di applicare metodi formali basati su Model Checking che consentono di introdurre due funzionalità principali: verifica e selezione. Mentre la prima permette di verificare e monitorare le proprietà di un sistema, la seconda favorisce il riuso dei processi aziendali e la collaborazione tra attori differenti. Entrambe possono essere impiegate sia in fase di modellazione che di esecuzione con l’obiettivo di fornire supporto agli utenti coinvolti nel processo. Per valutare l’approccio descritto in questa tesi è stato preso in esame un caso di studio relativo all’ambito sanitario. In particolare, considerando come le visite radiologiche vengono eseguite all’interno degli ospedali, è stato possibile analizzare i risultati ottenuti.