Curriculum Didattico e Scientifico

di

Marco Montali

Aggiornato al 4 dicembre 2010

Sinossi

Marco Montali ha conseguito il Diploma di Laurea in Ingegneria Informatica cum laude nel2003, il Diploma di Laurea Specialistica in Ingegneria Informatica cum laude nel 2005 e il titolodi Dottore di Ricerca in Informatica, Elettronica e Telecomunicazioni nel 2009. E attualmentetitolare di un assegno di ricerca post-dottorale presso il Dipartimento di Elettronica, Informaticae Sistemistica dell’Universita di Bologna.La sua attivita di ricerca si inquadra nell’area dell’Intelligenza Artificiale. In particolare, verte suaspetti fondazionali, metodologici e sperimentali legati allo studio di linguaggi formali basatisulla logica computazionale, e dei relativi strumenti di ragionamento automatico, per la specificae la verifica di modelli di interazione in sistemi basati su eventi. Fra i campi applicativi dellasua ricerca figurano i processi aziendali, i sistemi orientati ai servizi e agli agenti, le linee guidain campo medico.E autore di una monografia edita da Springer su specifica e verifica di modelli di interazionedichiarativi e aperti, e di piu di 50 articoli sui seguenti temi: logica computazionale, programma-zione logica e sue estensioni; modellazione (dichiarativa), verifica formale e monitoraggio diprocessi aziendali, regole di business, coreografie di servizi, linee guida in campo medico e pro-tocolli di cura; process mining; verifiche di interoperabilita, composizione e discovery di serviziweb (semantici); sistemi multi-agente aperti e approcci basati su commitments; ragionamentotemporale e calcolo degli eventi.La sua tesi di Dottorato e stata insignita del premio “Marco Cadoli”, promosso dall’AssociazioneItaliana di Programmazione Logica per le due migliori tesi di Dottorato svolte sui temi dellaLogica Computazionale e discusse nel triennio 2007-2009. Nel 2010 ha vinto un Best Paper Award.Dal 2004, Marco Montali svolge attivita didattica di supporto a livello accademico, nell’ambitodei corsi di Fondamenti di Informatica, Sistemi Operativi e Intelligenza Artificiale, e dal 2006

segue tesi di laurea in qualita di co-relatore. Dal 2009, svolge attivita di formazione azienda-le e consulenza informatica. E chair del doctoral program per la Terza Scuola InternazionalePrimaverile sulla Logica Computazionale (ISCL 2011).

indice

1 INFORMAZIONI GENERALI 3

1.1 Dati biografici 3

1.2 Formazione scientifica, borse di studio e soggiorni all’estero 3

2 RICONOSCIMENTI E PREMI 7

2.1 Marco Cadoli Distinguished Dissertation Award 7

2.2 Finalista al Premio Lions Club per la ricerca scientifica e l’innovazionetecnologica 8

2.3 Best Paper Awards 8

3 ATTIVITA DI SUPPORTO ALLA RICERCA 9

3.1 Partecipazione a progetti di ricerca 9

3.2 Attivita organizzative 9

3.3 Relazioni invitate e seminari 9

3.4 Attivita di revisione e comitati di programma 10

3.5 Presentazioni a eventi internazionali 10

4 ATTIVITA DI RICERCA 11

4.1 Approcci dichiarativi e aperti per la rappresentazione della conoscenza eil ragionamento automatico in sistemi basati su eventi 11

4.2 Logiche per la formalizzazione di modelli di interazione 12

4.3 Business process management 13

4.4 Architetture orientate ai servizi 15

4.5 Sistemi multi-agente aperti 17

4.6 Combinazione di approcci orientati agli agenti, servizi e processi 18

4.7 Linee guida in campo medico e protocolli di cura 19

5 PUBBLICAZIONI 20

5.1 Libri 20

5.2 Tesi di Dottorato 20

5.3 Riviste internazionali 20

5.4 Riviste a diffusione internazionale 21

5.5 Contributi su libro 21

5.6 Atti di conferenze e workshop 21

5.7 Altre conferenze e workshop con revisione 25

5.8 Tesi di laurea 27

5.9 Articoli in fase di revisione 27

6 ATTIVITA DIDATTICA 28

7 ALTRE COMPETENZE 30

7.1 Linguaggi ed ambienti di sviluppo 30

7.2 Altre esperienze 30

8 REFERENZE 31

2

1. informazioni generali

1.1 Dati biografici

Nome Marco Montali

Cittadinanza Italiana

Nato a Verona, il 27 settembre 1981

Telefono +39 333 1581175

E-mail marco.montali@unibo.it

Home page http://ai.unibo.it/People/MarcoMontali

Titoli di studio Laurea di Primo Livello in Ingegneria Informatica, conseguita nel luglio2003 presso l’Universita di Bologna, con votazione 110/110 e lode.

Laurea Specialistica in Ingegneria Informatica, conseguita nell’ottobre2005 presso l’Universita di Bologna, con votazione 110/110 e lode.

Dottorato in Elettronica, Informatica e Telecomunicazioni, conseguitonell’aprile 2009 presso l’Universita di Bologna.

Posizione attuale Titolare di un Assegno di Ricerca Post-Dottorale presso il Dipartimentodi Elettronica, Informatica e Sistemistica (DEIS) dell’Universita diBologna.

Lingue straniere Inglese, Tedesco (possessore di Patentino di Bilinguismo - Livello B,rilasciato dalla Provincia Autonoma di Bolzano)

1.2 Formazione scientifica, borse di studio e soggiorni all’estero

Luglio 2000 Consegue il diploma di Liceo Scientifico con voto finale di 100/100.

Luglio 2003 Discute la tesi dal titolo “Modellazione dell’interazione nei sistemi multi-agente”e consegue la Laurea di Primo Livello in Ingegneria Informatica pres-so l’Universita di Bologna, con voto finale di 110/110 e lode (media deivoti pari a 29.5/30). Nella tesi approfondisce lo studio di diversi linguag-gi per la specifica di protocolli di interazione nei sistemi multi-agente,confrontando in particolare approcci dichiarativi (orientati ai vincoli) eprocedurali (orientati ai flussi di esecuzione).Corsi sostenuti: analisi matematica, chimica, fisica, fondamenti di informatica, elettro-tecnica, reti logiche, geometria ed algebra, controlli automatici, matematica applicata,comunicazioni elettriche, calcolatori elettronici, elettronica analogica, elettronica digi-tale, reti di telecomunicazioni, sistemi operativi, analisi numerica, sistemi informativi,fondamenti di ricerca operativa, reti di calcolatori, ingegneria del software, economia emanagement, amministrazione di reti di calcolatori, tecnologie web.

3

Gennaio 2005 Vince una borsa di trasferimento tecnologico presso il Consorzio Spin-ner (Servizi per la Promozione dell’INNovazione e della Ricerca). Ilprogetto verte sulla formalizzazione e verifica di protocolli di cura; coin-volge da un lato i gruppi di Intelligenza Artificiale del Dipartimento diElettronica, Informatica e Sistemistica dell’Universita di Bologna e delDipartimento di Ingegneria dell’Universita di Ferrara, e dall’altro Dianoe-ma s.p.a.1, una delle piu importanti aziende a livello europeo nel campodell’informatica clinica ospedaliera.

Ottobre 2005 Discute la tesi dal titolo “Un linguaggio grafico per la specifica e la verifica diprotocolli” e consegue la Laurea Specialistica in Ingegneria Informaticapresso l’Universita di Bologna, con voto finale di 110/110 e lode (mediadei voti pari a 29.9/30). Nella tesi progetta un linguaggio per la specificadell’interazione (combinando una notazione grafica worfklow-like con l’usodi ontologie di dominio), e sintetizza un algoritmo per tradurre auto-maticamente i modelli prodotti in una corrispondente rappresentazioneformale basata sulla logica, al fine di abilitare diverse tipologie di verifica.Corsi sostenuti: Algoritmi di ottimizzazione, controlli automatici (corso avanzato), calco-latori elettronici (corso avanzato), fondamenti di intelligenza artificiale, applicazioni diintelligenza artificiale, gestione dell’innovazione e dei progetti, ingegneria del software(corso avanzato), linguaggi e modelli computazionali, matematica discreta, processi etecniche di data mining, reti di calcolatori (corso avanzato), ricerca operativa (corsoavanzato), sistemi informativi (corso avanzato), sistemi digitali, sistemi in tempo reale,sistemi operativi (corso avanzato), tecnologie per la sicurezza.

Gennaio 2006 E tra i vincitori del concorso per l’ammissione al Dottorato di Ricercain Elettronica, Informatica e Telecomunicazioni presso l’Universita diBologna, e beneficia di una borsa di studio (triennale) MIUR per svolgereil Dottorato. Inizia la sua attivita di ricerca, affrontando temi inerenti lamodellazione di sistemi basati su eventi con approcci dichiarativi, e la loroformalizzazione e verifica mediante linguaggi e strumenti di ragionamentobasati su logica computazionale. Ne studia l’applicazione in diversi ambitiapplicativi, quali i processi di business, le linee guida in campo medico,sistemi orientati ai servizi e sistemi multi-agente.

Gennaio 2009 Vince il bando C.I.N.I. per un contratto di prestazione d’opera a progettonell’ambito del Progetto TOCAI.IT, della durata di quattro mesi, sul tema“Process mining: analisi di tracce di esecuzione di processi aziendali”. Svilup-pa uno strumento per l’analisi a posteriori di log di processi aziendalimediante regole di business, e ne studia l’applicazione su diversi casi distudio industriali. Per maggiori informazioni, si veda [P.29].

Aprile 2009 Consegue il titolo di Dottore di Ricerca in Elettronica, Informatica e Te-lecomunicazioni presso l’Universita di Bologna, discutendo la tesi daltitolo Specification and Verification of Declarative Open Interaction Models: a

1 Oggi Noemalife

4

