Implementazione automatica di protocolli di interazione AUML mediante reti di Petri

Questa tesi si basa su una serie di lavori precedenti, volti ad analizzare la correlazione tra i modelli AUML e le reti di Petri, per riuscire a fornire una metodologia di traduzione dai primi alle seconde. Questa traduzione permetterà di applicare tecniche di model checking alle reti così create, al fine di stabilire le proprietà necessarie al sistema per poter essere realizzato effettivamente. Verrà poi discussa un'implementazione di tale algoritmo sviluppata in tuProlog ed un primo approccio al model checking utilizzando il programma Maude. Con piccole modifiche all'algoritmo utilizzato per la conversione dei diagrammi AUML in reti di Petri, è stato possibile, inoltre, realizzare un sistema di implementazione automatica dei protocolli precedentemente analizzati, verso due piattaforme per la realizzazione di sistemi multiagente: Jason e TuCSoN. Verranno quindi presentate tre implementazioni diverse: la prima per la piattaforma Jason, che utilizza degli agenti BDI per realizzare il protocollo di interazione; la seconda per la piattaforma TuCSoN, che utilizza il modello A&A per rendersi compatibile ad un ambiente distribuito, ma che ricalca la struttura dell'implementazione precedente; la terza ancora per TuCSoN, che sfrutta gli strumenti forniti dalle reazioni ReSpecT per generare degli artefatti in grado di fornire una infrastruttura in grado di garantire la realizzazione del protocollo di interazione agli agenti partecipanti. Infine, verranno discusse le caratteristiche di queste tre differenti implementazioni su un caso di studio reale, analizzandone i punti chiave.

Interferometria SAR per lo studio di movimenti e generazione di modelli digitali del terreno in Antartide

Satellite SAR (Synthetic Aperture Radar) interferometry represents a valid technique for digital elevation models (DEM) generation, providing metric accuracy even without ancillary data of good quality. Depending on the situations the interferometric phase could be interpreted both as topography and as a displacement eventually occurred between the two acquisitions. Once that these two components have been separated it is possible to produce a DEM from the first one or a displacement map from the second one. InSAR DEM (Digital Elevation Model) generation in the cryosphere is not a straightforward operation because almost every interferometric pair contains also a displacement component, which, even if small, when interpreted as topography during the phase to height conversion step could introduce huge errors in the final product. Considering a glacier, assuming the linearity of its velocity flux, it is therefore necessary to differentiate at least two pairs in order to isolate the topographic residue only. In case of an ice shelf the displacement component in the interferometric phase is determined not only by the flux of the glacier but also by the different heights of the two tides. As a matter of fact even if the two scenes of the interferometric pair are acquired at the same time of the day only the main terms of the tide disappear in the interferogram, while the other ones, smaller, do not elide themselves completely and so correspond to displacement fringes. Allowing for the availability of tidal gauges (or as an alternative of an accurate tidal model) it is possible to calculate a tidal correction to be applied to the differential interferogram. It is important to be aware that the tidal correction is applicable only knowing the position of the grounding line, which is often a controversial matter. In this thesis it is described the methodology applied for the generation of the DEM of the Drygalski ice tongue in Northern Victoria Land, Antarctica. The displacement has been determined both in an interferometric way and considering the coregistration offsets of the two scenes. A particular attention has been devoted to investigate the importance of the role of some parameters, such as timing annotations and orbits reliability. Results have been validated in a GIS environment by comparison with GPS displacement vectors (displacement map and InSAR DEM) and ICEsat GLAS points (InSAR DEM).

Interfaccia web per un sistema di condivisione semantica dell'informazione: studio e implementazione

Questa tesi progettuale nasce per integrare gli sforzi attuali sullo sviluppo del web semantico. La piattaforma di riferimento sulla quale è stato svolto il presente lavoro è SMART-M3. Questa piattaforma mette a disposizione uno spazio condiviso di informazioni, rappresentate e accessibili secondo le tecnologie del web semantico. In questo scenario, nasce la necessità di disporre di un'interfaccia web capace di interagire con la piattaforma - in grado di risolvere la complessità intrinseca dei dati semantici - allo scopo di averne un completo controllo; ricerche precedenti a questo proposito hanno dato come frutto una libreria PHP che mi è stata consegnata come strumento per lo sviluppo dell'interfaccia. La tesi si è articolata in 3 fasi principali: una fase iniziale di documentazione sull'argomento, eseguita principalmente sul libro “A developer's guide to the semantic web” di Liyang Yu e sulla tesi “Ontologie per il web semantico: un'analisi comparativa.” di Indrit Beqiri; una seconda fase, quella principale, di sviluppo del progetto informatico; una terza fase, infine, di sviluppo di questo elaborato di tesi, da considerarsi come la trattazione di tutto il percorso soprascritto, dall'inizio alla fine, secondo l'ordine cronologico in cui si svolto l'intero processo della tesi.

