Il linguaggio Alloy come ausilio nella specifica formale di modelli UML

UML è ampiamente considerato lo standard de facto nella fase iniziale di modellazione di sistemi software basati sul paradigma Object-Oriented; il suo diagramma delle classi è utilizzato per la rappresentazione statica strutturale di entità e relazioni che concorrono alla definizione delle specifiche del sistema; in questa fase viene utilizzato il linguaggio OCL per esprimere vincoli semantici sugli elementi del diagramma. Il linguaggio OCL però soffre della mancanza di una verifica formale sui vincoli che sono stati definiti. Il linguaggio di modellazione Alloy, inserendosi in questa fase, concettualmente può sopperire a questa mancanza perchè può descrivere con le sue entità e relazioni un diagramma delle classi UML e, tramite propri costrutti molto vicini all'espressività di OCL, può specificare vincoli semantici sul modello che verranno analizzati dal suo ambiente l'Alloy Analyzer per verificarne la consistenza. In questo lavoro di tesi dopo aver dato una panoramica generale sui costrutti principali del linguaggio Alloy, si mostrerà come è possibile creare una corrispondenza tra un diagramma delle classi UML e un modello Alloy equivalente. Si mostreranno in seguito le analogie che vi sono tra i costrutti Alloy e OCL per la definizione di vincoli formali, e le differenze, offrendo nel complesso soluzioni e tecniche che il modellatore può utilizzare per sfruttare al meglio questo nuovo approccio di verifica formale. Verranno mostrati anche i casi di incompatibilità. Infine, come complemento al lavoro svolto verrà mostrata, una tecnica per donare una dinamicità ai modelli statici Alloy.

Celti e Reti tra V e I sec. a.C. Oggetti tipo LaTène all'interno della cerchia culturale Fritzens-Sanzeno (arco alpino centro-orientale)