Logic-Based Approach (relatore: Prof. Paola Mello). La tesi e stata succes-sivamente insignita del premio “Marco Cadoli”, promosso dal Grupporicercatori e Utenti di Logic Programming per le due migliori tesi di Dot-torato svolte sui temi della Logica Computazionale e discusse nel triennio2007–2009 (si veda pagina 7). Una versione riveduta e corretta e statainoltre recentemente pubblicata come monografia Springer nella serieLecture Notes in Business Information Processing.

Maggio 2009 Vince il bando del Dipartimento di Elettronica, Informatica e Sistemisticadell’Universita di Bologna per un contratto di collaborazione coordinatae continuativa, della durata di cinque mesi, sull’applicazione di tecnichedi Intelligenza Artificiale applicate ai flussi turistici. Si occupa dell’inte-grazione tra ontologie e regole per la modellazione del dominio turisticoe la validazione di pacchetti e servizi.

Agosto 2009 Comincia la sua attivita di formazione e consulenza informatica aziendale.In particolare, ricopre il ruolo di consulente di direzione (senior consul-tant) presso l’azienda Image Line s.r.l., leader nella realizzazione di portaliinformativi e redazionali nel settore agricolo. In particolare, si occupa:

• di attivita di consulenza sugli obiettivi di breve, medio e lungotermine dell’azienda;

• della realizzazione di un sistema gestionale web con relativo CRM;

• della ristrutturazione della base dati aziendale e dei portali web, conparticolare attenzione alla fruizione delle informazioni e all’integra-zione dei dati;

• della formazione del personale tecnico aziendale su temi di ingegne-ria del software, con particolare attenzione allo sviluppo del software“orientato agli oggetti”, UML, pattern architetturali e di progetto,JAVA, tecnologie J2EE e meccanismi di Object-Relational Mapping(ORM).

Novembre 2009 Risulta vincitore di un assegno di ricerca post-dottorale presso il Di-partimento di Elettronica, Informatica e Sistemistica dell’Universita diBologna, sul tema “Un approccio dichiarativo per la specifica e verifica di lineeguida in campo medico”. L’attivita di ricerca verte sull’uso di linguaggi grafi-ci, e di formalismi basati sulla logica computazionale, per complementareuna modellazione workflow-like delle linee guida con una componentedichiarativa e flessibile, al fine di catturare in maniera piu adeguata laconoscenza medica coinvolta in esse. Vengono inoltre approfondite diver-se tecniche di verifica e monitoraggio, per fornire concreto supporto aglioperatori sanitari durante l’esecuzione.

Luglio 2010 Vince un Visitor Travel Grant assegnato dall’ente olandese per la ricercascientifica (NWO – Netherlands Organization for Scientific Research). Si recain visita per un mese alla Eindhoven University of Technology, al finedi collaborare con il Prof. Wil van der Aalst e il gruppo Architecture of

5

Information Systems sullo studio di metodologie e strumenti di supportoall’esecuzione dei processi di business. Viene in particolare approfonditoil tema del monitoraggio di business constraints mediante approcci logici(Calcolo degli Eventi e Logica Temporale Lineare) e implementato unprototipo all’interno dell’ultima versione del noto framework di processmining denominato ProM.

6

2. riconoscimenti e premi

2.1 Marco Cadoli Distinguished Dissertation Award

Vince il premio “Marco Cadoli”, promosso dal Gruppo ricercatori e Utenti di LogicProgramming (GULP) per le due migliori tesi di Dottorato svolte sui temi della Logi-ca Computazionale e discusse tra il 2007 e il 2009. La procedura di assegnazione delpremio ha visto coinvolti piu di trenta esperti internazionali2. Si allegano di seguito icommenti dei revisori che hanno accettato di rendere pubblica la propria valutazione.

Robert A. Kowalski - Professor Emeritus, Department of Computing, Logic and Artificial Intelligence Group,Imperial College London, UK

I decided to read the entire thesis, because it contains so much interesting and important material.The thesis contains both wide-ranging background work and the original contributions of the thesis itself.The contributions of the thesis include not only significant contributions to theory, but also importantwork on practical implementation and applications.The subject of the thesis, the Specification and Verification of Declarative Open Interaction Models, isexceptionally broad and outward-looking. The thesis bridges the gap between the methods of Com-putational Logic developed mainly in Artificial Intelligence and the tools and techniques developed insuch otherwise unrelated domains as Business Process Management, Clinical Guidelines and CareflowProtocols, Service-Oriented and Multi-Agent Systems. Most PhD theses are restricted to a single domainand narrowly deal with only theoretical, implementation of application issues.In addition to the original work presented in the thesis, the thesis includes a analysis of and comparisonwith related work, including the use of Linear Temporal Logic and Model Checking. Montali presentsconvincing evidence for the benefits of his approach, but is modest in his acknowledgement of itslimitations and in his assessment of related work.This is one of the best PhD theses I have seen in a long time.

Wil M.P. van der Aalst - Full Professor, Department of Mathematics & Computer Science, Eindhoven Universityof Technology, Eindhoven, The Netherlands

The thesis is truly excellent and I would like to nominate the work for the best dissertation award.The work covers a broad area and provides deep and interesting results. Moreover, the work is supportedby a nice set of tools. The framework consists of ConDec, CLIMB (a subset of SCIFF), g-SCIFF, andREC. It is shown that CLIMB is more expressive than LTL and this is demonstrated using ConDec.This is supported by checks at design-time and run-time. Moreover, the approach provides all kinds ofadditional support. Very interesting is the ability to discover declarative models. This is challenging andhighly relevant.The thesis work has resulted in a large number of high-quality publications. Moreover, the work hasbeen presented at top conferences.

2 Per vedere il panel degli esperti, si consultihttp://lia.deis.unibo.it/gulp/Burocrazia/bando-premi-tesi-2009.html

7

2.2 Finalista al Premio Lions Club per la ricerca scientifica e l’innovazione tecnologica

Nel maggio 2010, Marco Montali e selezionato tra i 5 finalisti per il Premio LionsClub per la ricerca scientifica e l’innovazione tecnologica, assegnato alla miglior tesinell’anno 2009-2010 sviluppata nell’ambito della Scuola di Dottorato in Scienze eIngegneria dell’Informazione – Universita di Bologna.

2.3 Best Paper Awards

L’articolo F. Chesani, P. Mello, M. Montali e P. Torroni. Monitoring Time-Aware SocialCommitments with Reactive Event Calculus. Proceedings of the 7th International Symposium“From Agent Theory to Agent Implementation” (AT2AI-7), Vienna (Austria), 6-7 aprile 2010vince il Best Paper Award.

8

3. attivita di supporto alla ricerca

3.1 Partecipazione a progetti di ricerca

PRIN 2005 Progetto MIUR PRIN 2005-011293 Specifica e verifica di protocolli diinterazione fra agenti, Coordinatore Prof. Alberto Martelli.

FIRB 2005 Progetto FIRB RBNE05BFRK TOCAI.IT – Tecnologie Orientate alla Co-noscenza per Aggregazioni di Imprese in Internet, Coordinatore Prof. Mau-rizio Lenzerini. In particolare, partecipa all’attivita 9: “scoperta e classifica-zione di processi e conoscenza intra e inter-organizzativa”.

PRIN 2007 Progetto MIUR PRIN 2007-7WWCR8 Le forme di correlazione tra Ita-lian Style, flussi di turismo e trend di consumo del Made in Italy,Coordinatore Prof. Bernardo Valli.

3.2 Attivita organizzative

Aprile 2011 E chair del doctoral program per la Terza Scuola Internazionale Primaverilesulla Logica Computazionale (ISCL 2011), http://lia.deis.unibo.it/confs/iscl/

3.3 Relazioni invitate e seminari

12/12/2007 Declarative Specification and Verification of Service Choreographies. Relazioneinvitata al PSW Day (giornata tematica sulla verifica dei web services),LORIA, Nancy (Francia).

08/01/2008 Verification of Declarative Business Processes and Choreographies. Seminariopresso la Eindhoven University of Technology, Eindhoven (Olanda).

17/01/2008 Verification of Declarative Business Processes and Choreographies. Seminarionella riunione conclusiva del progetto PRIN 2005 Specifica e verifica diprotocolli di interazione fra agenti, Alessandria.

19/07/2010 Reasoning on Execution Traces with the Event Calculus. Tutorial presso laEindhoven University of Technology, Eindhoven (Olanda).

29/07/2010 Business Constraints Monitoring and Operational Support. Seminario pressola Eindhoven University of Technology, Eindhoven (Olanda).

30/11/2010 Monitoring Time-Aware Social Commitments. Relazione invitata all’Annualmeeting of the Interdisciplinary Laboratory on Interacting Knowledge Systems(ILIKS), LOA–CNR, Trento.

9

3.4 Attivita di revisione e comitati di programma

Marco Montali ha svolto attivita di revisione e/o e stato parte del comitato di pro-gramma per le seguenti riviste e convegni internazionali e nazionali:IEEE Transactions on Services Computing, Journal of Autonomous Agents and Multi-Agent Systems (JAAMAS), LNCS Transactions on Petri Nets and Other Models ofConcurrency (ToPNoC), International Joint Conference on Artificial Intelligence (IJCAI),International Conference on Autonomous Agents and Multiagent Systems (AAMAS),European Conference on Logics in Artificial Intelligence (JELIA), Conference on Ar-tificial Intelligence in Medicine (AIME), International Symposium on Methodologiesfor Intelligent Systems (ISMIS), International Conference on Advances in SemanticProcessing (SEMAPRO), Mexican International Conference on Artificial Intelligence(MICAI 2006), International Workshop on Declarative Agent Languages and Techno-logies (DALT), Workshop on Computational Logic in Multi-Agent Systems (CLIMA),International Workshop on Governance, Risk, and Compliance on Information Systems(GRCIS), Workshop on Agents, Web-Services, and Ontologies (MALLOW AWESO-ME), Convegno Italiano di Logica Computazionale (CILC), Workshop on Multi-AgentSystems and Bioinformatics (MAS&BIO).