Evoluzione dei Modelli e delle Tecnologie per il Web: DART e HTML5 come caso di studio

Nell’ultimo decenno si è assisitito ad una frenetica evoluzione delle tecnologie di connessione e trasferimento dati, dagli impianti di fibra ottica sempre più diffusi e performanti, alle varie tecnologie mobile UMTS e LTE. Tutto ciò ha permesso a sempre più persone di poter spendere una maggiore fetta del proprio tempo sulla rete sia per svago che per lavoro. Questo ha portato col tempo l’utente interattivo alla ricerca di servizi remoti che prima usufruiva in locale, sia per motivi di portabilità e di interconnessione, sia per una semplice questione di sincronizzazione fra i vari dispositivi posseduti. Il presente progetto di tesi si pone come obiettivo di indagare con occhio ingegneristico all’evoluzione della struttura del web fino ad identificare e analizzare l’attuale necessità di poter avere in rete tutti quei servizi anche completi e strutturalmente complessi che prima si aveva sul proprio desktop; tutto ciò attraverso l’esempio di un nuovo linguaggio di sviluppo per applicazioni web strutturate proposto da Google: DART. In questa analisi non si potrà prescindere dallo studio attento della tecnologia che sin dagli inizi della rete ha fatto da struttura al web ovvero l’Html e il suo ultimo standard Hmtl5. Nella prima parte verrà mostrata, attraverso un breve percorso, la nascita e lo sviluppo del web, sino ai giorni nostri. Si effettuerà quindi una panoramica, rivisitando tutti più importanti passi che hanno portato la rete internet ad essere ciò che oggi utilizziamo, ponendo una particolare attenzione alle attuali esigenze di progettazione della struttura dei servizi web. Nel secondo capitolo viene introdotta la tecnologia a base del web, l’Html; attraverso una breve analisi dell’evoluzione di quest’ultima si arriverà sino all’attuale HTML5 e alle funzionalità offerte nell’ottica della programmazione web strutturata. Nel terzo capitolo si analizzerà in maniera più approfondita la necessità di un web strutturato e le potenzialità del progetto Dart attraverso alcuni esempi esplicativi. Infine si trarranno alcune conclusioni sull’attuale situazione del web, sulla necessità di un web strutturato e sulla possibilità di riuscita del progetto Dart.

Studio di espressione e funzione della PLCβ1 nucleare in modelli murini ed umani di cellule ematopoietiche mieloidi e linfoidi

The aims of this work were to investigate the role of nuclear Phospholipase C beta 1 (PI-PLCβ1) in human and mouse cell lines and to identify new binding partners of nuclear PI-PLCβ1 to further understand the functional network in which the enzyme acts. The intracellular distribution of PI-PLCβ1 was further investigated in human leukaemia cell lines (NB4, HL60, THP1, CEM, Jurkat, K562). With the exception of HL60, a high endogenous level of PI-PLCβ1 was detected in purified nuclei in each of the cell lines. We found that also in Ba/F3 pro-B cells overexpressing PI-PLCβ1b the protein localize within the nucleus. Although our data demonstrated that PI-PLCβ1b was not involved in cell proliferation and IGF-1 response as shown in other cell lines (FELC and Swiss 3T3), there was an effect on apoptosis. Activation of early apoptotic markers caspase-3 and PARP was delayed in PI-PLCβ1b overexpressing Ba/F3 cells treated with 5 gr/ml mitomycin C for 24h. We performed an antibody-specific immunoprecipitation on nuclear lysates from FELC-PLCβ1b cells. Mass spectrometry analysis (nano-ESI-Q-TOF) of co-immunoprecipitated proteins allowed for identification of 92 potential nuclear PI-PLCβ1b interactors. Among these, several already documented PI-PLCβ1b interacting partners (Srp20, LaminB, EF1α2) were identified, further validating our data. All the identified proteins were nuclear, mostly localized within the nuclear speckles. This evidence is particularly relevant as PI-PLCβ1 is known to localize in the same domains. Many of the identified proteins are involved in cell cycle, proliferation and transcriptional control. In particular, many of the proteins are components of the spliceosome multi-complex, strengthening the idea that PI-PLCβ1b is involved in mRNA processing and maturation. Future work will aim to better characterize the regulatory role of PI-PLCβ1b in mRNA splicing.