The study of the objects LaTène type found in middle-eastern alpine region (Trentino Alto Adige-Südtirol, Engadina, North Tirol, Voralberg and Villach basin) is aimed to a better comprehension of the complex net of relationships established among the Celts, settled both in the central Europe territories and, since the IV century b.C., in the Po Plain, and the local populations. The ancient authors, who called the inhabitants of this area Raeti, propose for this territory the usual pattern according to which, the population of a region was formed consequently to a migration or was caused by the hunting of pre-existing peoples. The archaeologists, in the last thirty years, recognized a cultural facies typical of the middle-eastern alpine territory during the second Iron Age, and defined that as Fritzens-Sanzeno culture (from the sites of Fritzens, Inn valley, and Sanzeno, Non Valley). The so-called Fritzens-Sanzeno culture spread out without breaks from the material culture of the final Bronze Age and the first Iron Age. This local substratum, characterized by a ceramic repertoire strongly standardized, by peculiar architectural solutions and by a particular typology of rural sacred places (Brandopferplätze), accepted, above all during the second Iron Age, the strong influences coming from the Etruscan world and from the Celtic one (evident in the presence of objects of ornament, of glass artefacts, of elements of the weaponry and of coins). The objects LaTène type become, with different degrees of reliability, important markers of the relationships existing between the Celts and the Raeti, although the ways of interaction (cultural influence, people's movements, commercial exchanges, gifts among élites etc.) is not still clear. The revision of published data and the study of unpublished materials allows to define a rich and articulated picture both to chronological level and to territorial one.

Ruolo ecologico di Ficopomatus enigmaticus (Polychaetae: Serpulidae) nelle lagune dell’Oristanese.

Gli agglomerati calcarei costruiti dalla specie invasiva Ficopomatus enigmaticus, polichete serpulide, possono influenzare i sistemi lagunari e produrre effetti negativi per la pesca e alterazioni nell’ambiente. Le lagune di Corru S’Ittiri (CI), San Giovanni-Marceddì (GM) e Santa Giusta (SG) sono state studiate al fine di definire le condizioni ecologiche che favoriscono le formazione delle costruzioni biogeniche di F. enigmaticus. In questo lavoro sono riportati i risultati preliminari, osservati in ogni laguna, sulle caratteristiche del sedimento (granulometria, sostanza organica e carbonati) e della comunità macrozoobentonica (abbondanza, biomassa e diversità), in due condizioni contrastanti: presenza e assenza dei reef, in due tempi di campionamento (maggio e ottobre 2012). I campioni di sedimento sono stati prelevati esclusivamente nel primo tempo di campionamento. La granulometria dei sedimenti era differente nelle tre lagune: CI e SG si sono rivelate più sabbiose, mentre GM era più fangosa. Sono stati osservati diversi valori nei contenuti di sostanza organica e carbonati senza rivelarsi significativamente diversi. Nel primo tempo di campionamento l’abbondanza di zoobentos varia tra le zone di presenza (P) e le zone di assenza (A) dei reef; in CI l’abbondanza è maggiore in P rispetto ad A, mentre in GM e SG invece è maggiore in A rispetto a P. La stessa situazione si verifica nel secondo tempo di campionamento. La biomassa, al tempo uno, è risultata maggiore nelle zone P rispetto alle zone A in CI e SG; in GM le zone A la biomassa è risultata maggiore rispetto a P. Nel secondo tempo di campionamento i valori risultano maggiori in P rispetto ad A in CI e GM; valori maggiori in A rispetto a P si sono riscontrati in SG. Importante da evidenziare la presenza di un altro costruttore di barriere, Hudroides dianthus, con abbondanze superiori rispetto a quelle di F. enigmaticus in particolare in CI e SG. Sono stati anche trovati diversi individui di Musculista sonhousia in CI e GM. M. senhousia è noto come specie invasiva in molte lagune del Mediterraneo ed è stato recentemente individuato nella zone di Oristano. Questo lavoro ha dimostrato come le caratteristiche dei sedimenti lagunari, la struttura della comunità macrozoobentonica, così come la natura e l’abbondanza delle specie costruttrici di reef può variare tra le lagune e le diverse zone delle lagune. È importante indagare sulle condizioni chimico-fisiche e idrodinamiche delle singole lagune per capire cosa influenza il reale sviluppo dei reef dei biocostruttori.

Sviluppo e caratterizzazione di algoritmi di segmentazione per l'analisi del cammino in acqua con tecnica markerless

Recenti studi hanno evidenziato come il cammino in ambiente acquatico possa portare a notevoli benefici nell’ambito di un processo riabilitativo: il cammino in acqua è infatti oggi considerato una delle principali terapie per pazienti con disturbi nella deambulazione, oltre ad essere impiegato per migliorare il recupero a seguito di interventi ed infortuni. Una caratterizzazione biomeccanica del cammino umano in acqua permetterebbe tuttavia di giungere a una conoscenza più approfondita degli effetti di quest’attività sul processo riabilitativo, e dunque a una sua prescrizione più mirata come parte delle terapie. Nonostante il crescente interesse, uno dei motivi per cui ancora pochi studi sono stati condotti in questo senso risiede nell’inadeguatezza di molti dei tradizionali sistemi di Motion Capture rispetto all’impiego subacqueo. La nuova branca della Markerless Motion Capture potrebbe invece in questo senso rappresentare una soluzione. In particolare, ci si occuperà in questo lavoro di tesi della tecnica markerless basata sulla ricostruzione del visual hull per retroproiezione delle silhouette. Il processo iniziale che permette di ottenere le silhouette dai video delle acquisizioni è detto segmentazione, la quale è anche una fase particolarmente importante per ottenere una buona accuratezza finale nella ricostruzione della cinematica articolare. Si sono pertanto sviluppati e caratterizzati in questo lavoro di tesi sette algoritmi di segmentazione, nati specificamente nell’ottica dell’analisi del cammino in acqua con tecnica markerless. Si mostrerà inoltre come determinate caratteristiche degli algoritmi influenzino la qualità finale della segmentazione, e sarà infine presentato un ulteriore algoritmo di post-processing per il miglioramento della qualità delle immagini segmentate.

Ingegneria di Manutenzione

Lo scopo di questa tesi di dottorato di ricerca consiste nel fornire la giusta collocazione della manutenzione fra le discipline dell'ingegneria, raccogliendo e formalizzando le metodologie di analisi di affidabilità e di pianificazione degli interventi all'interno di un unico processo di progettazione e di controllo. In linea di principio, un processo di analisi dei guasti e di programmazione della manutenzione deve essere in grado di fornire chiare e sicure risposte ai seguenti interrogativi: Quali sono le funzioni richieste e con quali criteri di prestazioni il sistema è chiamato ad assolverle? Qual'è l'andamento della disponibilità del sistema in funzione del tempo? Quanti guasti e di quale tipo si possono verificare durante la vita del sistema? Quali possono essere le conseguenze che ledono la sicurezza e la protezione ambientale? Quanti pezzi di ricambio sono necessari? Che tipo di interventi di manutenzione preventiva risultano tecnicamente fattibili? A quali scadenze devono essere programmati? A quanto ammonta la previsione del costo di esercizio del sistema? Quante squadre di manutenzione devono essere assegnate al sistema? Come deve essere organizzata la logistica di manutenzione? Con quali tecniche si prevede di riconoscere i guasti e quali procedure devono essere attivate per farvi fronte? E' possibile implementare tecniche di `condition monitoring' delle macchine? Su quali tempi di preavviso sui guasti si può contare? In tal senso, la manutenzione necessita delle tecniche e degli opportuni strumenti che siano in grado di misurarne l'efficacia e l'efficienza. L'efficacia in primo luogo, in quanto l'obiettivo principe consiste nel garantire che il sistema oggetto di studio continui a svolgere le proprie funzioni nei limiti di prestazioni accettabili, secondo le specifiche richieste degli utilizzatori. L'efficienza in secondo luogo, ma non per questo di minore importanza, in quanto perseguendo l'obiettivo di cui sopra, occorre impegnare il minimo di risorse possibili, organizzando con razionalità il supporto logistico del sistema al fine di raggiungere i massimi livelli di rendimento di gestione. La migliore strategia di manutenzione può essere pianificata, a priori, solo se si è in grado di prevedere con la necessaria precisione l'evoluzione del sistema nel suo contesto operativo futuro. E' allora possibile formulare un modello matematico del sistema, studiarne la dinamica ed osservare le reazioni alla simulazione di eventuali stimoli esterni. I metodi ed i modelli noti dell'ingegneria dei sistemi possono essere molto utili per la risoluzione di casi semplici, ma sovente richiedono la formulazione di ipotesi troppo restrittive che aumentano in modo inaccettabile la distanza del modello dalla realtà. Una strada alternativa ed affascinante, che ho percorso con entusiasmo durante questi tre anni di studi e ricerca, consiste nella simulazione numerica della vita del sistema, utilizzando il metodo Monte Carlo per la gestione dei processi stocastici di guasto e per l'esecuzione degli interventi di manutenzione. Ho quindi messo a punto il codice di simulazione RAMSES, perseguendo l'idea di costruire uno strumento di misura dell'efficacia e dell'efficienza di una politica di manutenzione simulata al calcolatore. Nella tesi si presentano i concetti di base dell'ingegneria dei sistemi applicata al caso della manutenzione e si introduce il formalismo della Reliability Centred Maintenance come miglior guida nella pianificazione delle schede di manutenzione. Si introducono le nozioni di base per fornire una struttura solida e corretta alla simulazione numerica dei sistemi riparabili e si presenta il codice RAMSES corredando le informazioni tecniche con i dovuti esempi ed applicazioni pratiche. Si conclude il lavoro, infine, con la presentazione di un modello di massima verosimiglianza particolarmente utile per le analisi dei dati sperimentali di guasto dei componenti.

Progettazione ed ottimizzazione del telaio di una macchina automatica formatrice per brick

Progettazione del telaio di una macchina automatica formatrice per brik. Per giungere a tale risultato è stato fondamentale risalire alla definizione delle leggi di moto e dei sistemi a camme generanti il movimento delle parti, per poter calcolare correttamente i carichi in gioco sollecitanti la struttura.

La Ricostruzione 3D di Bologna nel XVI Secolo

Il lavoro presentato ha come oggetto la ricostruzione tridimensionale della città di Bologna nella sua fase rinascimentale. Tale lavoro vuole fornire un modello 3D delle architetture e degli spazi urbani utilizzabile sia per scopi di ricerca nell’ambito della storia delle città sia per un uso didattico-divulgativo nel settore del turismo culturale. La base del lavoro è una fonte iconografica di grande importanza: l’affresco raffigurante Bologna risalente al 1575 e situato in Vaticano; questa è una veduta a volo d’uccello di grandi dimensioni dell’intero tessuto urbano bolognese all’interno della terza cerchia di mura. In esso sono rappresentate in maniera particolareggiata le architetture civili e ecclesiastiche, gli spazi ortivi e cortilivi interni agli isolati e alcune importanti strutture urbane presenti in città alla fine del Cinquecento, come l’area portuale e i canali interni alla città, oggi non più visibili. La ricostruzione tridimensionale è stata realizzata tramite Blender, software per la modellazione 3D opensource, attraverso le fasi di modellazione, texturing e creazione materiali (mediante campionamento delle principali cromie presenti nell’affresco), illuminazione e animazione. Una parte della modellazione è stata poi testata all’interno di un GIS per verificare l’utilizzo delle geometrie 3D come elementi collegabili ad altre fonti storiche relative allo sviluppo urbano e quindi sfruttabili per la ricerca storica. Grande attenzione infine è stata data all’uso dei modelli virtuali a scopo didattico-divulgativo e per il turismo culturale. La modellazione è stata utilizzata all’interno di un motore grafico 3D per costruire un ambiente virtuale interattivo nel quale un utente anche non esperto possa muoversi per esplorare gli spazi urbani della Bologna del Cinquecento. In ultimo è stato impostato lo sviluppo di un’applicazione per sistemi mobile (Iphone e Ipad) al fine di fornire uno strumento per la conoscenza della città storica in mobilità, attraverso la comparazione dello stato attuale con quello ricostruito virtualmente.

Fluidodinamica biomedica computazionale del flusso sanguigno in presenza di affezioni strumentali e/o patologiche

La tesi di Dottorato studia il flusso sanguigno tramite un codice agli elementi finiti (COMSOL Multiphysics). Nell’arteria è presente un catetere Doppler (in posizione concentrica o decentrata rispetto all’asse di simmetria) o di stenosi di varia forma ed estensione. Le arterie sono solidi cilindrici rigidi, elastici o iperelastici. Le arterie hanno diametri di 6 mm, 5 mm, 4 mm e 2 mm. Il flusso ematico è in regime laminare stazionario e transitorio, ed il sangue è un fluido non-Newtoniano di Casson, modificato secondo la formulazione di Gonzales & Moraga. Le analisi numeriche sono realizzate in domini tridimensionali e bidimensionali, in quest’ultimo caso analizzando l’interazione fluido-strutturale. Nei casi tridimensionali, le arterie (simulazioni fluidodinamiche) sono infinitamente rigide: ricavato il campo di pressione si procede quindi all’analisi strutturale, per determinare le variazioni di sezione e la permanenza del disturbo sul flusso. La portata sanguigna è determinata nei casi tridimensionali con catetere individuando tre valori (massimo, minimo e medio); mentre per i casi 2D e tridimensionali con arterie stenotiche la legge di pressione riproduce l’impulso ematico. La mesh è triangolare (2D) o tetraedrica (3D), infittita alla parete ed a valle dell’ostacolo, per catturare le ricircolazioni. Alla tesi sono allegate due appendici, che studiano con codici CFD la trasmissione del calore in microcanali e l’ evaporazione di gocce d’acqua in sistemi non confinati. La fluidodinamica nei microcanali è analoga all’emodinamica nei capillari. Il metodo Euleriano-Lagrangiano (simulazioni dell’evaporazione) schematizza la natura mista del sangue. La parte inerente ai microcanali analizza il transitorio a seguito dell’applicazione di un flusso termico variabile nel tempo, variando velocità in ingresso e dimensioni del microcanale. L’indagine sull’evaporazione di gocce è un’analisi parametrica in 3D, che esamina il peso del singolo parametro (temperatura esterna, diametro iniziale, umidità relativa, velocità iniziale, coefficiente di diffusione) per individuare quello che influenza maggiormente il fenomeno.

Cloud Computing: analisi dei modelli architetturali e delle tecnologie per lo sviluppo di applicazioni

Uno dei temi più discussi ed interessanti nel mondo dell’informatica al giorno d’oggi è sicuramente il Cloud Computing. Nuove organizzazioni che offrono servizi di questo tipo stanno nascendo ovunque e molte aziende oggi desiderano imparare ad utilizzarli, migrando i loro centri di dati e le loro applicazioni nel Cloud. Ciò sta avvenendo anche grazie alla spinta sempre più forte che stanno imprimendo le grandi compagnie nella comunità informatica: Google, Amazon, Microsoft, Apple e tante altre ancora parlano sempre più frequentemente di Cloud Computing e si stanno a loro volta ristrutturando profondamente per poter offrire servizi Cloud adeguandosi così a questo grande cambiamento che sta avvenendo nel settore dell’informatica. Tuttavia il grande movimento di energie, capitali, investimenti ed interesse che l’avvento del Cloud Computing sta causando non aiuta a comprendere in realtà che cosa esso sia, al punto tale che oggi non ne esiste ancora una definizione univoca e condivisa. La grande pressione inoltre che esso subisce da parte del mondo del mercato fa sì che molte delle sue più peculiari caratteristiche, dal punto di vista dell’ingegneria del software, vengano nascoste e soverchiate da altre sue proprietà, architetturalmente meno importanti, ma con un più grande impatto sul pubblico di potenziali clienti. L’obbiettivo che ci poniamo con questa tesi è quindi quello di esplorare il nascente mondo del Cloud Computing, cercando di comprenderne a fondo le principali caratteristiche architetturali e focalizzando l’attenzione in particolare sullo sviluppo di applicazioni in ambiente Cloud, processo che sotto alcuni aspetti si differenzia molto dallo sviluppo orientato ad ambienti più classici. La tesi è così strutturata: nel primo capitolo verrà fornita una panoramica sul Cloud Computing nella quale saranno date anche le prime definizioni e verranno esposti tutti i temi fondamentali sviluppati nei capitoli successivi. Il secondo capitolo costituisce un approfondimento su un argomento specifico, quello dei Cloud Operating System, componenti fondamentali che permettono di trasformare una qualunque infrastruttura informatica in un’infrastruttura Cloud. Essi verranno presentati anche per mezzo di molte analogie con i classici sistemi operativi desktop. Con il terzo capitolo ci si addentra più a fondo nel cuore del Cloud Computing, studiandone il livello chiamato Infrastructure as a Service tramite un esempio concreto di Cloud provider: Amazon, che fornisce i suoi servizi nel progetto Amazon Web Services. A questo punto, più volte nel corso della trattazione di vari temi saremo stati costretti ad affrontare le problematiche relative alla gestione di enormi moli di dati, che spesso sono il punto centrale di molte applicazioni Cloud. Ci è parso quindi importante approfondire questo argomento in un capitolo appositamente dedicato, il quarto, supportando anche in questo caso la trattazione teorica con un esempio concreto: BigTable, il sistema di Google per la gestione della memorizzazione di grandi quantità di dati. Dopo questo intermezzo, la trattazione procede risalendo lungo i livelli dell’architettura Cloud, ricalcando anche quella che è stata l’evoluzione temporale del Cloud Computing: nel quinto capitolo, dal livello Infrastructure as a Service si passa quindi a quello Platform as a Service, tramite lo studio dei servizi offerti da Google Cloud Platform. Il sesto capitolo costituisce invece il punto centrale della tesi, quello che ne soddisfa l’obbiettivo principale: esso contiene infatti uno studio approfondito sullo sviluppo di applicazioni orientate all’ambiente Cloud. Infine, il settimo capitolo si pone come un ponte verso possibili sviluppi futuri, analizzando quali sono i limiti principali delle tecnologie, dei modelli e dei linguaggi che oggi supportano il Cloud Computing. In esso viene proposto come possibile soluzione il modello ad attori; inoltre viene anche presentato il framework Orleans, che Microsoft sta sviluppando negli ultimi anni con lo scopo appunto di supportare lo sviluppo di applicazioni in ambiente Cloud.

Sviluppo di Applicazioni Mobile Platform-independent: il Linguaggio e Piattaforma Mobl

L’obbiettivo di questa tesi consiste in un analisi dello sviluppo di applicazioni mobile, rivolgendo particolare attenzione riguardo a quelle soluzioni che consentono di astrarre dall’ambiente su cui effettivamente queste verranno eseguite, per poi prendere in esame la piattaforma e il linguaggio Mobl. Sarà quindi necessario effettuare una panoramica sullo stato attuale del mercato, introducendo i diversi sistemi presenti e le metodologie proposte per la costruzione del software. Da questo studio sarà possibile ricavare i pregi e i difetti di una programmazione nativa. Volendo, in seguito, ricercare un processo di produzione software che favorisca un’indipendenza dai sistemi precedentemente descritti, verranno illustrati alcuni tra i più importanti Mobile Frameworks e tra questi si prenderà in esame Mobl, che si contraddistingue grazie a caratteristiche peculiari.