3.5 Presentazioni a eventi internazionali

24/06/2005 Using social integrity constraints for on-the-fly compliance verification of medicalprotocols. Presentazione al 18th IEEE Symposium on Computer Based MedicalSystems (CBMS’05), Dublino (Irlanda).

28/08/2006 Abduction for specifying and verifying web service choreographies. Presentazio-ne al 4th International Workshop on AI for Service Composition (AISC2006), incongiunzione con ECAI2006, Riva del Garda.

09/09/2006 Computational Logic for Run-Time Verification of Web Services Choreographies:exploiting the SOCS-SI tool. Presentazione al 3rd International Workshop onWeb Services and Formal Methods (WS-FM 2006), Vienna (Austria).

01/09/2008 Checking Compliance of Execution Traces to Business Rules. Presentazione alWorkshop on Business Process Intelligence (BPI2008), in congiunzione conBPM2008, Milano.

05/09/2008 Verification of Choreographies During Execution Using the Reactive Event Calcu-lus. Presentazione al 5th International Workshop on Web Services and FormalMethods (WS-FM2008), Milano.

09/07/2009 A REC-Based Commitment Tracking Tool. Demo al Decimo Workshop Nazionale“Dagli Oggetti agli Agenti”, Parma.

06/04/2010 Monitoring Time-Aware Social Commitments with Reactive Event Calculus.Presentazione al 7th International Symposium “From Agent Theory to AgentImplementation” (AT2AI-7), Vienna (Austria). L’articolo ha vinto il BestPaper Award.

10

4. attivita di ricerca

L’attivita di ricerca di Marco Montali si inquadra nell’area dell’Intelligenza Artificiale.In particolare, verte su aspetti fondazionali, metodologici e sperimentali legati allostudio di linguaggi formali basati sulla logica computazionale, e dei relativi strumentidi ragionamento automatico, per la specifica e la verifica di modelli di interazione insistemi basati su eventi. Fra i campi applicativi della sua ricerca figurano i processiaziendali, i sistemi orientati ai servizi e agli agenti, le linee guida in campo medico.

4.1 Approcci dichiarativi e aperti per la rappresentazione della conoscenza e il ragionamentoautomatico in sistemi basati su eventi

L’avvento dei sistemi distribuiti ed eterogenei ha gettato le basi per la nascita di nuoviparadigmi architetturali, nell’ambito dei quali entita separate ed autonome collaboranoed interagiscono al fine di raggiungere obiettivi strategici complessi, impossibili darealizzarsi in solitudine. Una lista non esaustiva di sistemi organizzati con questiparadigmi include la gestione dei processi aziendali (Business Process Management),le linee guida in campo medico e i protocolli di cura (Clinical Guidelines e Care-FlowProtocols), i sistemi orientati ai servizi (Service-Oriented Systems) e agli agenti (Multi-AgentSystems). Tutti questi sistemi spostano l’attenzione dai singoli partecipanti alla lorointerazione/cooperazione; ogni (inter)azione effettuata viene tipicamente modellata etracciata in termini di eventi, il cui insieme caratterizza la dinamica “osservabile” diuna specifica esecuzione del sistema. Per questo motivo tali sistemi possono esseregenericamente identificati con l’accezione di sistemi basati su eventi.

In tale ambito, Marco Montali sta investigando nuovi paradigmi e linguaggi di model-lazione, capaci di mediare tra supporto alla conformita (compliance), per regolamentareil comportamento dei partecipanti, e flessibilita, intesa come liberta di azione delle entitainteragenti, permettendo loro di cogliere opportunita e sfruttare le proprie competenze.Per rispondere a questi requisiti, Marco Montali sta studiando come complementare iclassici linguaggi di specifica orientati al flusso di esecuzione (workflow) con approccidichiarativi e aperti [P.2], [P.1]. Dichiarativi, in modo da focalizzare l’attenzione delmodellista sui vincoli comportamentali che devono essere rispettati senza fissare uninsieme predeterminato e rigido di flussi di esecuzione corretti. Aperti, al fine di la-sciare ai partecipanti la liberta di effettuare un’azione se questa non e esplicitamentevietata, requisito fondamentale in ambienti in cui la conoscenza di ogni partecipante eincompleta e in continuo aggiornamento rispetto all’evolversi degli eventi.

Piu specificatamente, l’attivita di ricerca di Montali si focalizza sui seguenti temi:

• studio di linguaggi grafici per la specifica dei modelli di interazione, con partico-lare attenzione alla loro usabilita;

• sintesi di opportuni metodi di traduzione automatica per passare dalla rappre-sentazione grafica ad una corrispondente rappresentazione formale basata sullalogica;

11

• definizione e realizzazione di tecniche di ragionamento automatico per supportarela verifica, l’esecuzione e l’analisi di modelli di interazione lungo tutto il loro ciclodi vita;

• applicazione di questi linguaggi e strumenti nel campo dei processi aziendali,delle linee guida in campo medico, dei sistemi orientati ai servizi e agli agenti.

4.2 Logiche per la formalizzazione di modelli di interazione

Se da un lato e fondamentale che i modelli di interazione possano essere specificatida utenti esperti del dominio ma non tecnici, dall’altro e altrettanto importante chesiano dotati di una rappresentazione formale, che ne definisca una semantica precisa epermetta di applicare strumenti di ragionamento rigorosi. In quest’ottica, Marco Montalisi occupa di studiare l’applicazione di diversi framework logici per la formalizzazionedi modelli di interazione.

In [P.2], [P.1] e [P.3], e stato indagato l’uso del linguaggio SCIFF3 per specificaremodelli di interazione dichiarativi e aperti. SCIFF e un framework basato sulla pro-grammazione logica abduttiva, che permette di modellare l’interazione in sistemi basatisu eventi utilizzando regole (reattive) che vincolano il comportamento dei partecipanti,esprimendo cosa ci si aspetta che (non) avvenga a fronte del verificarsi di una determi-nata situazione. E dotato di una semantica dichiarativa che definisce formalmente ilconcetto di conformita di una esecuzione del sistema rispetto alle regole modellate, edha una elevata espressivita: supporta l’uso di variabili, che possono essere soggette avincoli CLP4 e predicati Prolog. La natura abduttiva del linguaggio si concilia con laconoscenza incompleta e sempre in aggiornamento che i partecipanti hanno del sistemadurante l’esecuzione. Al linguaggio sono associate diverse procedure di dimostrazioneche possono essere impiegate per effettuare verifiche statiche sul modello, per ragionarein tempo reale durante un’esecuzione del sistema o per effettuare analisi a posteriori.

L’attivita di Marco Montali si e focalizzata non solo sull’uso di SCIFF come linguag-gio di specifica, ma anche sulla comparazione con altri linguaggi logici utilizzati inletteratura, in particolare la logica temporale lineare (LTL). In [P.3], le due logiche sonoproposte come alternative alla modellazione dell’interazione, e vengono comparate daun punto di vista linguaggistico ma anche rispetto alle diverse forme di ragionamentoautomatico che permettono di supportare. [P.2] contiene invece un’indagine di naturateorica, che mette in relazione il concetto di entailment SCIFF con quello LTL e comparaformalmente l’espressivita delle due logiche.

Pur essendo un linguaggio molto ricco, SCIFF non permette di caratterizzare esplicita-mente gli stati in cui un’evoluzione del sistema si puo trovare, ne di modellare proprietache variano all’accadere di eventi. Questi requisiti sono invece coperti dal calcolo deglieventi5 (EC), uno dei piu noti framework logici, nell’ambito della rappresentazione della

3 M. Alberti, F. Chesani, M. Gavanelli, E. Lamma, P. Mello, and P. Torroni, Verifiable Agent Interaction inAbductive Logic Programming: the SCIFF framework. ACM Transactions on Computational Logic 9:4 (2008).

4 J. Jaffar and M. J. Maher. Constraint Logic Programming: a Survey. Logic Programming 19-20, pages503–582, 1994.

5 R. A. Kowalski and M. Sergot. A Logic-Based Calculus of Events. New Generation Computing 4:1, pages67–95, 1986.

12

conoscenza, per modellare e ragionare sulle azioni e i loro effetti. In letteratura sonostate proposte molte formalizzazioni di una moltitudine di varianti di EC. Purtroppo,gli approcci proposti non coprono tutte le forme di ragionamento del framework SCIFF,e in molti casi si tratta di implementazioni ad-hoc o soluzioni che ricorrono a costruttiextra-logici.

Al fine di combinare i vantaggi di SCIFF e EC, in [P.42], [P.14], [P.7], [P.9] MarcoMontali e colleghi hanno effettuato il primo (a nostra conoscenza) tentativo di assio-matizzare EC in termini reattivi senza ricorrere a costrutti extra-logici (Reactive EventCalculus, REC). In questo modo diviene possibile da un lato studiare le proprieta for-mali del calcolo (come correttezza, completezza e irrevocabilita), e dall’altro monitorarel’esecuzione di un sistema, generando dinamicamente l’andamento dei fluenti a frontedell’accadimento di nuovi eventi.

4.3 Business process management

In [P.2] e [P.1], Marco Montali ha proposto un framework chiamato CLIMB (Compu-tational Logic for the verIfication and Modeling of Business Constraints), il quale combinamodellazione grafica, linguaggi basati su logica computazionale e tecniche di ragiona-mento automatico per specificare rigorosamente modelli di interazione dichiarativi eaperti, e fornire supporto durante tutto il loro ciclo di vita.

CLIMB adotta una versione estesa del linguaggio grafico ConDec6 per specificarevincoli comportamentali sull’interazione. ConDec e un linguaggio per la specificaflessibile di processi di business. ConDec viene esteso considerando vincoli temporaliquantitativi (come scadenze, latenze e ritardi) e attivita non atomiche, nonche datie condizioni basate sui dati. Tutti i costrutti di ConDec (esteso) vengono tradotti intermini di regole SCIFF e teorie EC, rendendo possibile l’applicazione delle proceduredi ragionamento automatico legate a SCIFF anche a modelli ConDec.