Studio ed analisi della sicurezza del protocollo SIP nelle reti Voice over IP

Nell'era di Internet e della digitalizzazione, anche la telefonia ha avuto la possibilità di evolversi, e grazie alle tecnologie Voice-over-IP è stato possibile realizzare servizi di comunicazione avanzata su reti di dati. Anche se la comunicazione vocale è l'aspetto chiave di questi sistemi, le reti VoIP supportano altri tipi di servizi, tra cui video, messaggistica istantanea, condivisione di file, ecc. Il successo di questa nuova tipologia di rete è dovuto ad una migliore flessibilità rispetto ai vecchi sistemi analogici, grazie ad architetture aperte e implementazioni a livello software, e soprattutto ad un minor costo legato alle apparecchiature ed ai collegamenti utilizzati, ed ai nuovi modelli di business e di consumo sempre più orientati allo sfruttamento della connettività a banda larga. Tuttavia, l'implementazione dei sistemi VoIP rappresenta anche un grado di complessità maggiore in termini di architetture di rete, di protocolli, e di implementazione, e con questo ne segue un incremento delle possibili vulnerabilità. Una falla nella sicurezza in questi sistemi può portare a disservizi e violazione della privacy per gli utenti con conseguenti ripercussioni economiche per i relativi gestori. La tesi analizza la sicurezza delle reti VoIP concentrandosi sul protocollo che sta alla base dei servizi multimediali, il protocollo SIP. SIP è un protocollo di livello applicativo realizzato per creare, modificare e terminare delle sessioni multimediali tra due o più utenti. Dopo un'introduzione alle generalità del protocollo, vengono esaminate le classi di vulnerabilità delle reti VoIP e gli attacchi a SIP, e vengono presentate alcune contromisure attuabili. Viene mostrato un esempio di come vengano attuati alcuni dei principali attacchi a SIP tramite l'utilizzo di appositi strumenti. L'eborato conclude con alcune considerazioni sulle minacce al protocollo e sugli obiettivi futuri che la comunità scientifica dovrebbe perseguire.

Studio degli effetti funzionali e tossici di derivati di Brassicaceae in modelli sperimentali

I vegetali appartenenti alla famiglia delle Brassicaceae, sono ricchi di molecole biologicamente attive note per le numerose proprietà salutari. L’effetto di un estratto di germogli di cavolo nero toscano (TBCSE) è stato investigato, in termini chemiopreventivi, sugli enzimi epatici del metabolismo degli xenobiotici e antiossidanti, in ratti trattati con TBCSE. I risultati hanno mostrato un complesso pattern di modulazione, con una prevalente inibizione, del sistema citocromo P450-dipendente, e induzioni significative degli enzimi di fase II (glutatione transferasi e glucuronosiltransferasi) e antiossidanti (catalasi, NAD(P)H:chinone reduttasi, glutatione reduttasi e perossidasi). Successivamente, l’effetto di TBCSE è stato studiato nei confronti delle alterazioni provocate da un’alimentazione iperlipidica nel ratto. Il trattamento si è dimostrato efficace nel contrastare gli effetti deleteri dei grassi presenti nella dieta, come l’iperlipidemia, l’aumento del peso corporeo e del fegato, l’indebolimento delle attività degli enzimi antiossidanti e del potenziale detossificante a livello epatico. Complessivamente, TBCSE emerge essere un promettente prodotto nutraceutico con potenziali effetti chemiopreventivi, e da impiegare come strategia alimentare per contrastare gli effetti correlati ad una dieta iperlipidica. Il consumo di dosi sovralimentari di molecole isolate dalle Brassicaceae, tramite per esempio integratori dietetici, come strategia alimentare preventiva, potrebbe tuttavia rappresentare un rischio per la salute. La potenziale tossicità del sulforafane, glucorafanina, indolo-3-carbinolo, e 3,3'-diindolimetano, è stata valutata in epatociti primari di ratto. La citotossicità e l’induzione di stress ossidativo, osservate a concentrazioni non lontane da quelle che potrebbero essere raggiunte in vivo, insieme ad una forte modulazione dell’espressione genica, riguardante principalmente il metabolismo degli xenobiotici, risposte ad alterazioni dello stato ossidoredutivo, eventi di riparazione del DNA e di proteine, induzione dell’apoptosi, e meccanismi (co)cancerogeni, sottolineano la potenzialità di queste molecole di determinare un rischio tossicologico, in seguito ad un’assunzione prolungata e ad alte dosi.

Validazione di modelli numerici per lo studio del cambiamento di fase solido/liquido in leghe metalliche in regime di convezione naturale

