Sono Disponibili Tesi e Stage (Interni od Esterni) Sui Seguenti Argomenti



Verifica Automatica di Sistemi Reattivi (Model Checking)

Molti sistemi di largo uso sono di fatto sistemi reattivi. Esempi sono: hardware digitale, sistemi operativi, sistemi embedded, protocolli, sistemi di controllo, sistemi per telecomunicazioni.

Un errore in tali sistemi può comportare danni a persone o cose (violazione dei requisiti di safety ) oppure a trasmissione indesiderata di informazione (violazione dei requisiti di security ).

In breve, per questi sistemi il costo (umano od economico) di un errore è spesso elevato. In constrasto il time-to-market è sempre più piccolo ed il costo del testing sempre più elevato. Per questo sono necessarie tecniche sempre più efficienti di testing e debugging con un coverage molto elevato (praticamente 100%).

L'obiettivo del model checking e dei relative tools (model checkers) è appunto quello di effettuare off-line un testing esaustivo (verifica) della descrizione (in un opportuno linguaggio di programmazione) del sistema da realizzare.

Le tesi in tale area possono essere sia progettuali che di ricerca.

Una tesi progettuale può ad esempio consistere nella implementazione di un algoritmo di model checking oppure nell'analisi della safety/security di un particolare sistema (ad esempio un protocollo od un sistema embedded).

Una tesi di ricerca può ad esempio consistere nella ideazione ed implementazione di un algoritmo di model checking.


Sintesi Automatica di Controllers da Specifiche Formali

Un controllore è un sistema reattivo che invia comandi ad una altro sistema reattivo (spesso chiamato plant) al fine di raggiungere determinati obiettivi.

Il problema della sintesi del controller è: dato il modello del plant e gli obiettivi di controllo sintetizzare automaticamente il controller.

Le tesi possono essere sia progettuali che di ricerca.


Verifica e Sintesi di Automatica di Sistemi Ibridi

I sistemi ibridi (Hybrid Systems) sono sistemi il cui stato e' rappresentato in parte da componenti continue ed in parte da componenti discrete. Quasi tutti gli embedded systems sono sistemi ibridi.

Alcuni esempi: il software di controllo per: aerei, autoveicoli, motori, forni, lavatrici, televisori, alimentatori, frullatori, giocattoli, etc ...

Una tesi in tale ambito tipicamente consisite nella modellazione, verifica o sintesi (del controllore) di un sistema ibrido.

Le tesi possono essere sia progettuali che di ricerca.


Criptoanalisi del DES

L'obiettivo di un algoritmo di cifratura è di trasformare (con l'ausilio di una chiave segreta) un testo sorgente (testo in chiaro) in un corrispondente testo cifrato.

Il DES è uno dei più noti e più usati algoritmi di cifratura. Ad esempio il DES è usato in molti dei protocolli sicuri per internet.

L'obiettivo della criptoanalisi è di ricostruire il testo in chiaro a partire da uno o più testi cifrati. Questo permette di valutare la sicurezza dell'algoritmo di cifratura analizzato.

L'obiettivo della presente tesi è di indagare l'applicabilità di nuovi approcci alla criptoanalisi del DES sia dal punto di vista teorico che da quello sperimentale.

Per informazioni rivolgersi al Prof. Riccardo Silvestri od al Prof. Enrico Tronci.


Uso del datamining nell'analisi automatica di sistemi reattivi

Il datamining è una particolare tecnica di Machine Learning.

L'obiettivo delle tesi proposte è quello di studiare e sperimentare l'uso del datamiming negli algoritmi di analisi automatica (sia off-line che on-line) per sistemi reattivi.


Datamining per grandi insiemi di dati

Il datamining è una particolare tecnica di Machine Learning.

L'uso del datamining nell'analisi di sistemi reattivi comporta obbliga al machine learning su insiemi di dati di grandi dimensioni.

L'obiettivo delle tesi proposte è quello di studiare opportuni algoritmi per il datamining su grandi insiemi di dati.


Case Studies

Si tratta tipicamente di utilizzare i metodi automatici (model checking) per la verifica e/o validazione automatica di sistemi concorrenti. Ecco alcuni esempi di progetti completati.

I case studies sono tesi progettuali.

Freeware on WEB

Uso, modifica e progetto di freeware (e.g. Linux, Apache, Perl, etc) per applicazioni distribuite sul web. Esempi: basi dati, comunita' virtuali, intelligent houses, etc.


Case Base Reasoning (CBR)

Tesi di Laurea in ENEA con periodo di tirocinio nell'Ente.

La tesi di laurea si inquadra nel contesto delle attività previste da progetto europeo SAFEGUARD il cui obbiettivo è quello di sviluppare una rete di protezioni per infrastrutture critiche di tipo "information intensive".

All'interno di questo contesto essa è rivolta allo sviluppo e prova di algoritmi basati su metodologie di Intelligenza Artificiale (Case Base Reasoning) da implementare negli agenti di più basso livello (Anomaly Detection Agents) previsti nell'architettura multi-agente SAFEGUARD.