In particolare, il ragionamento in CLIMB si appoggia su uina famiglia di procedure didimostrazione per effettuare verifiche statiche di proprieta (g-SCIFF proof procedure),monitoraggio (SCIFF proof procedure e EC) e process mining (SCIFF proof procedure,Prolog e algoritmi di programmazione logica induttiva).

verifica statica con g-sciff La verifica statica si applica ex ante, durante lafase di progetto, e mira a garantire la correttezza e consistenza dei modelli prodotti,individuando errori che, se scoperti a run-time, potrebbero essere molto difficili daaffrontare, se non addirittura compromettere il sistema. g-SCIFF segue un approcciosimulativo basato su abduzione, ovvero utilizza le regole che formalizzano il modellocercando di generare delle tracce di esecuzione che siano conformi con la specifica e nelcontempo rispettino (o violino) una proprieta (in)desiderata.

La fattibilita dell’uso di g-SCIFF per la verifica statica di modelli ConDec e statavalutata sia da un punto di vista teorico ([P.2], [P.1] e [P.5]) che da un punto di vistasperimentale, mediante la definizione di alcuni benchmark atti a valutarne prestazionie scalabilita e a compararne il comportamento con tecniche di satisfiability checking via

6 M. Pesic and W. M. P. van der Aalst. A Declarative Approach for Flexible Business Processes Management.In proceedings of the BPM 2006 Workshops, LNCS 4103, pages 169-180, 2006, Springer.

13

model checking, considerando model checkers espliciti e simbolici dello stato dell’arte,nonche tecniche basate su SAT ([P.3], [P.17], [P.43], [P.5]).

supporto all’esecuzione Processi di business complessi e che vedono la parteci-pazione di esperti umani presentano un alto grado di imprevedibilita: non e possibileprevedere a priori quali saranno i comportamenti effettivi dei partecipanti in un determi-nato contesto. Diventa quindi fondamentale la disponibilita di tecniche automatiche percontrollare costantemente un’evoluzione del sistema rilevando prontamente la presenzadi una deviazione dalle prescrizioni del modello desiderato.

Il linguaggio SCIFF e associato a una procedura di dimostrazione (denominata an-ch’essa SCIFF) che permette di acquisire dinamicamente o a posteriori le tracce diesecuzione di un sistema, verificando che esse rispettino effettivamente le regole specifi-cate. In [P.2] e [P.1] si e mostrato come l’uso congiunto di EC e SCIFF (REC) permetta dimonitorare in tempo reale l’esecuzione di un processo, calcolando dinamicamente l’im-patto degli eventi accaduti sui vincoli di business modellati e segnalando prontamenteeventuali violazioni.

process mining Una vasta gamma di sistemi basati su eventi (compresi tutti iprincipali business process management systems) memorizza gli eventi caratteristici delleproprie esecuzioni in un sistema informativo. Questi log di eventi possono essereanalizzati a posteriori al fine di estrarre informazioni utili agli analisti aziendali oal personale amministrativo, supportandoli nell’analisi dei trend comportamentalidell’azienda, nel decision making, nella revisione della propria struttura organizzativa enel miglioramento dei propri processi.

L’insieme di tecniche per l’estrazione di informazioni da log di eventi e detto processmining. In quest’ambito, Marco Montali e colleghi hanno lavorato principalmente sudue filoni:

• la classificazione delle tracce di esecuzione presenti nel log rispetto alla conformitacon regole di business;

• l’apprendimento di un modello dichiarativo (specificato in ConDec) a partireda un insieme di tracce precedentemente classificate come conformi o non con-formi rispetto a un certo criterio; il modello appreso e capace di discriminarecorrettamente i due insiemi.

Rispetto al primo punto, e stato definito un linguaggio pseudo-naturale ispirato a SCIFFe ConDec per specificare regole di business reattive (ECA-like). E stato poi implementatoun plug-in per ProM, uno dei piu noti framework di process mining, che permettedi configurare tali regole di business ed effettuare concretamente la classificazione.L’interfaccia grafica di configurazione delle regole e stata implementata in JAVA, mentreil motore di classificazione e stato realizzato in Prolog. Dettagli sul plug-in si trovano in[P.44], [P.29] e [P.1]. Lo strumento e stato testato in diversi ambiti applicativi. E stato inparticolare impiegato nell’ambito del progetto FIRB TOCAI.IT da parte di un’aziendaleader nel campo manifatturiero [P.29], e per l’analisi dei processi chimici in impianti didepurazione delle acque [P.45], come parte di un’architettura di complex event processingche combina tecniche di ragionamento sub-simboliche e simboliche [P.6].

14

Rispetto al secondo punto, in [P.47] e [P.15] e stato proposto un algoritmo di appren-dimento basato su programmazione logica induttiva definito per apprendere modelliConDec dalle tracce di esecuzione di un processo. L’algoritmo e capace di apprendereun modello SCIFF. grazie alla possibilita di rappresentare ConDec in SCIFF, un mecca-nismo di traduzione inversa viene infine applicato per ottenere una rappresentazionegrafica del modello appreso. In [P.10], viene presentato un framework di process miningdichiarativo che utilizza queste tecniche ed e stato effettivamente implementato comeplug-in per ProM. Il plug-in assiste l’utente nelle fasi di preparazione dei dati perl’algoritmo di apprendimento e si occupa di visualizzare i diagrammi prodotti.

4.4 Architetture orientate ai servizi

In [P.3], Montali e coautori hanno mostrato alcuni limiti critici nell’adozione di approcciprocedurali e chiusi (quali ad esempio WS-CDL) per la specifica di coreografie di servizi,mostrando come colmare questi limiti con DecSerFlow, un linguaggio grafico per laspecifica dichiarativa di vincoli di interazione tra servizi ispirato a ConDec. L’usabilitadi DecSerFlow e stata valutata ricorrendo alle dimensioni cognitive di Green7. Sonostati definiti inoltre opportuni metodi di traduzione automatica in termini di formuleLTL e regole SCIFF, mostrando punti di forza e debolezza di entrambi gli approcci.

SCIFF e stato proposto non solo come linguaggio per la formalizzazione di vincolicoreografici, ma anche per la specifica di interfacce comportamentali dei servizi, appli-cando le procedure di dimostrazione SCIFF e g-SCIFF per la verifica statica e dinamicadi composizioni di servizi.

discovery e contracting di (semantic) web services La ricerca e scopertadi servizi (web) e attualmente un tema molto importante nell’ambito delle architettureorientate ai servizi. A fronte di un aumento esponenziale del numero di servizi residisponibili sulla rete, infatti, sono necessari metodi intelligenti per recuperare queiservizi che davvero possono risolvere il compito richiesto. Questi strumenti sonoutili sia come base per la costruzione di motori di ricerca avanzata per gli utenti,che come nucleo centrale per il processo di composizione (dinamica) dei servizi. Alfine di rendere possibili tali tipologie di ricerca avanzata, numerosi autori stannoproponendo di estendere l’interfaccia esposta dai servizi con informazioni legate allaloro “semantica”, sia in termini del significato delle informazioni scambiate, che inrelazione al comportamento pubblico. Marco Montali e colleghi hanno indagato l’usodel framework SCIFF per esprimere le interfacce comportamentali dei singoli serviziweb e per effettuare ragionamento al fine di stabilire, a priori, se puo esistere o menoalmeno una forma di interazione tra due servizi, in base alle politiche di comportamentodegli enti coinvolti.

In [P.37], [P.39] e [P.27] viene presentato un framework per la verifica di interoperabi-lita tra servizi, in cui le interfacce comportamentali sono modellate in SCIFF e vengonocombinate per verificare l’esistenza di una possibilita di interazione che porti al soddi-sfacimento di un certo obiettivo rispettando nel contempo le politiche di interazione deisingoli partecipanti (contracting).

7 T.R.G. Green. Cognitive Dimensions of Notations. People and Computer V, pages 443–460, 1989.

15

In [P.18], queste idee vengono sviluppate nell’ottica di realizzare un framework perla scoperta di servizi in cui il matching tra i requisiti del cliente e i servizi disponibilinon viene effettuato unicamente in base all’interfaccia sintattica di invocazione (UDDI),ma anche in base a politiche comportamentali.

L’approccio e stato ulteriormente esteso in [P.38] e [P.16] introducendo anche proble-matiche di natura ontologica (quali ad esempio matching fra termini in base al significatoe non alla corrispondenza sintattica). La verifica di interoperabilita viene effettuataconsiderando quindi in un unico framework sia le politiche comportamentali che lasemantica dei termini. Il framework si basa su SCIFF per verificare le corrispondenzecomportamentali e su Pellet8 per risolvere problematiche di natura ontologica.

conformita rispetto a una coreografia Le coreografie di servizi rappre-sentano un contratto pubblico e condiviso da tutti i partecipanti, che regola i possibiliscambi di messaggi al fine di garantire una corretta collaborazione. Grazie alle coreogra-fie, aziende diverse possono mutuamente beneficiare dei servizi delle altre, definendo apriori le regole che ognuno e tenuto a rispettare. In quest’ottica, e importante fornirestrumenti di supporto per verificare se (l’interfaccia comportamentale di) un certoservizio concreto puo effettivamente prendere parte alla coreografia giocando un certoruolo, rispettando tutte le regole coreografiche che insistono su quel ruolo.

In [P.50], [P.52] e [P.19] e stato affrontato il problema della conformita di un servizio ri-spetto a una coreografia modellando sia la coreografia che l’interfaccia comportamentaledel servizio in termini di modello logici abduttivi SCIFF. Viene presentato uno nuovostrumento software denominato Allows9, che combina diverse tecniche di ragionamentoal fine di stabilire se il servizio puo assumere correttamente un certo ruolo nell’ambitodella coreografia, assumendo che tutti gli altri servizi si comportino come descrittodalla coreografia. Se il servizio passa il test di conformita, viene garantito che essopotra interagire correttamente con qualunque altro servizio conforme con la coreografia(per un altro ruolo). Il test e piu flessibile dei classici test di bisimilarita, nel senso chenon e necessario che il comportamento del servizio sia esattamente “sovrapponibile”con quello richiesto dalla coreografia.

