Notizie
Course material will be made available on the Sapienza e-learning platform: https://elearning.uniroma1.it/ .
Information about courses is available under the label "Insegnamenti".
Exam schedules (including "appelli straordinari") are in Infostud.
You may contact me at: tronci@di.uniroma1.it .
Laurea Triennale in Informatica
FALL Semester
Ingegneria del Software (SE) - AA 2024/25.
Codice OPIS: L6W7560F
All info about the course syllabus, material, exams, and projects will be available on the Sapienza e-learning platform: https://elearning.uniroma1.it/ under the course "Software Engineering - AY 2024/25".
Start date: Wednesday, October 2nd, 2024
Class Schedule:
https://drive.google.com/file/d/130c7jinExYW1_R8NQdWJHRmtzU5Wvm-Z/view
Please register with the "Software Engineering" course on https://elearning.uniroma1.it/ to allow easy communication.
Spring Semester
Verifica e Validazione dei Sistemi intelligenti / (V&V) - AA 2024/25
Codice OPIS corso in presenza: REKUSTJ8
Codice OPIS corso in teledidattica: 5U6IQ7F2
Start date: March 4th, 2025
Class Schedule:
Tuesday, 10.30 am - 1 pm, Aula T1, Edificio E, Viale Regina Elena 295, Roma
Wednesday, 11.00 am - 1 pm, Aula S1, Edificio E, Viale Regina Elena 295, Roma
Please register with the "Verifica e Validazione dei Sistemi intelligenti " course at https://elearning.uniroma1.it/ to easy communication.
Master's Degree in Computer Science / Laurea Magistrale in Informatica
FALL Semester
Automatic Verification of Intelligent Systems (AVIS) - AY 2024/25
Codice OPIS: H0KTWIBU
All course syllabus information, material, exams, and projects will be available on the Sapienza e-learning platform: https://elearning.uniroma1.it/ under the course "Automatic Verification of Intelligent Systems - AY 2023/24".
Start date: Wednesday, October 2th, 2024
Class Schedule:
https://drive.google.com/file/d/12k-mOBkSO0JbI7y025RkTGqjiN6MMLHq/view
Please register with the "Automatic Verification of Intelligent Systems" course on https://elearning.uniroma1.it/ to allow easy communication.
Available Theses
Linked to ongoing research projects, I have many theses available for undergraduate students (Laurea Triennale) as well as for graduate students (Laurea Magistrale).
Basically all theses involve, at different degrees, methods and tools from Software Engineering (SE), Artificial Intelligence (AI), Reinforcement Learning (RL) and Model Checking (MC).
Here is a (non-exhaustive) list of topics:
AI, Model-Checking, and Reinforcement Learning for Automated Design of Intelligent Systems
- Automatic Design of Intelligent Systems
- Automatic Design of Cyber-Physical Systems
- Automatic Design of Software Systems
- Simulation-based design of Intelligent Systems from Digital Twins.
- Automatic anomaly detection and forecasting systems (e.g., predictive maintenance, trading agents, etc).
AI, Model-Checking, and Reinforcement Learning for Bioinformatics
- Identification of biomarkers (e.g., for cancer) from gene expression data
- Inferring Gene Regulatory Networks from Time Series Data
- In-silico trial through digital twins (Virtual Patients) based on Biochemical Networks and data from repositories such as https://elixir-europe.org/services/tag/data-resources
AI, Model-Checking, and Reinforcement Learning for Smart Grids
- Software-based management of Smart Grids
- Automatic management of electric grids with renewables and energy storage systems
Available Industrial Theses
Through collaborations with leading Industries, many theses are available for undergraduate (Laurea Triennale) and graduate (Laurea Magistrale) students.
Here is a (non-exhaustive) list of topics (in English or Italian, as they were provided).
- Algoritmi per Fusione dati sensoriali provenienti da veicoli unmanned: la tematica è quella della data-fusione tra i dati provenienti dai sensori afferenti al payload dei veicoli unmanned in movimento, con i dati dei sensori a bordo del veicolo ospitante (es. Nave). Studiare i paper sullo stato dell'arte e progettare/implementare l'algoritmo più idoneo al dominio applicativo. Studenti corso di laurea Magistrale. Contattere Enrico Tronci: tronci@di.uniroma1.it
- Data distribution su dati semi-strutturati e gerarchici nel dominio del Comando e Controllo: studiare lo stato dell'arte, analizzare i cots disponibili (es. Apache Kafka) e realizzare i benchmark, al fine di selezionare il più idoneo al dominio applicativo. Studenti corso di laurea Magistrale. Contattere Enrico Tronci: tronci@di.uniroma1.it
- Avatar per scenari di training cooperante: alcuni sistemi di Comando e Controllo necessitano la cooperazione di più operatori umani con Ruoli operativi distinti per condurre a compimento una operazione militare (es. Catena di ingaggio). Studiare una soluzione basata sull'Intelligenza Artificiale che possa implementare la virtualizzare di uno degli operatori cooperanti (Avatar) con cui l’operatore fisico in training possa cooperare in esercitazioni con scenari reali e interattivi. Studenti corso di laurea Magistrale. Contattere Enrico Tronci: tronci@di.uniroma1.it
- Riconoscimento automatico tramite reti neurali della "classifica" di oggetti sensore: le classficazioni di dominio e categoria degli oggetti effettuate dal software dei radar non sono spesso affidabili e necessitano di interazioni dell'operatore per confermare/sovrascrivere quelli proposti. Studiare una soluzione basata sull'intelligenza Artificiale che, tramite una rete neurale, vada a classificare per gli oggetti rilevati dai sensori (radar) connessi con il C2 il "dominio" (Land, Surface, Air, Undewater, Space) e la categoria (persone, automobili, carri, navi, imbarcazioni, aerei, droni, uccelli, ecc) basandosi sui dati relativi alla dinamicità della loro cinematica (no immagini). Studenti corso di laurea Magistrale. Contattere Enrico Tronci: tronci@di.uniroma1.it
- Data mining sui dati volatili da sensori e da C2: i Big Data sono un tema largamente applicato in molti contesti di business, ma scarsamente nei sistemi real-time o near-real-time come quello del Comando e Controllo, dove la "volatilità" dei dati grezzi dei sensori o dei dati elaborati dal C2 hanno una valenza solo nell'istante di utilizzo da parte degli operatori, per poi perdersi a meno di casi specifici. Data la valenza preziosa che al giorno d'oggi viene attribuita ai dati, si richiede di studiare una soluzione che vada a progettare un framework di Data Mining per la memorizzazione dei dati del sistema C2 al fine di supportare l'operatore con feature di inferenza strategico/tattica e business intelligence. Studenti corso di laurea Magistrale. Contattere Enrico Tronci: tronci@di.uniroma1.it
Orari di ricevimento
Giovedì: 15.00-16.00
Curriculum
1 Posizione Corrente
Dal 2001 Enrico Tronci (http://mclab.di.uniroma1.it, http://www.dsi.uniroma1.it/~tronci) è Professore Associato presso il Dipartimento di Informatica dell'Università di Roma ``La Sapienza'' (Italy).
2 Posizioni Precedenti
Dal 1994 al 2000 è stato ricercatore presso il Dipartimento di Informatica dell'Università di L'Aquila. Dal 1992 al 1993 è stato Post-Doc presso il LIP (Laboratoire pour l'Informatique du Parallelisme) all'ENS (Ecole Normal Superior) di Lyon (France).
3 Formazione
Nel 1991, con la supervisione del Prof. Richard Statman, ha ricevuto il Ph.D. degree da Carnegie Mellon University, Pittsburgh, USA. Nel 1987, con la supervisione di Prof. Corrado Boehm e Prof. Giorgio Ausiello, ha ricevuto la laurea in Ingegneria Elettronica dall'Università di Roma âœLa Sapienzaâ. La sua tesi ha ricevuto il premio IBM-Italia 1987 per le migliori tesi di laurea in Intelligenza Artificiale.
4 Ricerca
I suoi interessi di ricerca sono focalizzati su metodi e tools basati sul Model Checking per l'analisi e sintesi di sistemi reattivi mission critical oppure safety critical.
Un sistema reattivo è un sistema che scambia continuamente informazioni (input/output) con il suo ambiente allo scopo di conseguire determinati obiettivi. Esempi di sistemi reattivi sono: hardware digitale, sistemi di controllo, sistemi operativi, protocolli di comunicazione, business processes, Decision Support Systems (DSS), sistemi Sense and Respond (SaR) in generale.
Tipicamente un sistema è considerato mission critical se il suo fallimento può comportare perdite economiche, ma non umane. Un sistema è considerata safety critical se un suo fallimento può comportare perdite di vite umane.
Esempi di sistemi mission critical sono: satelliti spaziali, Decision Support Systems, sistemi ERP (Enterprise Resource Planning). Esempi di sistemi safety critical sono: sistemi di interlocking ferroviario, software per avionica.
4.1 Sintesi Automatica di Software di Controllo da Specifiche a ciclo Chiuso
Un sistema di controllo è costituito da un controllore (software nel nostro caso) ed da un un sistema controllato (plant). In un loop infinito il controllore osserva lo stato del plant (sensing), esegue una conversione AD, decide il comando da inviare al plant (decision), esegue una conversione DA ed infine invia il comando al plant (actuation). La nostra ricerca in questo ambito ha l'obiettivo di definre metodi e tools per la generation automatica del sotftware che implementa il controllore a partire da un modello del plant (come sistema ibrido), della conversione AD-DA e dalle specifiche del comportamento del sistema a ciclo chiuso. Classicamente l'Ingegneria dei Controlli si concentra sulla definizione delle specifica funzionale del controllore piuttosto che sulla sua implementazione. La presente attività di ricerca invece ha l'obiettivo appunto di produrre automaticamente software (corretto per costruzione) per il controllore. Ad esempio in [CAV10] presentiamo un metodo ed un tool per la sintesi automatica di software di controllo per sistemi a tempo discreto. Il software prodotto è corretto per costruzione (ad esempio è garantito essere esente da overflow aritmetici), ha un WCET (Worst Case Execution Time) garantito e noto a priori ed è in grado di rilevare automaticamente quando lo stato del plant è fuori dalla regione controllabile (Fault Detection).
Esempi di tale attività di ricerca sono in: [Sez5Pub1], [Sez5Pub4], [Sez5Pub6], [Sez5Pub25], [Sez5Pub26], [Sez5Pub29].
4.2 Algoritmi di Model Checking per Protocolli e Sistemi Ibridi
Il nostro focus è sul progetto di algoritmi di verifica automatica via model checking per protocolli e sistemi ibridi, cioè sistemi con variazioni di stato sia discrete che continue. Gli algoritmi studiati sfruttano la struttura statistica del sistema da verificare per contrastare la state explosion. Ad esempio questo è fatto sul codice sorgente in [Sez5Pub30] e sfruttando la località delle transizioni del grafo di transizione del sistema in [Sez5Pub23], [Sez5Pub21], [Sez5Pub16], [Sez5Pub18], [Sez5Pub13], [Sez5Pub12]. Un model checker probabilistico è stato realizzato in [Sez5Pub22]. In [Sez5Pub7] abbiamo investigato algoritmi di model checking per sistemi ibridi basati su SAT. In [APSEC07] abbiamo investigato algoritmi su disco per bounded model checking basato su SAT per la verifica del software (C).
4.3 Model Checking di Sistemi Stocastici
La località delle transizioni può essere sfruttata per realizzare algoritmi di bounded model checking per catene di Markov a tempo discreto [Sez5Pub8], [Sez5Pub14], [Sez5Pub17]. Il tool risultate (FHP-Murphi) permette la verifica (e quindi l'analisi di reliability) di sistemi fuori della portata di altri model checkers per sistemi stocastici.
4.4 Model Checking MAD Distributed Systems
Un sistema Multiple Administrative Domains (MAD) è un sistema cooperativo i cui nodi (agenti) appartengono a diversi domini amministrativi.
In [Sez5Pub3], [Sez5Pub2], in collaborazione con l'Univ. del Texas ad Austin, presentiamo un model checker (NashMV) per la verifica automatica di equilibri di Nash in sistemi MAD.
4.5 Technology Transfer
Per valutare l'efficacia degli approcci proposti, nell'ambito di progetti di ricerca Nazionali (ENEA, MIUR, MSE) ed Internazionali (ESA, EC) abbiamo condotto vari casi di studio in collaborazione con Industrie operanti nel settore. Alcuni esempi sono in [Sez5Pub11], [Sez5Pub15], [Sez5Pub20], [Sez5Pub24] ed in:
- [ERTS10] S. Mazzini, E. Tronci, C. Paccagnini, X. Olive. A Model-Based methodology to support the Space System Engineering (MBSSE). Proc. of: Embedded Real Time Software and Systems (ERTS), Toulouse, France, May 19-21, 2010
- [DASIA09] S. Mazzini, S. Puri, F. Mari, I. Melatti, E. Tronci. Formal Verification at System Level. In: DAta Systems In Aerospace (DASIA), Org. EuroSpace, Canadian Space Agency, CNES, ESA, EUMETSAT. May 26-29, 2009, Instanbul, Turkey, EuroSpace.
5 Comitati di Programma
Enrico Tronci ha servito come conference chair o membro del comitato di programma in molte importanti conference quali ad esempio: FDL (Formal Description Languages), CHARME (Correct Hardware Design and Verification Methods), FMCAD (Formal Methods in Computer Aided Design), DEVS (Symposium on Theory of Modeling & Simulation). Enrico Tronci è nell'Editorial Board di: International Journal of Discrete Event Control Systems (IJDECS)
6 Attività di Revisione
Enrico Tronci è regolarmente revisore per conference e journals internazionali quali ad esempio: International Journal of Computers and Applications, The Computer Journal, LICS (Logic in Computer Science), CHARME, FMCAD, FORMATS (Formal Modelling and Analysis of Timed Systems), IEE Proceedings - Computers and Digital Techniques, International Journal of Computers and Application, TCS (Theoretical Computer Science), CIMCA (International Conference on Computational Intelligence for Modelling, Control and Automation), Journal of Visual Languages and Computing, MeCBIC (Membrane Computing and Biologically Inspired Process Calculi), Fundamenta Informaticae, DEVS, IJMIC (International Journal of Modelling, Identification and Control).
Enrico Tronci è regolarmente revisore per progetti di ricerca Nazionali ed Internazionali quali ad esempio:
NWO (Netherlands Organisation for Scientific Research), Programma ``Rientro dei cervelli'', WWTF (Wiener Wissenschafts-, Forschungs- und Technologiefonds)
7 Software di Ricerca
Come parte della ricerca su algoritmi e tool di model checking è stato realizzato il seguente software di ricerca.
7.1 QKS
QKS (Quantized Kontrol Synthesizer) implementa gli algoritmi di sintesi automatica di software di controllo descritti in [Sez5Pub1].
7.2 NashMV
NashMV (http://mclab.di.uniroma1.it/software.html#nashmv), sviluppato con l'Univ. del Texas ad Austin, implementa gli algoritmi descritto in [Sez5Pub3], [Sez5Pub2] per la verifica automatica di equilibri di Nash in sistemi MAD.
7.3 CMurphi
CMurphi (http://mclab.di.uniroma1.it/software.html#cmurphi), Caching Murphi [Sez5Pub23], [Sez5Pub18], [Sez5Pub13], è una versione migliorata del model checker Murphi di Stanford University. CMurphi sfrutta la località delle transizioni per risparmiare sulla RAM e per accelerare gli algoritmi di verifica basati sul disco. CMurphi è stato ampiamente usato ad INTEL per la verifica di Cache Coherence Protocols. Infine, CMurphi può gestire i numeri reali a precisione finita ed è stato usato con successo nella verifica di sistemi ibridi non lineari.
7.4 FHP-Murphi
FHP-Murphi (http://mclab.di.uniroma1.it/software.html#fhpmurphi), Finite Horizon Probabilistic Murphi [Sez5Pub14], [Sez5Pub8], è un model checker esplicito per catene di Markov a tempo discreto. Esso è stato ampiamente usato per la verifica di protocolli probabilistici e per valutare l'affidabilità di sistemi complessi. FHP-Murphi può gestire reali a precisione finita ed è stato usato con successo per la verifica di sistemi stocastici non lineari.
7.5 BSP
BSP (http://mclab.di.uniroma1.it/software.html#bsp) è un interprete per Programmi Simbolici Booleani, cioè programmi che manipolano funzioni booleane. Essenzialmente, BSP è basata su una interfaccia basata sulla Logica del Prim'Ordine (First Order Logic, FOL) al pacchetto OBDD. Scrivere algoritmi simbolici con BSP è più facile che usare primitive C per le manipolazioni di OBDD. Di conseguenza, BSP può essere usato per prototipaggio veloce di algoritmi di model checking basati su OBDD. Tala approccio è stato usato in [Sez5Pub29], [Sez5Pub26], [Sez5Pub25] per implementare algoritmi simbolici per la sintesi di controllori supervisori.
8 Progetti di Ricerca
Enrico Tronci è costantemente coinvolto in molti progetti di ricerca finanziati dalla Comunità europea (EC), CNR, ENEA, MIUR ed industrie private. Ecco una lista selezionata.
1. PAEON (EC FP7) Model Driven Computation of Treatments for Infertility Related Endocrinological Diseases. (EC, Call FP7-ICT-2011-9, Objective ICT-2011.5.2 - Virtual Physiological Human). Il nostro ruolo in questo progetto è la progettazione di algoritmi di model checking per la verifica automatica e la sintesi di terapie personalizzate sulla base dei modelli matematici del sistema endocrinologico. Enrico Tronci è il coordinatore per questo progetto.
2. SmartHG (EC FP7) - Energy Demand Aware Open Services for Smart Grid Intelligent Automation. (EC, Call FP7-ICT-2011-8, Objective ICT-2011.6.1 - Smart Energy Grids). Il nostro ruolo in questo progetto è la progettazione di algoritmi di model checking per la verifica automatica e la sintesi di "energy demand aware price policies" per smart grids. Enrico Tronci è il coordinatore per questo progetto.
3. ESA ITI AO6067 - 2010 Model Checker Validator for Satellite Operational Procedure. Nel presente progetto finanziato dall'ESA (European Space Agency) sono responsabile scientifico del relativo contratto di ricerca con il Dipartimento di Informatica - Università di Roma ``La Sapienza''. Il main contractor del progetto è TELESPAZIO. L'obiettivo di questa Innovation Triangle Initiative (ITI) dell'ESA è di progettare e realizzare un model checker per la Verifica e Validazione (V&V) automatica delle procedure operative per satelliti.
4. Web Fitting Room (MSE) - 2010 Web Fitting Room (WFR) è un progetto sponsorizzato dal Ministero dello Svilluppo Economico (MSE) nell'ambito del programma ``Industria 2015''. Nel presente progetto sono responsabile scientifico dell'intero progetto e dell'unita di ricerca del Dipartimento di Informatica - Università di Roma ``La Sapienza''. L'obiettivo di WFR è il progetto e l'implementazione di un sistema web based per la produzioen on-demand di abiti connettendo vai Web un Camerino Virtuale (dove gli abiti vengono virtualmente indossati) ad un Decision Support System che, in tempo reale, organiza la produzione degli abiti selezionati. Il nostro ruolo nel presente progetto è il progetto e la realizzazione del DSS usando tecniche di Model CHekcing based Planning per contrastare il problema dell'esplosione dello spazio degli stati insito in DSS del tipo illustrato sopra.
5. ULISSE (EC FP7) - 2009 USOCs KnowLedge Integration and Dissemination for Space Science Experimentation (ULISSE) Questo è un progetto finanziato dall a Comunità Europea (EC) nell'ambito di FP7. Nel presente progetto Europeo sono responsabile scientifico per l'unità Dipartimento di Informatica - Università di Roma ``La Sapienza''. Il nostro compito in questo progetto è studiare tecniche di model checking per la verifica automatica delle procedure relative agli esperimenti di bordo nelle stazioni orbitanti (ad esempio la stazione Columbus).
6. SAPP (FILAS) - 2008 Sistema Avanzato per la Progettazione e la Pianificazione di Reti Wireless (SAPP). Nel presente progetto finanziato da FILAS (Finanziaria Laziale di Sviluppo) sono responsabile scientifico del relativo contratto di ricerca con il Dipartimento di Informatica - Università di Roma ``La Sapienza''. Il nostro compito in questo progetto è la progettazione e realizzazione di algoritmi per il posizionamento fault tolerant dei nodi relay di una rete wireless dati i modelli radio e le posizioni dei nodi gateway e sensori. Nello specifico si vuole garantire che anche in presenza di k nodi relay guasti la rete soddisfi le specifiche date.
7. ESA 5459 SSFRT - 2008 System and Software Functional Requirements Techniques (SSFRT). Nel presente progetto finanziato dall'ESA (European Space Agency) sono responsabile scientifico del relativo contratto di ricerca con il Dipartimento di Informatica - Università di Roma ``La Sapienza''. Il main contractor del progetto è INTECS. Il nostro compito in questo progetto è di investigare la possibilità di utilizzare tecniche di model checking per sistemi ibridi per la verifica automatica dei requisiti di sistema per satelliti e veicoli spaziali in genere. La modellazione di tali requisiti coinvolge sia il software che i sistemi (attuatori e sensori) con cui tale software interagisce. Da questo deriva la necessita di usare sistemi ibridi per la modellazione, validazione e verifica.
8. CRESCO (MIUR) - 2007 Centro Computazionale di RicErca sui Sistemi Complessi (CRESCO). Il contributo al presente progetto è stato nelle vesti di consulenti per l'Università del Salento che ha finanziato un contratto di ricerca, di cui sono il responsabile scientifico, con il Dipartimento di Informatica - Università di Roma ``La Sapienza''. Il nostro contributo al progetto consiste nel progetto e nella realizzazione di algoritmi per l'analisi automatica di indicatori di vulnerabilità di reti e servizi di telecomunicazione.
9. TRAMP (MIUR) - 2007 Sistema Integrato di Gestione e Controllo per il TRAsporto in Sicurezza di Merci Pericolose. Nel presente progetto finanziato dal MIUR sono responsabile scientifico per l'unità Dipartimento di Informatica - Università di Roma ``La Sapienza''. L'obiettivo del progetto è di aumentare la sicurezza del trasporto di materiali pericolosi usando tecnologie informatiche. Il nostro compito in questo progetto è di usare tecniche di model checking per verificare la safety dell'intero sistema con riferimento ai protocolli di livello applicativo ed alle politiche di controllo e gestione.
10. SETRAM (MIUR - ENEA) - 2006 Sistema esperto con funzioni di simulazione delle modalità di trasporto merci e di selezione dei percorsi sulla base di multicriteria. Il contributo al presente progetto è stato nelle vesti di consulenti ENEA che ha finanziato due contratti di ricerca, di cui sono stato il responsabile scientifico, con Dipartimento di Informatica - Università di Roma ``La Sapienza''. L'obiettivo del progetto è studiare l'applicazione dell'ottimizzazione multimodale a grandi ed esistenti sistemi di trasporto merci. Il nostro coinvolgimento in questo progetto è consistito nella progettazione e realizzazione di algoritmi di ottimizzazione per il trasporto multimodale.
11. IRRIIS (EC FP6 - ENEA) - 2005 Integrated Risk Reduction of Information-based Infrastructure. Il contributo al presente progetto Europeo è stato nelle vesti di consulenti ENEA che sulle tematiche del progetto ha finanziato un contratto di ricerca, di cui sono stato il responsabile scientifico, con il Dipartimento di Informatica - Università di Roma ``La Sapienza''. L'obiettivo di questo progetto è di definire tecniche di riduzione del rischio per grandi sistemi di infrastrutture critiche. Il nostro contributo al progetto è consistito nel progettare e realizzare algoritmi basati sulla programmazione lineare intera mista (MILP) per minimizzare l'inoperabilità di infrastrutture critiche.
12. SAFEGUARD (EC - ENEA) - 2004 Intelligent Agents Organization to Enhance Dependability and Survivability of Large Complex Critical Infrastructure. Il contributo al presente progetto Europeo è stato nelle vesti di consulenti ENEA che sulle tematiche del progetto ha finanziato un contratto di ricerca, di cui sono stato il responsabile scientifico, con il Dipartimento di Informatica - Università di Roma ``La Sapienza''. L'obiettivo di questo progetto è l'investigazione di metodi per aumentare l'affidabilità di grandi infrastrutture critiche. Il nostro contributo al progetto è consistito nel progettare ed implementare un tool basato su catene di Markov per la rivelazione automatica di anomalie nel traffico TCP.
13. SAFE TUNNEL (EC - ENEA) - 2003 Innovative systems and frameworks for enhancing of traffic safety in road tunnels. Il contributo al presente progetto Europeo è stato nelle vesti di consulenti ENEA che sulle tematiche del progetto ha finanziato un contratto di ricerca, di cui sono stato il responsabile scientifico, con il Dipartimento di Informatica - Università di Roma ``La Sapienza''. L'obiettivo di questo progetto è di investigare l'utilizzo di tecniche dell'information technology per aumentare la sicurezza all'interno dei trafori alpini. Il nostro contributo al progetto è consistito nella verifica della safety dei protocolli di comunicazione e controllo all'interno di tunnel stradali usando tecniche di model checking.
14. MEFISTO (MIUR - COFIN) - 2002 MEtodi FormalI per Sicurezza e TempO. Il presente progetto è un COFIN a cui ho partecipato come membro dell'unità di ricerca del Dipartimento di Informatica dell'Università di Pisa. L'obiettivo del progetto è di investigare come i metodi formali possano essere usati per verificare la sicurezza di sistemi in cui il tempo gioca un ruolo importante. Il nostro contributo al progetto è consistito nell'ideazione e realizzazione di algoritmi e tool oltre lo stato dell'arte per la verifica di protocolli probabilistici e sistemi ibridi.
15. ICARO (ENEA) - 2001 ICARO. Il presente progetto è stato finanziato da ENEA attraverso un contratto di ricerca, di cui sono stato il responsabile scientifico, con il Dipartimento di Informatica - Università di Roma ``La Sapienza''. L'obiettivo di questo progetto è l'investigazione di metodi per l'analisi di affidabilità di sistemi di controllo complessi come l'impianto di cogenerazione ICARO in uso all'ENEA di Casaccia. Il nostro contributo al progetto è consistito nella modellazione e verifica del sistema di controllo di ICARO usando tecniche di model checking per sistemi ibridi.
16. TOSCA (MIUR - COFIN) - 2000 Teoria della Concorrenza, Linguaggi di Ordine Superiore e Strutture di Tipi. Il presente progetto è un COFIN a cui ho partecipato come membro dell'unità di ricerca del Dipartimento di Informatica dell'Università di L'Aquila. Il nostro contributo al progetto è consistito nell'ideazione e realizzazione di algoritmi e tool innovativi per la verifica di sistemi concorrenti.
17. SIPA (MIUR) - 1999 SIPA. Il contributo al presente progetto MIUR è stato nelle vesti di consulente per GCE (Global Consulting Engineering) che sulle tematiche del progetto ha finanziato un contratto di ricerca, di cui sono stato il responsabile scientifico. Il nostro contributo al progetto è consistito nella progettazione e realizzazione di algoritmi per il controllo non intrusivo di un processo di produzione dell'industria casearia.
18. GUARDS (EC) - 1998 GUARDS. Il contributo al presente progetto Europeo è stato nelle vesti di consulenti per il Consorzio Pisa Ricerche che sulle tematiche del progetto ha finanziato un contratto di ricerca, di cui sono stato il responsabile scientifico. In nostro contributo al progetto è consistito nella progettazione e realizzazione di algoritmi di model checking simbolico per il model checker per ACTL del Consorzio Pisa Ricerche.