Site Network:

ICT4Law Regione Piemonte

Attività del Dipartimento di Informatica - Università del Piemonte Orientale

L'attività svolta dall'unità del Dipartimento Informatica dell’Università del Piemonte Orientale (da gennaio 2012, Sezione di Informatica del Dipartimento di Scienze e Innovazione Tecnologica) è stata rivolta alla verifica di conformità (compliance) a norme di procedure aziendali e amministrative.

Tale attività ha compreso tre aspetti fra essi correlati: la modellazione delle procedure, la modellazione delle norme e il ragionamento automatico per dimostrare la conformità.

Nell’ambito dei formalismi esistenti per la modellazione di processi aziendali presenti in letteratura è stato individuato il linguaggio YAWL (Yet Another Workflow Language) come linguaggio di riferimento, in quanto si tratta di uno dei linguaggi più espressivi, basato su un’ampia analisi dei pattern di workflow utilizzati in pratica, e su un approccio formale; utilizza XML, che favorisce l’interoperabilità; come i sistemi commerciali, ha associato un vero e proprio BPMS (Business Process Management System).

La specifica di un processo in un formalismo come YAWL ai fini dell’esecuzione del processo, o ai fini di documentazione interna, non richiede tuttavia di modellare esplicitamente le relazioni tra i passi del processo e i concetti, le condizioni e gli eventi menzionati e vincolati dalle norme.
A tal fine è stato quindi previsto di arricchire il modello con annotazioni che descrivano gli effetti e le precondizioni dei task atomici presenti nel processo, in particolare quelli menzionati nelle norme o correlati a questi ultimi. Rispetto a proposte simili presenti in letteratura, si è scelto di utilizzare i formalismi sviluppati in Intelligenza Artificiale per modellare il ragionamento su azioni e cambiamento, in quanto essi permettono di modellare in modo sofisticato dipendenze tra condizioni ed eventi (ovvero come i cambiamenti dei valori di verità di alcune condizioni possono ripercuotersi su altre).
È stato quindi definito uno schema XML per rappresentare regole che descrivono effetti diretti delle azioni (intese in questo caso come attività atomiche del processo) e regole causali che descrivono interdipendenze tra condizioni, permettendo di rappresentare conoscenza generale sul dominio che metta in relazione effetti delle attività e condizioni menzionate nelle norme.

Date tali premesse, è stato naturale individuare le logiche temporali, utilizzate in letteratura per la verifica di proprietà di sistemi e processi di vario tipo, come il formalismo per la rappresentazione delle norme da verificare in questo caso. Gli obblighi, presenti nelle norme di riferimento, sono stati rappresentati mediante la nozione di commitment, ben nota nell’approccio sociale alla comunicazione fra agenti. La verifica di conformità di un processo di business rispetto alle norme comprende la verifica che non esistano esecuzioni del processo che lascino dei commitment non realizzati.

Per quanto riguarda la verifica automatica della conformità sono state esplorate due alternative, la prima basata sulle Reti di Petri, la seconda sulla Logica Computazionale.

Le Reti di Petri sono uno dei formalismi più utilizzati nell’analisi di processi, in particolare per quanto riguarda il flusso di controllo, e sono disponibili diversi insiemi di tools per elaborazioni basati su Reti di Petri, ed in particolare CPN Tools, che fornisce un ambiente integrato per la definizione e verifica di modelli specificati con Colored Petri Net (CPN), ambiente basato sul linguaggio CPN-ML, un dialetto del linguaggio funzionale Standard ML.

È stato quindi realizzato il seguente percorso per la verifica:

- traduzione automatica di un modello YAWL e di un file XML di annotazioni del processo in una Rete di Petri Colorata che riproduce il flusso di controllo del modello YAWL, arricchita con posti, archi e funzioni sugli archi, allo scopo di calcolare il valore delle annotazioni semantiche;
- effettuazione, mediante apposito tool disponibile in CPN Tools, della verifica delle formule corrispondenti alle norme, espresse in ASK-CTL, una variante della logica temporale CTL, interpretata sullo spazio degli stati del modello CPN da verificare, che permette di esprimere le proprietà da verificare sia sugli stati sia sulle transizioni del modello stesso.

Tale percorso è attualmente limitato alla verifica di condizioni relative alla prospettiva del flusso di controllo; per gli aspetti relativi ai dati sono state individuate delle soluzioni, ed è prevista la realizzazione di una analoga traduzione.

Per quanto riguarda la Logica Computazionale, si è utilizzata la tecnologia dell' Answer Set Programming (ASP). In particolare, è stato introdotto il formalismo della Temporal ASP, combinazione di Answer Set Programming (ASP) e Dynamic Linear Time Temporal Logic (DLTL) che consente di specificare sia il processo di business sia le norme da verificare.

Il percorso per la verifica realizzato in questo caso consiste in:

- traduzione automatica di un modello YAWL e delle annotazioni XML in formule di Answer Set Programming
- rappresentazione in Answer Set Programming della tecnica di verifica detta Bounded Model Checking
- rappresentazione in Answer Set Programming della formula da verificare
- effettuazione della verifica come ricerca di modelli del programma risultante dall’unione delle formule ai punti precedenti

Viene trattata la prospettiva del flusso di controllo e, in forma limitata, la prospettiva dei dati.

L’approccio basato su Reti di Petri si basa su ambienti e strumenti che, pur non essendo direttamente progettati per un utilizzo commerciale, sono il risultato di progetti di ricerca di durata considerevole. D’altra parte, il trattamento delle annotazioni richiede apposita programmazione; inoltre, un trattamento completo di annotazioni con dipendenze complesse richiede l’implementazione di algoritmi simili a quelli utilizzati nel secondo approccio.
L’approccio basato su Logica Computazionale permette infatti di trattare direttamente i casi più generali di annotazioni; inoltre, data la natura dichiarativa dell’Answer Set Programming, questo percorso permette di integrare una rappresentazione dichiarativa del processo.

Pubblicazioni

- D. D'Aprile, L. Giordano, V. Gliozzi, A. Martelli, G. L. Pozzato, and D. Theseider Dupré. Verifying Business Process Compliance by Reasoning about Actions. In Jürgen Dix, João Leite, Guido Governatori, and Wojtek Jamroga, editors, Proceedings of CLIMA XI (Computational Logic in Multi-Agent Systems, 11th International Workshop), special session in Norms and Normative Multi-Agent Systems, volume 6245 of LNAI, pages 99-116, Lisbon, Portugal, 2010. Springer-Verlag.
- D. D'Aprile, L. Giordano, V. Gliozzi, A. Martelli, G. L. Pozzato, and D. Theseider Dupré. Verifying Business Process Compliance by Reasoning about Actions. In Angelo Susi, editor, Proceedings of the First Workshop on Law Compliancy Issues in Organisational Systems and Strategies (iComply 2010), Firenze, Italy, 2010.
- D. D'Aprile, L. Giordano, A. Martelli, G.L. Pozzato, D. Rognone, D. Theseider Dupré'. Business process compliance verification: an annotation based approach with commitments. In: Information Systems: Crossroads for Organization, Management, Accounting and Engineering. Springer, 2012.
- L. Giordano, A. Martelli, and D. Theseider Dupré. Reasoning about Actions with Temporal Answer Sets. Theory and Practice of Logic Programming, 2012, available at http://arxiv.org/abs/1110.3672.
- L. Giordano, A. Martelli, and D. Theseider Dupré. Achieving completeness in bounded model checking of action theories in ASP, Proc. 13th International Conference on Principles of Knowledge Representation and Reasoning, KR 2012.