In [P.3], [P.1] e [P.40] viene studiata una forma meno stringente di conformita. Iservizi e la coreografia sono rappresentati in questo caso in ConDec, e la verifica vieneeffettuata con la procedura g-SCIFF combinando le specifiche SCIFF della coreografia edel servizio, ottenute mediante la traduzione automatica definita in [P.3], [P.1]. Il test diconformita viene quindi effettuato su una completa composizione di servizi concretirispetto alla coreografia; se da un lato quindi il test ha validita meno generale rispettoa quello definito in [P.19], dall’altra parte garantisce maggiore flessibilitita, perchepermette di individuare composizioni di servizi che, pur non coprendo interamente laspecifica coreografica, possono correttamente interagire rispettandone le prescrizioni.

verifica in tempo reale e monitoraggio La verifica in tempo reale e il moni-toraggio sono temi di primaria importanza nell’ambito dei servizi. Anche in presenza diinformazioni statiche sul comportamento dei partecipanti, non si puo infatti essere certi

8 clarkparsia.com/pellet/9 Abductive Logic Web Service Specification

16

che l’interfaccia comportamentale pubblicata da un servizio corrisponda effettivamentealla sua implementazione interna.

In [P.26], il framework SCIFF viene utilizzato per verificare in tempo reale che i mes-saggi scambiati da un insieme di servizi rispettino effettivamente le regole coreograficheaccordate. L’approccio e stato esteso in [P.25] sfruttando il REC: il framework diventacapace di mostrare passo passo l’evolversi dei fluenti associati agli eventi del sistema;inoltre, le violazioni possono essere catturate esplicitamente (mediante un processo direificazione) ed utilizzate per generare allarmi o installare meccanismi di compensazione.

4.5 Sistemi multi-agente aperti

Nell’ambito dei sistemi multi-agente aperti10, Marco Montali si e occupato della specificae verifica di protocolli di interazione, con enfasi sugli aspetti normativi e di contrattotra gli agenti.

In [P.48] e [P.8], il framework SCIFF e stato applicato alla verifica di contratti, mo-strando la sua espressivita nella specifica di clausole contrattuali complesse, le tecnichedi inferenza e collegandone i costrutti a quelli della logica deontica.

La possibilita di formalizzare l’EC in termini di regole SCIFF ha fornito l’infrastrutturaper la modellazione, estensione e monitoraggio dei protocolli di interazione basati sucommitment11, ovvero sulle mutue obbligazioni che si vengono ad instaurare tra gliagenti durante l’esecuzione. Un commitment denota l’impegno che un agente debitoreprende verso un agente creditore per rendere vera una certa proprieta. La teoria deicommitment indica attraverso quali stati passa un commitment a fronte dell’accadere dicerti eventi.

In [P.14], Montali e coautori sono partiti dalla possibilita di assiomatizzare la teoria deicommitment in termini dell’EC12, estendendola con i concetti di deadline, per modellarecommitment in cui il debitore si impegna a rendere vera una proprieta entro un tempomassimo, e di compensazione derivante dalla violazione di tale tempo massimo. Vienequindi mostrato come l’uso di REC renda possibile acquisire dinamicamente gli eventiaccaduti durante l’interazione, calcolando reattivamente l’evolversi degli stati di ognicommitment. Vengono infine enunciate alcune proprieta formali del calcolo, tra le qualispicca l’irrevocabilita, ovvero la garanzia che i risultati calcolati da REC siano via viaestensioni (e non revisioni) dei precedenti, a patto che gli eventi acquisiti siano ordinatinel tempo.

In [P.30], la teoria dei commitment viene ulteriormente estesa considerando diversepossibili temporizzazioni per i commitment. Si differenziano in particolare commitmenttemporizzati esistenzialmente (per i quali la proprieta deve essere resa vera all’internodi un intervallo di tempo) e universialmente (per i quali la proprieta deve esserecontinuativamente mantenuta vera all’interno di un intervallo di tempo).

10 Sistemi multi-agente nei quali gli agenti interagiscono dinamicamente, entrando o uscendo dal sistemaliberamente, e nei quali non e quindi noto ne il numero di partecipanti, ne i loro dettagli implementativi.

11 C. Castelfranchi. Commitments: From Individual Intentions to Groups and Organizations. In Proceedingsof the First International Conference on Multiagent Systems (ICMAS1995), The MIT Press, pages 41–48, 1995.

12 P. Yolum and M. P. Singh. Flexible Protocol Specification and Execution: Applying Event CalculusPlanning Using Commitments. In Proceedings of the First International Joint Conference on AutonomousAgents & Multiagent Systems (AAMAS 2002), ACM Press, pages 527–534, 2002.

17

In [P.41], viene mostrata l’implementazione di un tool per il monitoraggio dei com-mitment, che sfrutta REC e SWI Prolog per la parte di ragionamento, e JAVA per laparte di acquisizione degli eventi e di visualizzazione dei risultati.

In [P.24], la proposta di formalizzazione presentata in [P.14] viene integrata con lostudio effettuato in [P.30]. Viene quindi descritto un framework per il monitoraggiodi protocolli basati su commitment temporizzati, dalla teoria (assiomatizzazione dellateoria dei commitment temporizzati nell’EC) alla pratica (uso di REC e dello strumentopresentato in [P.41]). L’articolo risulta vincitore del Best Paper Award.

Il monitoraggio delle interazioni fra agenti viene ulteriormente esteso in [P.33] rispettoal concetto di ruolo. In particolare, viene impiegato l’EC per modellare i ruoli e le lorodinamiche nel tempo. L’appartenenza ad un ruolo in un certo istante di tempo vieneutilizzata in combinazione con regole SCIFF per modellare regole comportamentali,aspettative, obbligazioni e divieti che devono essere rispettate dagli agenti in virtu deiloro ruoli.

La presentazione invitata [P.34] raccoglie le varie attivita di ricerca di Marco Montalie colleghi su questi temi.

4.6 Combinazione di approcci orientati agli agenti, servizi e processi

Marco Montali si e occupato di individuare punti di contatto e sinergie tra i sistemimulti-agente aperti e i sistemi orientati ai servizi e ai processi. Tali sistemi presentanosovente problematiche simili, le quali possono essere affrontate con successo medianteapprocci integrati.

In [P.49] e [P.7], approcci basati su vincoli di business e commitments vengonocombinati per modellare le coreografie di servizi in maniera flessibile e dinamica.I vincoli forti sull’esecuzione di attivita vengono rappresentati utilizzando ConDec,mentre i commitments vengono adottati per trattare le mutue obbligazioni tra servizi,nonche i protocolli di compensazione che scaturiscono da situazioni eccezionali oindesiderate. SCIFF e l’EC vengono utilizzati come formalismo unificante per trattareentrambi gli aspetti.

In [P.46], [P.28] e [P.4], si e affrontato il problema della rappresentazione e verificadi sistemi software orientati agli agenti, considerando sia aspetti legati ai requisiti eagli obiettivi degli agenti, che una dimensione di processo. Dal punto di vista lin-guaggistico, il problema viene affrontato utilizzando il linguaggio Tropos13, esteso convincoli comportamentali espressi in ConDec, con aspetti temporali e con la possibilitadi specificare condizioni guidate dai dati. In [P.4], viene utilizzata la procedura didimostrazione g-SCIFF per verificare staticamente la correttezza e l’eseguibilita dellespecifiche modellate; in particolare, vengono investigate le proprieta formali dell’ap-proccio, identificando una classe di specifiche per le quali e garantita la terminazionedel verificatore.

13 P. Bresciani, P. Giorgini, F. Giunchiglia, J. Mylopoulos, and A. Perini. TROPOS: An Agent-OrientedSoftware Development Methodology. Journal of Autonomous Agents and Multi-Agent Systems 8(3), pages203–236, 2004.

18

4.7 Linee guida in campo medico e protocolli di cura

L’attivita di ricerca nel campo delle linee guida in campo medico e cominciata perMarco Montali ancor prima del conseguimento della Laurea Specialistica, durante unprogetto SPINNER di trasferimento tecnologico. Nell’ambito del progetto, si e occupatodella rappresentazione di protocolli di cura e della verifica di conformita del personalesanitario rispetto alle specifiche modellate. Un primo studio preliminare su questi temisi puo trovare in [P.22].

Durante il progetto SPINNER e la tesi di Laurea Specialistica [P.53], Montali ha inoltredefinito un nuovo linguaggio grafico per la specifica della dimensione di processonelle linee guida. Il linguaggio e denominato GOSpeL (Guideline prOcess SpecificationLanguage) ed e un linguaggio di workflow strutturato, comprendente attivita atomiche,sottoprocessi, sequenze, cicli, rami in alternativa e sezioni parallele. Le singole attivitaed i relativi dati e partecipanti sono modellati utilizzando ontologie di dominio definitedi volta in volta dall’utente.

In [P.51] e [P.21], Montali e coautori hanno proposto un algoritmo di traduzione capacedi analizzare protocolli di cura specificati in GOSpeL e produrre automaticamente inuscita una corrispondente rappresentazione formale basata sul framework SCIFF. Intal modo, SCIFF puo essere impiegato per verificare a run-time il comportamentodel personale sanitario, o per analizzare a posteriori le tracce di esecuzione relativeall’applicazione passata della linea guida su una serie di pazienti. Un prototipo softwareper la specifica e la traduzione automatica di modelli GOSpeL e stato implementato inJAVA, appoggiandosi sulle librerie di Protege14 per la parte ontologica.