Il lavoro svolto ha come scopo l’implementazione e la validazione di un modello di cambiamento di fase mediante l’utilizzo del codice commerciale Comsol Multiphysics, che permette la modellazione e la risoluzione di equazioni matematiche che governano ambienti multifisici. La validazione dei modelli sviluppati è stata effettuata mediante confronto sia con soluzioni analitiche di riferimento, sia con soluzioni numeriche ottenute utilizzando il codice commerciale ProCAST, sviluppato appositamente per simulazioni di processi fusori I problemi analizzati hanno riguardato lo scambio termico sia in regime di sola conduzione, sia in presenza di convezione naturale all’interno di un materiale in cambiamento di fase solido-liquido. È stato considerato sia il caso di sostanze pure, quindi con un’unica temperatura di cambiamento di fase, sia il caso di leghe metalliche, la cui transizione di fase avviene in un intervallo di temperatura.  

Studio e implementazione di metodi per la migrazione di processi tramite dmtcp

In questo elaborato vengono descritte le principali modalità di migrazione di processi con riferimento al Sistema Operativo GNU Linux. Sono presentate : caratteristiche di migrazione, varianti implementative, tecniche di checkpoint restart, DMTCP ed il progetto ULPM. Il corso di riferimento è Progetto di Sistemi Virtuali. Il relatore è il professor Renzo Davoli.

Modelli stocastici per tassi di trasferimento e di interesse

Questa tesi nasce come risultato di un'esperienza di stage svolta presso l'ufficio Pianificazione e Risk Management in Cassa di Risparmio di Cento; l'obiettivo di questo lavoro è la descrizione dell'analisi da me svolta per la ricostruzione del metodo di determinazione del tasso interno di trasferimento adottato in questa banca. A questo studio è stata aggiunta una sezione legata all'analisi e all'implementazione di due modelli stocastici per l'evoluzione dei tassi di interesse (modello di Vasicek e modello CIR).

Modelli di predizione numerica di evoluzione di difetti in materiali metallici sotto carichi ciclici

Implementazione di modelli sul calcolatore per cercare di stimare la vita a fatica dei principali materiali metallici utilizzati in ambito aeronautico.

Studio e applicazione di tecniche di riduzione di dimensionalita a modelli geometrici di percezione visiva

La tesi affronta il tema della neuromatematica della visione, in particolare l’integrazione di modelli geometrici di percezione visiva con tecniche di riduzione di dimensionalità. Dall’inizio del secolo scorso, la corrente ideologica della Gestalt iniziò a definire delle regole secondo le quali stimoli visivi distinti tra loro possono essere percepiti come un’unica unità percettiva, come ad esempio i principi di prossimità, somiglianza o buona continuazione. Nel tentativo di quantificare ciò che gli psicologi avevano definito in maniera qualitativa, Field, Hayes e Hess hanno descritto, attraverso esperimenti psicofisiologici, dei campi di associazione per stimoli orientati, che definiscono quali caratteristiche due segmenti dovrebbero avere per poter essere associati allo stesso gruppo percettivo. Grazie alle moderne tecniche di neuroimaging che consentono una mappatura funzionale dettagliata della corteccia visiva, è possibile giustificare su basi neurofisiologiche questi fenomeni percettivi. Ad esempio è stato osservato come neuroni sensibili ad una determinata orientazione siano preferenzialmente connessi con neuroni aventi selettività in posizione e orientazione coerenti con le regole di prossimità e buona continuazione. Partendo dal modello di campi di associazione nello spazio R^2xS^1 introdotto da Citti e Sarti, che introduce una giustificazione del completamento percettivo sulla base della funzionalità della corteccia visiva primaria (V1), è stato possibile modellare la connettività cellulare risolvendo un sistema di equazioni differenziali stocastiche. In questo modo si sono ottenute delle densità di probabilità che sono state interpretate come probabilità di connessione tra cellule semplici in V1. A queste densità di probabilità è possibile collegare direttamente il concetto di affinità tra stimoli visivi, e proprio sulla costruzione di determinate matrici di affinità si sono basati diversi metodi di riduzione di dimensionalità. La fenomenologia del grouping visivo descritta poco sopra è, di fatto, il risultato di un procedimento di riduzione di dimensionalità. I risultati ottenuti da questa analisi e gli esempi applicativi sviluppati si sono rivelati utili per comprendere più nel dettaglio la possibilità di poter riprodurre, attraverso l’analisi spettrale di matrici di affinità calcolate utilizzando i modelli geometrici di Citti-Sarti, il fenomeno percettivo di grouping nello spazio R^2xS^1.