Stato dell'arte sugli algoritmi di Case Base Reasoning (CBR):
In ENEA è già disponibile uno strumento basato su algoritmo CBR e utilizzato per attività di diagnostica fuori-linea (p.e. diagnosi di malfunzionamento di Turbo-alternatori o prevenzione incidenti su depositi petroliferi).

Obiettivo della tesi:
Nuova implementazione dello strumento, mediante utilizzo di linguaggio object-oriented di tipo Java al fine di renderlo adatto al processamento in-linea (real-time) per poter essere integrato nel sistema SAFEGUARD.

Questo obiettivo può scindersi in due sotto-obiettivi:

I due sotto-obiettivi potrebbero essere affrontati nell'ambito di una singola tesi di laurea specialistica oppure nell'ambito di due tesi di laurea di primo livello.

Per questa tesi contattare: Claudio Balducelli (email: balducelli_c@casaccia.enea.it) oppure Enrico Tronci (email: tronci@dsi.uniroma1.it).


Reti Neurali (NN)

Tesi di Laurea in ENEA con periodo di tirocinio nell'Ente.

La tesi di laurea si inquadra nel contesto delle attività previste da progetto europeo SAFEGUARD il cui obiettivo è quello di sviluppare una rete di protezioni per infrastrutture critiche di tipo "information intensive".

All'interno di questo contesto essa è rivolta allo sviluppo e prova di algoritmi basati su metodologie di Intelligenza Artificiale (Neural Networks) da implementare negli agenti di più basso livello ("Hybrid Detection Agents") previsti nell'architettura multi-agente SAFEGUARD.

Stato dell'arte:
In ENEA è già disponibile uno strumento con interfaccia visuale (acronimo PEANO) che opera in ambiente Windows e che può essere utilizzato per attività di diagnostica fuori-linea (tipicamente classificazione e diagnostica di segnali provenienti da reti elettriche operanti a vari regimi). Lo strumento Peano servirà a prendere la necessaria confidenza con il dominio applicativo di riferimento (reti di trasmissione elettriche) e con gli aspetti algoritmici di una rete neurale.

Obiettivo della tesi:
Implementazione di una rete neurale di tipo back-propagation che opererà, secondo lo schema classico, in due modalità differenti: fase di addestramento in cui la rete dovrà "apprendere" e "memorizzare" lo stato normale di una rete di trasmissione elettrica fase di incapsulamento della rete neurale "addestrata" in un agente di basso livello per intercettare situazioni anomale ("novelty"). Il software verrà sviluppato in linguaggio Java e la sua implementazione sarà conforme al paradigma della programmazione ad oggetti.

Per questa tesi contattare: Giovanni Dipoppa (email: giovanni.dipoppa@casaccia.enea.it) oppure Enrico Tronci (email: tronci@dsi.uniroma1.it).


Applicazioni del Datamining all'Ingegneria Agraria

Tesi in collaborazione con l'ISMA (Istituto per la Meccanizzazione Agricola).

Uso di tecniche di Datamining per l'analisi di grandi database di misure fisiche multicanale (e.g. spettrofotometria visibile - vicino infrarosso) per l'analisi previsionale di fenomeni legati alla qualità di produzione di prodotti agricoli (agrumi, olivo, carne).

Obiettivo

Studiare le possibilità applicative e verificare le capacità previsionali di tecniche di machine learning applicati a grandi insiemi di dati ottenuti con strumenti innovativi multicanale, operanti su prodotti e processi agroalimentari.

Stato dell'arte

L'agricoltura nazionale è chiamata ad essere sempre più competitiva e al tempo stesso più rispettosa dei vincoli ambientali. Tale orientamento, sintetizzato nel termine tecnico di agricoltura sostenibile, può tradursi nella pratica operativa in una maggiore attenzione alla qualità di produzione e a quella del prodotto, in riferimento al consumatore nella duplice veste di acquirente e di beneficiario dell'ecosistema.

In tale senso negli ultimi anni è aumentata in maniera esponenziale la richiesta di sistemi di controllo e di monitoraggio dei parametri della produzione e del prodotto ai fini di una standardizzazione qualitativa, merceologica e per la riduzione dell'impatto ambientale.

La sostenibilità agricola, o per meglio dire dei bio-sistemi - secondo l'accezione internazionale più moderna - è perseguita non solo attraverso diretti interventi specifici, ma anche controllando le variabili agro-colturali produttive che per propria natura e disposizione spazio/temporale risultavano nel passato di difficile, se non impossibile, controllo. Basti pensare: alla valutazione localizzata degli stati eco-fisiologici delle colture, alla selezione per singolo frutto di parametri qualitativi complessi (grado zuccherino, colore, consistenza), al controllo di filiera degli andamenti di parametri termo-fisici e merceologici inerenti il trasporto e la trasformazione di prodotti deperibili.