L’architettura completa del sistema risultante, denominata GPROVE (Guideline PRocesscOnformance VErification), e presentata in [P.23], mentre in [P.13] viene presentatoun caso di studio reale, in cui GPROVE viene applicato nel contesto del protocollodi prevenzione del tumore della cervice uterina in Emilia Romagna, allo scopo diverificare l’aderenza delle sue esecuzioni concrete rispetto alle prescrizioni definitedall’organizzazione sanitaria regionale.

In [P.31], GPROVE viene comparato con GLARE15, allo scopo di identificarne punti dicontatto e differenze, e gettare quindi le basi per un approccio integrato. La valutazionedelle due proposte e stata condotta utilizzando una metodologia nota in letteratura.

Piu recentemente, l’attivita di ricerca di Montali nel campo delle linee guida si efocalizzata sull’integrazione di linguaggi di rappresentazione procedurali e dichiarativi,considerando non solo le prescrizioni definite nei documenti di raccomandazioneprodotti dalle organizzazioni sanitarie, ma anche la conoscenza medica di brackground.Una prima proposta in tal senso si trova in [P.20]. L’obiettivo ultimo di questa ricerca equello di fornire a medici e operatori sanitari degli strumenti di supporto alle decisioniche riescano a mediare controllo e flessibilita, permettendo di combinare le prescrizionigeneriche date dalle linee guida con il contesto e la situazione specifica di ogni paziente.

14 http://protege.stanford.edu15 P. Terenziani, S. Montani, A. Bottrighi, G. Molino, M. Torchio. Applying Artificial Intelligence to Clinical

Guidelines: the GLARE Approach. in Computer-Based Medical Guidelines and Protocols: a Primer and CurrentTrends, IOS Press, 2008.

19

5. pubblicazioni

5.1 Libri

[P.1] Marco Montali. Specification and Verification of Declarative Open Interaction Models: aLogic-Based Approach. Vol. 56 of Lecture Notes in Business Information Processing,Springer, 2010.

5.2 Tesi di Dottorato

[P.2] Marco Montali. Specification and Verification of Declarative Open Interaction Models: aLogic-Based Approach. Tesi di Dottorato, Dipartimento di Elettronica, Informaticae Sistemistica, Universita di Bologna, 2009.http://amsdottorato.cib.unibo.it/1829/

5.3 Riviste internazionali

[P.3] Marco Montali, Maja Pesic, W. M. P. van der Aalst, Federico Chesani, Paola Mello,and Sergio Storari. Declarative Specification and Verification of Service Choreographies.ACM Transactions on the Web, Vol. 4(1), 2010.Impact factor: 2.812.

[P.4] Marco Montali, Paolo Torroni, Nicola Zannone, Paola Mello, and Volha Bryl.Engineering and Verifying Agent-Oriented Requirements augmented by Business Con-straints with B-Tropos. Journal of Autonomous Agents and Multi-Agent Systems,Springer, 2010.Impact factor: 2.125.

[P.5] Marco Montali, Paolo Torroni, Marco Alberti, Federico Chesani, Evelina Lamma,and Paola Mello. Abductive Logic Programming as an Effective Technology for theStatic Verification of Declarative Business Processes. Special Issue of FundamentaInformaticae, 102 (3-4) 325–361, IOS Press.

[P.6] Luca Luccarini, Gianni Luigi Bragadin, Gabriele Colombini, Maurizio Mancini,Paola Mello, Marco Montali, and Davide Sottara. Formal Verification of WastewaterTreatment Processes using Events detected from continuous signals by means of ArtificialNeural Networks. Environmental Modelling and Software, 2009.Impact factor: 2.099.

[P.7] Federico Chesani, Paola Mello, Marco Montali, Sergio Storari, and Paolo Torroni.On the Integration of Declarative Choreographies and Commitment-based Agent Societiesinto the SCIFF Logic Programming Framework. Multiagent and Grid Systems,Special Issue on Agents, Web Services and Ontologies: Integrated Methodologies,6(2), 2010.

[P.8] Marco Alberti, Federico Chesani, Marco Gavanelli, Evelina Lamma, Paola Mello,Marco Montali, and Paolo Torroni. Expressing and Verifying Contracts with Abductive

20

Logic Programming. International Journal of Electronic Commerce, Special Issueon Contract Architectures and Languages, 12(4):9–38, 2008.Impact factor: 1.186.

[P.9] Federico Chesani, Paola Mello, Marco Montali, and Paolo Torroni. A Logic-Based,Reactive Calculus of Events. Special Issue of Fundamenta Informaticae, 104 1–27,IOS Press. In Press.

[P.10] Federico Chesani, Evelina Lamma, Paola Mello, Marco Montali, Fabrizio Riguzzi,and Sergio Storari. Exploiting Inductive Logic Programming Techniques for DeclarativeProcess Mining. LNCS Transactions on Petri Nets and Other Models of Concur-rency (ToPNoC), Special Issue on Concurrency in Process-Aware InformationSystems, 5460:278–295, 2009.

5.4 Riviste a diffusione internazionale

[P.11] Federico Chesani, Paola Mello, Marco Montali, and Paolo Torroni. Modeling andVerification of Business Processes and Choreographies in ALP. Il Milione – A Journeyin the Computational Logic in Italy, Proceedings of the Day Dedicated to Prof.Alberto Martelli, Special Issue of Intelligenza Artificiale, IOS Press. In Press.

[P.12] M. Baldoni, C. Baroglio, G. Berio, A. Martelli, V. Patti, M.L. Sapino, C. Schi-fanella, M. Alberti, M. Gavanelli, E. Lamma, F. Riguzzi, S. Storari, F. Chesani,A. Ciampolini, P. Mello, M. Montali, P. Torroni, A. Bottrighi, G. Casella, L. Gior-dano, V. Gliozzi, V. Mascardi, G. Pozzato, P. Terenziani, and D. Theseider Dupre.Web Service-Oriented Modeling, Verification and Reasoning Techniques. IntelligenzaArtificiale, IOS Press. In Press.

5.5 Contributi su libro

[P.13] Federico Chesani, Evelina Lamma, Paola Mello, Marco Montali, Sergio Storari,Paola Baldazzi, and Marilena Manfredi. Compliance Checking of Cancer-ScreeningCareflows: an Approach Based on Computational Logic. In A. ten Teije, S. Miksch, andP. Lucas, editors, Computer-Based Medical Guidelines and Protocols: a Primerand Current Trends. IOS Press, 2008.

5.6 Atti di conferenze e workshop

[P.14] Federico Chesani, Paola Mello, Marco Montali, and Paolo Torroni. CommitmentTracking via the Reactive Event Calculus. In C. Boutilier, editor, Proceedings of the21th International Joint Conference on Artificial Intelligence (IJCAI-09), pages91–96, 2009.ISBN: 978-1-57735-426-0. Acceptance rate: 25.7%.

[P.15] Evelina Lamma, Paola Mello, Marco Montali, Fabrizio Riguzzi, and Sergio Storari.Inducing Declarative Logic-Based Models from Labeled Traces. In M. Rosemann and

21

M. Dumas, editors, Proceedings of the 5th International Conference on BusinessProcess Management (BPM 2007), Vol. 4714 of LNCS, pages 344–359. SpringerVerlag, 2007.ISBN: 978-3-540-75182-3. Acceptance rate: 15%.

[P.16] Marco Alberti, Massimiliano Cattafi, Federico Chesani, Marco Gavanelli, EvelinaLamma, Paola Mello, Marco Montali, and Paolo Torroni. Integrating AbductiveLogic Programming and Description Logics in a Dynamic Contracting Architecture. Pro-ceedings of the 7th IEEE International Conference on Web Services (ICWS2009),pages 254–261, 2009.ISBN: 978-3-642-04929-3. Acceptance rate: 15.6%.

[P.17] Marco Montali, Paolo Torroni, Marco Alberti, Federico Chesani, Marco Gavanelli,Evelina Lamma, and Paola Mello. Verification from Declarative Specifications UsingLogic Programming. In M. Garcia De La Banda and E. Pontelli, editors, 24thInternational Conference on Logic Programming (ICLP2008), Vol. 5366 of LNCS,pages 440–454. Springer, 2008.ISBN: 978-3-540-89981-5. Acceptance rate: 35.6%.

[P.18] Marco Alberti, Federico Chesani, Marco Gavanelli, Evelina Lamma, Paola Mello,Marco Montali, and Paolo Torroni. Web Service contracting: Specification and Reaso-ning with SCIFF. In E. Franconi, M. Kifer, and W. May, editors, Proceedings of the4th European Semantic Web Conference (ESWC’07), Vol. 4519 of LNAI, pages68–83. Springer Verlag, 2007.ISBN: 978-3-540-72666-1. Acceptance rate: 17%.

[P.19] Marco Alberti, Federico Chesani, Marco Gavanelli, Evelina Lamma, Paola Mello,and Marco Montali. An Abductive Framework for A-Priori Verification of Web Services.In A. Bossi and M. J. Maher, editors, Proceedings of the 8th International ACMSIGPLAN Conference on Principles and Practice of Declarative Programming(PPDP2006), pages 39–50. ACM Press, 2006.ISBN: 1-59593-388-3.

[P.20] Alessio Bottrighi, Federico Chesani, Paola Mello, Gianpaolo Molino, Marco Mon-tali, Stefania Montani, Sergio Storari, Paolo Terenziani, Mauro Torchio. A HybridApproach to Clinical Guideline and to Basic Medical Knowledge Conformance. In C. Com-bi, Y. Shahar and A. Abu-Hanna, editors, Proceedings of the 12th InternationalConference on Artificial Intelligence in Medicine (AIME 2009), Vol. 5651 ofLNCS, pages 91–95. Springer, 2009.ISBN: 978-3-642-02975-2.

[P.21] Federico Chesani, Paola Mello, Marco Montali, and Sergio Storari. Testing CareflowProcess Execution Conformance by Translating a Graphical Language to ComputationalLogic. In R. Bellazzi, A. Abu-Hanna, and J. Hunter, editors, Proceedings of the11th International Conference on Artificial Intelligence in Medicine (AIME’07),Vol. 4594 of LNCS, pages 479–488. Springer, 2007.ISBN: 978-3-540-73598-4. Acceptance rate: 20%.

