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.

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.

Interpretazione delle proprietà meccaniche del sistema arterioso sistemico mediante modello Windkessel a quattro elementi.

Obiettivo della tesi è quello di effettuare una panoramica sull'evoluzione del modello Windkessel fino al modello a quattro elementi. In seguito si ha un analisi del comportamento dei modelli WK alternativi relativamente ad un campione di soggetti in età pediatrica confrontati con altri in età adulta.

Utilizzo di algoritmi genetici nell'ambito della bioingegneria: Applicazione alla identificazione di modelli cardiaci

In questo studio sarà trattato lo sviluppo degli algoritmi genetici, uno strumento di calcolo nato ispirandosi alle leggi Darwiniane sull’evoluzione naturale. Questi algoritmi, le cui basi furono introdotte a partire dagli anni '40, mirano alla risoluzione di una vasta categoria di problemi computazionali utilizzando un approccio differente, basato sulle regole di mutazione e ricombinazione proprie della genetica. Essi permettono infatti di valutare delle soluzioni di partenza e, grazie alle variazioni introdotte dalla modifica casuale o dalla ricombinazione di queste, crearne di nuove nel tentativo di convergere verso soluzioni ottimali. Questo studio si propone come una descrizione di questo strumento, dei suoi sviluppi e delle sue potenzialità in ambito bioingegneristico, focalizzandosi sul suo utilizzo recente nell’ identificazione parametrica di modelli cardiaci.

Dal medico di medicina generale al sistema integrato delle cure primarie: analisi e progettazione dell'architettura organizzativa di un modello in evoluzione.

L'oggetto della tesi è la costruzione di un modello organizzativo e funzionale per le nuove strutture previste a livello nazionale per l'assistenza primaria e denominate Unità Complesse di Cure Primarie (UCCP). Il modello è composto da un profilo organizzativo, un'architettura funzionale e un sistema di indicatori per il monitoraggio di un insieme di prestazioni rilevanti.

Definizione e validazione di un modello elettromeccanico per l'ottimizzazione dei servomeccanismi nelle macchine automatiche

In questo lavoro viene mostrato come costruire un modello elettromeccanico per il sistema costituito da motore elettrico-riduttore-trasmissione-carico. Il modello è progettato per essere implementato su software di simulazione. Sono illustrati aspetti relativi ai componenti del sistema, alla dinamica dei meccanismi, a modelli di perdite elettriche nei motori ed alle modalità di costruizione del software di simulazione. Sono infine mostrati i risultati di alcune simulazioni.

Modelli diffusivi ed effetti di ritardo nella conduzione del calore e nella dinamica delle popolazioni.

In questi tesi viene studiata la teoria classica di diffusione del calore come modello parabolico per cui viene calcolata una soluzione attraverso il metodo di separazione delle variabili e il metodo delle onde dispersive. Viene poi affrontata la teoria alternativa proposta da Cattaneo del modello iperbolico del calore, allo scopo di superare il paradosso di velocità di propagazione infinita. Si conclude con alcuni esempi in cui lo stesso ragionamento viene applicato in diverse teorie diffusive e di reazione-diffusione in ambiti bio-matematici, come ad esempio la dinamica delle popolazioni.

Realizzazione di un sistema di controllo per l'automazione dei test su veicolo a banco rulli

Per eseguire dei test automatizzati su una moto posta su banco a rulli, è necessario un software che permetta di gestire determinati attuatori sulla moto, in modo da poter simulare le condizioni di guida desiderate. Nel modello preso in esame, sono stati utilizzati Simulink e NI VeriStand. Simulink è un ambiente grafico di simulazione e analisi di sistemi dinamici completamente integrato con Matlab, caratterizzato dalla tipica interfaccia a blocchi, che possono essere personalizzati o scelti dalla libreria. Ni VeriStand è invece un ambiente software che permette di elaborare modelli scritti in Simulink in real time. Il presente lavoro è stato incentrato proprio su quest’ultimo aspetto. Per prima cosa è stata esaminata a fondo la parte del modello in Simulink, dopo di che è stata valutata la possibilità di riscrivere alcune parti del modello con un’applicazione interna a Simulink (StateFlow), che si potrebbe prestare meglio a simulare la logica di controllo rispetto a com’è gestita attualmente.

Cambiamenti epidemiologici dell'epatocarcinoma agli inizi del xxi secolo: Dal ruolo emergente delle malattie dismetaboliche quali fattori eziopatogemetici alla necessita' di revisione del sistema di stadiaziome