A questa serie di problematiche e di richieste più o meno latenti da parte del sistema agro-alimentare, è possibile fornire parziale soluzione indagando sulle possibilità di sviluppo e di applicazione delle tecnologie innovative in campo elettronico e informatico, con particolare riferimento a quelle opto-elettroniche.

L'approccio strumentale e la conseguente produzione di grandi quantità dati (e.g. di informazioni multicanale), porta con se la necessità di usare sistemi automatici avanzati di analisi dei dati. Lo studio delle potenzialità applicative di questi sistemi sono ancora molto limitati nel settore agroalimentare.

La situazione descritta giustifica l'obiettivo della presente tesi.

Contatti

Per questa tesi contattare: Paolo Menessati (email: p.menesatti@ingegneriaagraria.it) oppure Enrico Tronci (email: tronci@dsi.uniroma1.it).


Formalizzazione dei modelli di calcolo CDFG, SARE, FSM e definizione di modalità di interazione tra essi

Tesi di Laurea ENEA, con periodo di tirocinio nell'Ente.

La tesi è finalizzata a formalizzare un modello di calcolo multiformalismo, basato su tre modelli di calcolo esistenti: il modello dei Control Data Flow Graphs (CDFG), delle System of Affine Recurrence Equations (SARE) e delle Macchine a Stati Finiti (FSM).

Una volta acquisite le caratteristiche dei tre modelli di calcolo, il lavoro di tesi si focalizzerà nella definizione di modalità di interazione tra i vari modelli. Le interazioni sono finalizzate a permettere la descrizione di un'applicazione complessa all'interno dei tre modelli di calcolo.

Per questa tesi contattare: Paolo Palazzari (email: palazzari@casaccia.enea.it) oppure Enrico Tronci (email: tronci@dsi.uniroma1.it).


Sviluppo di procedure di analisi per verificare la correttezza dei risultati prodotti da un algoritmo espresso in un modello di calcolo multiformalismo

Tesi di Laurea ENEA, con periodo di tirocinio nell'Ente.

Il lavoro di tesi si prefigge di individuare modalitàà per la verifica della correttezza di un algoritmo espresso all'interno di in un modello di calcolo multiformalismo.

Le procedure di verifica, principalmente basate sulla simulazione dell'algoritmo nella semantica che caratterizza il modello di calcolo, controlleranno la coincidenza/discrepanza dei risultati attesi da quelli effettivamente prodotti dall'algoritmo.

Le attività previste in questa tesi sono sostanzialmente rivolte alla realizzazione di un simulatore del modello di calcolo prescelto ed alla individuazione di metodiche per la selezione di pattern di test significativi per la verifica della correttezza dell'algoritmo.

Per questa tesi contattare: Paolo Palazzari (email: palazzari@casaccia.enea.it) oppure Enrico Tronci (email: tronci@dsi.uniroma1.it).


Strumenti innovativi per l'analisi e la gestione del traffico

Tesi di Laurea ENEA, con periodo di tirocinio nell'Ente.

La tesi è finalizzata allo sviluppo di strumenti di supporto al processo decisionale di gestione in linea del traffico urbano. In particolare si tratta di formulare e sviluppare modelli in grado di stimare lo stato della rete partendo da diverse misure generate, in tempo reale, da appositi sensori, nonchè di prevedere l'evoluzione a breve termine (30-60 minuti) del traffico.

La tesi può essere inoltre finalizzata alla formulazione e sviluppo di modelli per l'identificazione precoce di stati di crisi/congestione del traffico.

Per questa tesi contattare: Gaetano Valenti (email: g.valenti@casaccia.enea.it, Tel. 0630483460) oppure Enrico Tronci (email: tronci@dsi.uniroma1.it).


Modellazione ed analisi di sistemi digitali basati su Reti Pubbliche Mobili

Tesi di Laurea ENEA, con periodo di tirocinio nell'Ente.

Il lavoro di tesi prevede:

Per questa tesi contattare: Ester Ciancamerla (email: ciancamerlae@casaccia.enea.it) oppure Enrico Tronci (email: tronci@dsi.uniroma1.it).


Progettazione prototipale e analisi automatica di sistemi complessi

Tesi di Laurea ENEA, con periodo di tirocinio nell'Ente.

L'attività consiste nella realizzazione di un prototipo del sistema mediante tools e linguaggi ad alto livello testuali e grafici, partendo dai requisiti del sistema.

L'obiettivo della prototipazione è supportare l'analisi dei requisiti, in particolare safety e security.

Esempi di sistemi di interesse sono: i sistemi di controllo basati su reti di telecomunicazione, i sistemi di controllo embedded, i sistemi reattivi in generale.

Le metodologie e tools usati per l'analisi dei requisiti e la prototipazione includono: model checking, reti di petri, simulatori del sistema.

Le proprietà del sistema sono investigate mediante approcci qualitativi, quantitativi, deterministici e probabilistici.

Per questa tesi contattare: Michele Minichino (email: minichino@casaccia.enea.it) oppure Enrico Tronci (email: tronci@dsi.uniroma1.it).