22

[P.22] Anna Ciampolini, Paola Mello, Marco Montali, and Sergio Storari. Using SocialIntegrity Constraints for On-the-Fly Compliance Verification of Medical Protocols. InA. Tsymbal and P. Cunningham, editors, In Proceedings of the 18th IEEE Sym-posium on Computer Based Medical Systems (CBMS’05), pages 503–505. IEEEComputer Society, 2005.ISBN: 0-7695-2355-2.

[P.23] Federico Chesani, Pietro De Matteis, Paola Mello, Marco Montali, and SergioStorari. A Framework for Defining and Verifying Clinical Guidelines: a Case Study onCancer Screening. In F. Esposito, Z. W. Ras, D. Malerba, and G. Semeraro, editors,Proceedings of the 16th International Symposium on Foundations of IntelligentSystems (ISMIS 2006), Vol. 4203 of LNAI, pages 338–343. Springer, 2006.ISBN: 3-540-45764-X.

[P.24] Federico Chesani, Paola Mello, Marco Montali, and Paolo Torroni. MonitoringTime-Aware Social Commitments with Reactive Event Calculus. In Proceedings of the7th International Symposium “From Agent Theory to Agent Implementation”,Austrian Cybernetics Studies, 2010.Best Paper Award.

[P.25] Federico Chesani, Paola Mello, Marco Montali, and Paolo Torroni. Verificationof Choreographies During Execution Using the Reactive Event Calculus. In R. Bruni,K. Wolf, editors, Proceedings of the 5th International Workshop on Web Serviceand Formal Methods (WS-FM2008), volume 5387 of LNCS, pages 129–140. Sprin-ger, 2009.ISBN: 978-3-642-01363-8. Acceptance rate: 40.5%.

[P.26] Marco Alberti, Federico Chesani, Evelina Lamma, Marco Gavanelli, Paola Mello,Marco Montali, Sergio Storari, and Paolo Torroni. Computational Logic for theRun-time Verification of Web Service Choreographies: Exploiting the SOCS-SI Tool.In M. Bravetti, M. Nunez, and G. Zavattaro, editors, Proceedings of the 3rdInternational Workshop on Web Services and Formal Methods (WS-FM’06),volume 4184 of LNCS, pages 58–72. Springer, 2006.ISBN: 3-540-38862-1. Acceptance rate: 37%.

[P.27] Marco Alberti, Federico Chesani, Marco Gavanelli, Evelina Lamma, Paola Mello,Marco Montali, and Paolo Torroni. A Rule-Based Approach for Reasoning aboutCollaboration between Smart Web-Services. In M. Marchiori, J. Z. Pan, and C. de Sain-te Marie, editors, Proceedings of the First International Conference on WebReasoning and Rule Systems (RR’07), Vol. 4524 of LNAI, pages 279–288. Sprin-ger, 2007.ISBN: 978-3-540-72981-5.

[P.28] Volha Bryl, Paola Mello, Marco Montali, Paolo Torroni, and Nicola Zannone.B-Tropos: Agent-Oriented Requirements Engineering Meets Computational logic forDeclarative Business Process Modeling and Verification. In F. Sadri and K. Satoh,editors, Post-Proceedings of the 8th International Workshop on Computational

23

Logic in Multi-Agent Systems (CLIMA-VIII), Revised Selected and Invited Pa-pers, Vol. 5056 of LNCS, pages 157–176. Springer, 2009.ISBN: 978-3-540-88832-1.

[P.29] Federico Chesani, Paola Mello, Marco Montali, Fabrizio Riguzzi, Maurizio Seba-stianis, and Sergio Storari. Checking Compliance of Execution Traces to Business Rules.In D. Ardagna and M. Mecella and J. Yang, editors, International Workshop onBusiness Intelligence, Proceedings of BPM 2008 Workshops, Vol. 17 of LNBIP,pages 134–145, Springer, 2009.ISBN: 978-3-642-00327-1.

[P.30] Paolo Torroni, Federico Chesani, Paola Mello, and Marco Montali. Social Commit-ments in Time: Satisfied or Compensated. In M. Baldoni, J. Bentahar, J. Lloyd, M. Birnavan Riemsdijk, editors, Post-proceedings of the 7th International Workshop onDeclarative Agent Languages and Technologies (DALT 2009) - Selected Revisedand Invited Papers, Vol. 5948 of LNAI, pages 228–243. Springer, 2010.ISBN: 978-3-642-11354-3.

[P.31] Alessio Bottrighi, Federico Chesani, Paola Mello, Marco Montali, Stefania Montani,Sergio Storari and Paolo Terenziani. Analysis of the GLARE and GPROVE approachesto Clinical Guidelines. In D. Riano, A. ten Teije, editors, Proceedings of the Work-shop on Knowledge Representation for Health-Care: Patient Data, Processesand Guidelines (KR4HC 2009), Vol. 5943 of LNCS, pages 76–87. Springer, 2010.ISBN: 978-3-642-11807-4.

[P.32] Stefano Bragaglia, Federico Chesani, Anna Ciampolini, Paola Mello, Marco Monta-li, and Davide Sottara. An Hybrid Architecture Integrating Forward Rules with FuzzyOntological Reasoning. In Proceedings of the 5th International Conference onHybrid Artificial Intelligence Systems (HAIS 2010), Vol. 6076 of LNCS, Springer,2010.ISBN: 978-3-642-13768-6.

[P.33] Federico Chesani, Paola Mello, Marco Montali, and Paolo Torroni. Role Mo-nitoring in Open Agent Societies. In Proceedings of the 4th KES InternationalSymposium on Agent and Multi-Agent Systems: Technologies and Applica-tions (KES-AMSTA 2010), Vol. 6070 of LNCS, Springer, 2010.ISBN: 978-3-642-13479-1.

[P.34] Federico Chesani, Paola Mello, Marco Montali, and Paolo Torroni. DeclarativeTechnologies for Open Agent Systems and Beyond. In Proceedings of the 4th KESInternational Symposium on Agent and Multi-Agent Systems: Technologiesand Applications (KES-AMSTA 2010), Vol. 6070 of LNCS, Springer, 2010.ISBN: 978-3-642-13479-1.

[P.35] Marco Alberti, Federico Chesani, Marco Gavanelli, Evelina Lamma, Paola Mello,Marco Montali, Sergio Storari, and Paolo Torroni. A Computational Logic-BasedApproach to Verification of IT Systems. In H. G. Hegering, H. Reiser, M. Schiffers, andTh. Nebe, editors, Proceedings of the 14th Annual Workshop of HP Software Uni-versity Association. HP Software University Association, Infonomics-Consulting,

24

2007.ISBN: 978-3-000-21690-9.

[P.36] Marco Alberti, Federico Chesani, Anna Ciampolini, Paola Mello, Marco Montali,Sergio Storari, and Paolo Torroni. Protocol Specification and Verification by UsingComputational Logic. In F. Corradinin, F. de Paoli, E. Merelli, and A. Omicini,editors, Proceedings of the 6th AI*IA/TABOO Joint Workshop “From Objects toAgents” (WOA 2005), pages 184–192. Pitagora Editrice Bologna, 2005.ISBN: 88-371-1590-3.

[P.37] Marco Alberti, Federico Chesani, Evelina Lamma, Marco Gavanelli, Paola Mello,Marco Montali, and Paolo Torroni. Policy-Based Reasoning for Smart Web Service In-teraction. In A. Polleres, S. Decker, G. Gupta, and J. de Brujin, editors, Proceedingsof the First International Workshop on Applications of Logic Programming inthe Semantic Web and Semantic Web Services (ALPSWS2006), Vol. 196 of CEURWorkshop Proceedings, pages 87–102, 2006.Acceptance rate (full length presentations): 46%.

[P.38] Federico Chesani, Paola Mello, Marco Montali, and Paolo Torroni. OntologicalReasoning and Abductive Logic Programming for Service Discovery and Contracting.In A. Gangemi, J. Keizer, V. Presutti, and H. Stoermer, editors, 5th Workshopon Semantic Web Applications and Perspectives (SWAP2008), Vol. 429 of CEURWorkshop Proceedings, 2009.

[P.39] Marco Alberti, Federico Chesani, Marco Gavanelli, Evelina Lamma, Paola Mello,Marco Montali, and Paolo Torroni. Policy-Based Reasoning for Smart Web ServiceInteraction. In G. Tummarello, editor,Proceedings of the 3rd Workshop on Seman-tic Web Applications and Perspectives (SWAP’06), Vol. 201 of CEUR WorkshopProceedings, 2006.

[P.40] Federico Chesani, Paola Mello, Marco Montali and Paolo Torroni. Verifyinga-Priori the Composition of Declarative Specified Services. In Proceedings of the2nd Multi-Agent Logics, Languages, and Organisations Federated Workshops(MALLOW), International Workshop on Agents, Web Services and Ontologies,Integrated Methodologies, 2009. Vol. 494 of CEUR Workshop Proceedings.

5.7 Altre conferenze e workshop con revisione

[P.41] Federico Chesani, Paola Mello, Marco Montali and Paolo Torroni. A REC-BasedCommitment Tracking Tool (demo paper). 10th AI*IA/TABOO Joint Workshop“From Objects to Agents” (WOA 2009), 2009.

[P.42] Federico Chesani, Paola Mello, Marco Montali and Paolo Torroni. A Logic-Based,Reactive Calculus of Events. 24mo Convegno Italiano di Logica Computazionale(CILC 2008), 2009.

[P.43] Marco Montali, Paolo Torroni, Marco Alberti, Federico Chesani, Marco Gava-nelli, Evelina Lamma, and Paola Mello. Verification from Declarative Specifications

25

Using Logic Programming. 15th RCRA workshop: Experimental evaluation ofalgorithms for solving problems with combinatorial explosion, 2008.