Introduzione e scopo: la rapida diffusione delle malattie dismetaboliche sta modificando l’epidemiologia dell’epatocarcinoma (HCC). Scopo della tesi è, attraverso quattro studi, analizzare l’impatto di questi cambiamenti nella gestione clinica del paziente affetto da HCC. Materiali e metodi: quattro studi di coorte, condotti con analisi retrospettiva del database ITA.LI.CA. Studio 1:3658 pazienti arruolati tra il 01-01-2001 ed il 31-12-2012 suddivisi in base alla data di diagnosi:2001-2004 (954 pazienti), 2005-2008 (1122 pazienti), 2009-2012 (1582 pazienti). Studio 2:analisi comparativa tra 756 pazienti con HCC-NAFLD e 611 pazienti con HCC-HCV. Studio 3:proposta di quattro modelli alternativi al BCLC originale con validazione di una proposta di sottostadiazione dell’intermedio, considerando 2606 pazienti arruolati tra il 01-01-2000 e il 31-12-2012 e riallocati secondo gradi diversi di perfomance status (PS). Studio 4:analisi di 696 pazienti con HCC in stadio intermedio diagnosticato dopo il 1999 stratificati per trattamento. Risultati: studio 1:progressivo aumento dell’età alla diagnosi e delle eziologie dismetaboliche; più frequente esordio dell’HCC in stadio precoce e con funzione epatica più conservata; aumento della sopravvivenza dopo il 2008. Studio 2:i pazienti con HCC-NAFLD mostrano più frequentemente un tumore infiltrativo diagnosticato fuori dai programmi di sorveglianza, con prognosi peggiore rispetto ai pazienti HCC-HCV. Questa differenza di sopravvivenza si elimina rimuovendo i fattori di confondimento attraverso propensity analysis. Studio 3:il PS1 non è un predittore indipendente di sopravvivenza. Il modello 4 (considerando PS1=PS0 e con la sottostadiazione proposta), ha la migliore capacità discriminativa. Studio 4:i trattamenti curativi riducono la mortalità più della TACE, anche dopo propensity analysis. Conclusioni: l’aumento delle patologie dismetaboliche comporterà diagnosi di malattia ad uno stadio più avanzato, quando sintomatica, rendendo necessario stabilire un programma di sorveglianza. Inoltre per una migliore stratificazione e gestione dei pazienti, bisogna riconsiderare il ruolo del PS ed offrire un ventaglio di opzioni terapeutiche anche per il pazienti in stadio intermedio.

Progettazione e sviluppo di un sistema distribuito per la gestione di transazioni finanziarie.

L'opera si propone di esplorare modelli innovativi, in particolare quello ad attori, per lo sviluppo di applicazioni enterprise distribuite con elevata scalabilità, prendendo come caso di studio lo sviluppo di un sistema per la gestione delle transazioni finanziarie in ambito petrolifero.

Transizione a stati congestionati in modelli di traffico

La congestione del traffico è un fenomeno molto familiare, con il quale si ha a che fare nelle più svariate occasioni. Dal punto di vista fisico, il flusso del traffico rappresenta un sistema di particelle interagenti (i ve- icoli) in condizione di non equilibrio. L’effetto complessivo di un sistema composto da molte particelle interagenti è la creazione di una instabil- ità, osservata empiricamente, nello stato di free flow (scorrimento libero), causata dall’aumentare delle fluttuazioni. In questi casi di parla di phan- tom traffic jam, ovvero una congestione che ha origine senza cause appar- enti, come incidenti o lavori in corso. Sarà dimostrato come la condizione di stop & go si verifichi spontaneamente se la densità media dei veicoli eccede un certo valore critico. L’importanza di poter predire una congestione stradale non è un problema puramente matematico, ma ha risvolti socio-economici non indifferenti. Infatti, le caratteristiche della mobilità e dei sistemi di trasporto sono strettamente legate alla struttura della comunità e alla qualità della vita. Con il seguente studio si cercherà di trovare un osservabile facilmente calcolabile, che potrebbe essere un predittore della formazione di uno stato congestionato con un intervallo di tempo sufficientemente adeguato. A tal fine sono state prese in considerazione misure relative alle condizioni del traffico su strade provinciali dell’Emilia-Romagna, tramite un sistema MTS composto da 3509 spire che registra i passaggi delle macchine; in seguito, per poter avere una comprensione maggiore dei fenomeni che si manifestano durante la transizione a stato congestionato, si è provveduto a creare un modello matematico utilizzato per le simulazioni al computer. I risultati ottenuti dalle simulazioni, poi, sono stati utilizzati per trovare l’osservabile cercato nei dati pervenuti dalle strade campione.

Uso del gas plasma per l'inattivazione di listeria monocytogenes in sistema modello e vegetali

Negli ultimi anni è aumentato l’interesse dell’industria verso lo sviluppo di tecnologie alternative ai trattamenti tradizionali degli alimenti. Tra le varie tecnologie non termiche troviamo il gas plasma. Il plasma è un gas ionizzato neutro, composto da diverse particelle. I principali agenti responsabili dell’azione battericida sembrano essere le specie reattive dell’ossigeno e dell’azoto, causando danni alle cellule microbiche. Recentemente si sta studiando l’“acqua plasmata attivata”. L’obiettivo generale di questa tesi è stato quello di verificare se trattamenti al plasma di soluzioni saline (NaCl 0.9%) possano “attivarle” dotandole di attività battericida nei confronti di un ceppo di Listeria monocytogenes (ceppo 56 Ly) e di stabilire se il materiale con cui sono costruiti gli elettrodi di un generatore di plasma del tipo DBD, possa influenzare l’efficacia delle soluzioni trattate. Si sono pertanto effettuati trattamenti al plasma di soluzioni saline utilizzando elettrodi di differenti materiali: vetro, ottone, acciaio, argento; le soluzioni così ottenute sono state analizzate in termini chimici, e se ne è valutata l’azione decontaminante nei confronti di Listeria monocytogenes 56 Ly nello stesso sistema modello e, in via preliminare, in sistema reale rappresentato da carote julienne deliberatamente contaminate con L. monocytogenes. Dai risultati ottenuti si è visto che la sensibilità di L. monocytogenes 56Ly alle soluzioni acquose trattate al plasma è influenzato sia dal tipo di materiale dell’elettrodo, sia dal tempo di esposizione. L’acciaio si è rivelato il materiale più efficace. Per quanto concerne il sistema reale, il lavaggio con acqua plasmata per 60 minuti ha determinato un livello di inattivazione di circa 1 ciclo logaritmico analogamente a quanto ottenuto con la soluzione di ipoclorito. In conclusione, i risultati ottenuti hanno evidenziato una minore efficacia dei trattamenti al plasma quando applicati ai sistemi reali, ma comunque il gas plasma ha delle buone potenzialità per la decontaminazione prodotti ortofrutticoli.