[P.44] Marco Montali, Paola Mello, Federico Chesani, Fabrizio Riguzzi, Maurizio Seba-stianis, and Sergio Storari. Compliance Checking of Execution Traces to Business Rules:an Approach Based on Logic Programming. 23esimo Convegno Italiano di LogicaComputazionale (CILC 2008), 2008.

[P.45] Luca Luccarini, Gianni Luigi Bragadin, Gabriele Colombini, Maurizio Mancini,Paola Mello, Marco Montali, and Davide Sottara. Process Quality Assessmentin Automatic Management of Wastewater Treatment Plants Using Formal Verification.Simposio Internazionale di Ingegneria Sanitaria Ambientale (SIDISA 2008),2008.

[P.46] Volha Bryl, Paola Mello, Marco Montali, Paolo Torroni, and Nicola Zannone. Exten-ding Agent-oriented Requirements with Declarative Business Processes: a ComputationalLogic-based Approach. 22esimo Convegno Italiano di Logica Computazionale(CILC 2007), 2007.

[P.47] Evelina Lamma, Paola Mello, Marco Montali, Fabrizio Riguzzi, and Sergio Storari.Learning DecSerFlow Models from Labeled Traces. First International Workshop onthe Induction of Process Models, 2007.

[P.48] Marco Alberti, Federico Chesani, Marco Gavanelli, Evelina Lamma, Paola Mello,Marco Montali e Paolo Torroni. Expressing and verifying contracts with abductive logicprogramming. Dagstuhl Seminar on Normative Multi-agent Systems. A cura diG. Boella, L. van der Torre, e H. Verhagen. Dagstuhl Seminar Proceedings 07122,2007.

[P.49] Federico Chesani, Paola Mello, Marco Montali, and Sergio Storari. Agent Societiesand Service Choreographies: a Declarative Approach to Specification and Verification.International Workshop on Agents, Web-Services and Ontologies: IntegratedMethodologies (AWESOME’007), 2007.

[P.50] Federico Chesani, Paola Mello, Marco Montali, Marco Alberti, Marco Gavanelli,Evelina Lamma, and Sergio Storari. Abduction for Specifying and Verifying WebService Choreographies. 4th International Workshop on AI for Service Compo-sition (AISC 2006), co-located with the 17th European Conference on ArtificialIntelligence (ECAI’06), 2006.

[P.51] Federico Chesani, Anna Ciampolini, Paola Mello, Marco Montali, and SergioStorari. Testing Guidelines Conformance by Translating a Graphical Language to Com-putational Logic. Workshop on AI Techniques in Healthcare: Evidence-BasedGuidelines and Protocols, co-located with the 17th European Conference onArtificial Intelligence (ECAI’06), 2006.

[P.52] Marco Alberti, Federico Chesani, Marco Gavanelli, Evelina Lamma, Paola Mello,and Marco Montali. A-priori Verification of Web Services with Abduction. 21esimoConvegno Italiano di Logica Computazionale (CILC2006), 2006.

26

5.8 Tesi di laurea

[P.53] Marco Montali. Un linguaggio grafico per la specifica e la verifica di protocolli. Tesi dilaurea specialistica, Universita di Bologna, 2005.

[P.54] Marco Montali. Modellazione dell’interazione nei sistemi multi-agente. Tesi di laurea,Universita di Bologna, 2003.

5.9 Articoli in fase di revisione

[P.55] Federico Chesani, Paola Mello, Marco Montali, and Paolo Torroni. MonitoringSocial Commitments. Artificial Intelligence.

[P.56] Massimiliano Cattafi, Federico Chesani, Marco Gavanelli, Evelina Lamma, PaolaMello, Marco Montali, and Paolo Torroni. A Computational Logic ApplicationFramework for Service Discovery and Contracting. International Journal of WebServices Research.

[P.57] Federico Chesani, Paola Mello, Marco Montali, Paolo Torroni. Monitoring Time-Aware Commitments Inside Agent-Based Simulation Environments. Special issue ofCybernetics and Systems.

27

6. attivita didattica

Negli ultimi sette anni, Marco Montali ha svolto un’attivita didattica differenziatae costante, nell’ambito dei C.d.L. triennale e specialistica/magistrale in IngegneriaInformatica e Ingegneria dell’Automazione, nonche in ambito aziendale.Dal 2006 segue con costanza la stesura di tesi di laurea in qualita di co-relatore.

2005–oggi Tiene seminari, lezioni, esercitazioni in aula ed in laboratorio per i corsidi Fondamenti di Intelligenza Artificiale L-S e di Applicazioni di In-telligenza Artificiale L-S, nell’ambito del C.d.L. specialistica/magistrale diIngegneria Informatica.I corsi vertono sui principi e i metodi che stanno alla base della risoluzionedi problemi di Intelligenza Artificiale, con riferimento a sistemi basatisulla conoscenza e metodologie basate sulla logica.

2009–oggi Svolge attivita seminariale e di formazione aziendale presso Imagelines.r.l., azienda leader nella realizzazione di applicazioni web, softwaree portali informativi e redazionali nel settore agricolo ed agronomico.Trasferisce conoscenze relative ai modelli di sviluppo del software e allosviluppo del software orientato agli oggetti, ai linguaggi orientati aglioggetti (JAVA in particolare), al linguaggio UML e alla documentazionedi analisi e progetto, ai pattern architetturali e ai meccanismi di object-relational mapping.

2008/2009 Professore a contratto, nel ruolo di tutor, per il corso di Fondamentidi Informatica e Laboratorio T-AB nell’ambito del C.d.L. di Ingegneriadell’Automazione. Attivita svolta: tiene le esercitazioni in laboratorio, ed ecoadiutore durante gli esami di profitto degli studenti. Il corso introduceall’uso di linguaggi di programmazione di alto livello e relativi ambientidi sviluppo, e mira a trasferire competenze di analisi, specifica e sintesi dialgoritmi nonche di analisi, specifica e progetto, orientati agli oggetti, disistemi software.

Professore a contratto, nel ruolo di tutor, per il corso di Fondamenti diInformatica T-1 nell’ambito del C.d.L. di Ingegneria Informatica. Attivitasvolta: tiene le esercitazioni in laboratorio, ed e coadiutore durante gliesami di profitto degli studenti. Il corso discute le problematiche generaliconnesse alla programmazione in-the-small nel linguaggio imperativo C,ed e affiancato da un ampio set di esercitazioni pratiche di laboratorio, incui gli studenti sono seguiti nelle attivita proposte.

2006–2008 Professore a contratto, nel ruolo di tutor, per il corso di Laboratorio diInformatica L-A nell’ambito del C.d.L. di Ingegneria Informatica. Attivitasvolta: tiene parte delle esercitazioni di laboratorio ed e coadiutore durantegli esami di profitto degli studenti. Le tematiche principali del corso sonoi principi e gli strumenti di base della programmazione, insegnare adesprimere la soluzione di un piccolo problema (algoritmo) e codificarlo

28

in un linguaggio di programmazione (linguaggio C), presentare comecostruire un singolo progetto software che rispecchi una certa specifica.

03/’04 – 05/’06 Professore a contratto, nel ruolo di tutor, per il corso di Sistemi OperativiL-A nell’ambito del C.d.L. di Ingegneria Informatica. Attivita svolta: tiene leesercitazioni in laboratorio ed e coadiutore durante gli esami di profittodegli studenti. Il corso mira a fornire alcuni concetti fondamentali dellateoria dei Sistemi Operativi, nonche ad illustrare le caratteristiche di unsistema operativo reale (Unix/Linux) e gli strumenti a disposizione diutenti e programmatori per il suo utilizzo. La parte di laboratorio riguardaprincipi di programmazione shell e file comandi, programmazione inC/Unix con system call, file system Unix, segnali, pipe, Java thread.

29

7. altre competenze

7.1 Linguaggi ed ambienti di sviluppo

Padroneggia i seguenti linguaggi:

• Java, C#, SQL

• C, C/Unix, Unix Shell

• Prolog, CLP

• UML, BPMN

• XML, XPATH, XSL, (X)HTML, CSS

• Javascript, JQuery, JSP, Coldfusion 9

• LATEX

Padroneggia i seguenti framework ed ambienti di sviluppo:

• tecnologie ORM (in particolare Hibernate)

• SQL Server

• Eclipse, NetBeans, Visual Studio 2008 e precedenti

• SICStus Prolog, SWI-Prolog

Sistemi operativi: MacOs X, Windows NT/2K/XP/Vista, Linux.

7.2 Altre esperienze

Nel 2004 partecipa, in gruppo con altri tre studenti, al concorso Imagine Cup Italia,concorso nazionale organizzato dalla Microsoft e inerente lo sviluppo di soluzionisoftware innovative in grado di migliorare la qualita della vita. Il suo gruppo siclassifica quarto.

30

8. referenze

• Prof. Paola MelloDipartimento di Elettronica, Informatica e SistemisticaUniversita degli Studi di BolognaViale Risorgimento, 2

40136, BolognaTel.: +39 051 20 93818

Fax: +39 051 20 93073

E-mail: paola.mello@unibo.it

• Prof. Robert KowalskiDepartment of ComputingImperial College180 Queen’s Gate, LondonSW7 2BZ, UKE-mail: r.kowalski@imperial.ac.uk

• Prof. Wil M. P. van der AalstDepartment of Mathematics and Computer ScienceTU/e - Technische Universiteit EindhovenP.O. Box 513, NL-5600 MBEindhoven, The NetherlandsE-mail: w.m.p.v.d.aalst@tue.nl

• Prof. Matteo BaldoniDipartimento di InformaticaUniversita degli Studi di TorinoCorso Svizzera, 185

10149, TorinoTel.: +39 011 670 67 56

Fax: +39 011 75 16 03

E-mail: baldoni@di.unito.it

• Prof. Evelina LammaDipartimento di IngegneriaUniversita degli Studi di FerraraVia Saragat, 1

44100, FerraraTel.: +39 0532 97 4894

Fax: +39 0532 97 4870

E-mail: evelina.lamma@unife.it

31