Specification and Verification of Declarative Open Interaction Models - A Logic-based framework

The advent of distributed and heterogeneous systems has laid the foundation for the birth of new architectural paradigms, in which many separated and autonomous entities collaborate and interact to the aim of achieving complex strategic goals, impossible to be accomplished on their own. A non exhaustive list of systems targeted by such paradigms includes Business Process Management, Clinical Guidelines and Careflow Protocols, Service-Oriented and Multi-Agent Systems. It is largely recognized that engineering these systems requires novel modeling techniques. In particular, many authors are claiming that an open, declarative perspective is needed to complement the closed, procedural nature of the state of the art specification languages. For example, the ConDec language has been recently proposed to target the declarative and open specification of Business Processes, overcoming the over-specification and over-constraining issues of classical procedural approaches. On the one hand, the success of such novel modeling languages strongly depends on their usability by non-IT savvy: they must provide an appealing, intuitive graphical front-end. On the other hand, they must be prone to verification, in order to guarantee the trustworthiness and reliability of the developed model, as well as to ensure that the actual executions of the system effectively comply with it. In this dissertation, we claim that Computational Logic is a suitable framework for dealing with the specification, verification, execution, monitoring and analysis of these systems. We propose to adopt an extended version of the ConDec language for specifying interaction models with a declarative, open flavor. We show how all the (extended) ConDec constructs can be automatically translated to the CLIMB Computational Logic-based language, and illustrate how its corresponding reasoning techniques can be successfully exploited to provide support and verification capabilities along the whole life cycle of the targeted systems.

Un applicativo Web con tecnologia single-page AJAX, servizi REST e grafica X3D, per la configurazione di modelli CAD tridimensionali

In questa tesi è stato realizzato un sistema web-based, per la configurazione di modelli meccanici tridimensionali. L’intero software è basato su architettura multi-tier. Il back-end espone servizi RESTful che permettono l’interrogazione di una base di dati contenente l’anagrafica dei modelli e l’interazione con il CAD 3D SolidWorks. Il front-end è rappresentato da due pagine HTML ideate come SPA (Single Page Application), una per l’amministratore e l’altra per l’utente finale; esse sono responsabili delle chiamate asincrone verso i servizi, dell’aggiornamento automatico dell’interfaccia e dell’interazione con immagini tridimensionali.

A new double laser pulse pumping scheme for transient collisionally excited plasma soft X-ray lasers

Within this thesis a new double laser pulse pumping scheme for plasma-based, transient collisionally excited soft x-ray lasers (SXRL) was developed, characterized and utilized for applications. SXRL operations from ~50 up to ~200 electron volt were demonstrated applying this concept. As a central technical tool, a special Mach-Zehnder interferometer in the chirped pulse amplification (CPA) laser front-end was developed for the generation of fully controllable double-pulses to optimally pump SXRLs.rnThis Mach-Zehnder device is fully controllable and enables the creation of two CPA pulses of different pulse duration and variable energy balance with an adjustable time delay. Besides the SXRL pumping, the double-pulse configuration was applied to determine the B-integral in the CPA laser system by amplifying short pulse replica in the system, followed by an analysis in the time domain. The measurement of B-integral values in the 0.1 to 1.5 radian range, only limited by the reachable laser parameters, proved to be a promising tool to characterize nonlinear effects in the CPA laser systems.rnContributing to the issue of SXRL pumping, the double-pulse was configured to optimally produce the gain medium of the SXRL amplification. The focusing geometry of the two collinear pulses under the same grazing incidence angle on the target, significantly improved the generation of the active plasma medium. On one hand the effect was induced by the intrinsically guaranteed exact overlap of the two pulses on the target, and on the other hand by the grazing incidence pre-pulse plasma generation, which allows for a SXRL operation at higher electron densities, enabling higher gain in longer wavelength SXRLs and higher efficiency at shorter wavelength SXRLs. The observation of gain enhancement was confirmed by plasma hydrodynamic simulations.rnThe first introduction of double short-pulse single-beam grazing incidence pumping for SXRL pumping below 20 nanometer at the laser facility PHELIX in Darmstadt (Germany), resulted in a reliable operation of a nickel-like palladium SXRL at 14.7 nanometer with a pump energy threshold strongly reduced to less than 500 millijoule. With the adaptation of the concept, namely double-pulse single-beam grazing incidence pumping (DGRIP) and the transfer of this technology to the laser facility LASERIX in Palaiseau (France), improved efficiency and stability of table-top high-repetition soft x-ray lasers in the wavelength region below 20 nanometer was demonstrated. With a total pump laser energy below 1 joule the target, 2 mircojoule of nickel-like molybdenum soft x-ray laser emission at 18.9 nanometer was obtained at 10 hertz repetition rate, proving the attractiveness for high average power operation. An easy and rapid alignment procedure fulfilled the requirements for a sophisticated installation, and the highly stable output satisfied the need for a reliable strong SXRL source. The qualities of the DGRIP scheme were confirmed in an irradiation operation on user samples with over 50.000 shots corresponding to a deposited energy of ~ 50 millijoule.rnThe generation of double-pulses with high energies up to ~120 joule enabled the transfer to shorter wavelength SXRL operation at the laser facility PHELIX. The application of DGRIP proved to be a simple and efficient method for the generation of soft x-ray lasers below 10 nanometer. Nickel-like samarium soft x-ray lasing at 7.3 nanometer was achieved at a low total pump energy threshold of 36 joule, which confirmed the suitability of the applied pumping scheme. A reliable and stable SXRL operation was demonstrated, due to the single-beam pumping geometry despite the large optical apertures. The soft x-ray lasing of nickel-like samarium was an important milestone for the feasibility of applying the pumping scheme also for higher pumping pulse energies, which are necessary to obtain soft x-ray laser wavelengths in the water window. The reduction of the total pump energy below 40 joule for 7.3 nanometer short wavelength lasing now fulfilled the requirement for the installation at the high-repetition rate operation laser facility LASERIX.rn

Temperature Variation Aware Energy Optimization in Heterogeneous MPSoCs

Thermal effects are rapidly gaining importance in nanometer heterogeneous integrated systems. Increased power density, coupled with spatio-temporal variability of chip workload, cause lateral and vertical temperature non-uniformities (variations) in the chip structure. The assumption of an uniform temperature for a large circuit leads to inaccurate determination of key design parameters. To improve design quality, we need precise estimation of temperature at detailed spatial resolution which is very computationally intensive. Consequently, thermal analysis of the designs needs to be done at multiple levels of granularity. To further investigate the flow of chip/package thermal analysis we exploit the Intel Single Chip Cloud Computer (SCC) and propose a methodology for calibration of SCC on-die temperature sensors. We also develop an infrastructure for online monitoring of SCC temperature sensor readings and SCC power consumption. Having the thermal simulation tool in hand, we propose MiMAPT, an approach for analyzing delay, power and temperature in digital integrated circuits. MiMAPT integrates seamlessly into industrial Front-end and Back-end chip design flows. It accounts for temperature non-uniformities and self-heating while performing analysis. Furthermore, we extend the temperature variation aware analysis of designs to 3D MPSoCs with Wide-I/O DRAM. We improve the DRAM refresh power by considering the lateral and vertical temperature variations in the 3D structure and adapting the per-DRAM-bank refresh period accordingly. We develop an advanced virtual platform which models the performance, power, and thermal behavior of a 3D-integrated MPSoC with Wide-I/O DRAMs in detail. Moving towards real-world multi-core heterogeneous SoC designs, a reconfigurable heterogeneous platform (ZYNQ) is exploited to further study the performance and energy efficiency of various CPU-accelerator data sharing methods in heterogeneous hardware architectures. A complete hardware accelerator featuring clusters of OpenRISC CPUs, with dynamic address remapping capability is built and verified on a real hardware.

Design of a GNSS receiver for the ESEO mission

This thesis was carried out inside the ESA's ESEO mission and focus in the design of one of the secondary payloads carried on board the spacecraft: a GNSS receiver for orbit determination. The purpose of this project is to test the technology of the orbit determination in real time applications by using commercial components. The architecture of the receiver includes a custom part, the navigation computer, and a commercial part, the front-end, from Novatel, with COCOM limitation removed, and a GNSS antenna. This choice is motivated by the goal of demonstrating the correct operations in orbit, enabling a widespread use of this technology while lowering the cost and time of the device’s assembly. The commercial front-end performs GNSS signal acquisition, tracking and data demodulation and provides raw GNSS data to the custom computer. This computer processes this raw observables, that will be both transferred to the On-Board Computer and then transmitted to Earth and provided as input to the recursive estimation filter on-board, in order to obtain an accurate positioning of the spacecraft, using the dynamic model. The main purpose of this thesis, is the detailed design and development of the mentioned GNSS receiver up to the ESEO project Critical Design Review, including requirements definition, hardware design and breadboard preliminary test phase design.

Geophotohunt: Studio di algoritmi di confronto di immagini per realizzare una caccia al tesoro fotografica

Questo studio si propone di realizzare un’applicazione per dispositivi Android che permetta, per mezzo di un gioco di ruolo strutturato come caccia al tesoro, di visitare in prima persona città d’arte e luoghi turistici. Gli utenti finali, grazie alle funzionalità dell’app stessa, potranno giocare, creare e condividere cacce al tesoro basate sulla ricerca di edifici, monumenti, luoghi di rilevanza artistico-storica o turistica; in particolare al fine di completare ciascuna tappa di una caccia al tesoro il giocatore dovrà scattare una fotografia al monumento o edificio descritto nell’obiettivo della caccia stessa. Il software grazie ai dati rilevati tramite GPS e giroscopio (qualora il dispositivo ne sia dotato) e per mezzo di un algoritmo di instance recognition sarà in grado di affermare se la foto scattata rappresenta la risposta corretta al quesito della tappa. L’applicazione GeoPhotoHunt rappresenta non solo uno strumento ludico per la visita di città turistiche o più in generale luoghi di interesse, lo studio propone, infatti come suo contributo originale, l’implementazione su piattaforma mobile di un Content Based Image Retrieval System (CBIR) del tutto indipendente da un supporto server. Nello specifico il server dell’applicazione non sarà altro che uno strumento di appoggio con il quale i membri della “community” di GeoPhotoHunt potranno pubblicare le cacce al tesoro da loro create e condividere i punteggi che hanno totalizzato partecipando a una caccia al tesoro. In questo modo quando un utente ha scaricato sul proprio smartphone i dati di una caccia al tesoro potrà iniziare l’avventura anche in assenza di una connessione internet. L’intero studio è stato suddiviso in più fasi, ognuna di queste corrisponde ad una specifica sezione dell’elaborato che segue. In primo luogo si sono effettuate delle ricerche, soprattutto nel web, con lo scopo di individuare altre applicazioni che implementano l’idea della caccia al tesoro su piattaforma mobile o applicazioni che implementassero algoritmi di instance recognition direttamente su smartphone. In secondo luogo si è ricercato in letteratura quali fossero gli algoritmi di riconoscimento di immagini più largamente diffusi e studiati in modo da avere una panoramica dei metodi da testare per poi fare la scelta dell’algoritmo più adatto al caso di studio. Quindi si è proceduto con lo sviluppo dell’applicazione GeoPhotoHunt stessa, sia per quanto riguarda l’app front-end per dispositivi Android sia la parte back-end server. Infine si è passati ad una fase di test di algoritmi di riconoscimento di immagini in modo di avere una sufficiente quantità di dati sperimentali da permettere di effettuare una scelta dell’algoritmo più adatto al caso di studio. Al termine della fase di testing si è deciso di implementare su Android un algoritmo basato sulla distanza tra istogrammi di colore costruiti sulla scala cromatica HSV, questo metodo pur non essendo robusto in presenza di variazioni di luminosità e contrasto, rappresenta un buon compromesso tra prestazioni, complessità computazionale in modo da rendere la user experience quanto più coinvolgente.

Progettazione ed implementazione di un dispositivo portabile per l'acquisizione ed il filtraggio di segnali biomedici

The use of wearable devices for the monitoring of biological potentials is an ever-growing area of research. Wearable devices for the monitoring of vital signs such as heart-rate, respiratory rate, cardiac output and blood oxygenation are necessary in determining the overall health of a patient and allowing earlier detection of adverse events such as heart attacks and strokes and earlier diagnosis of disease. This thesis describes a bio-potential acquisition embedded system designed with an innovative analog front-end, showing the performance in EMG and ECG applications and the comparison between different noise reduction algorithms. We demonstrate that the proposed system is able to acquire bio-potentials with a signal quality equivalent to state of the art bench-top biomedical devices and can be therefore used for monitoring purpose, with the advantages of a low-cost low-power wearable device.

Firmware development and testing for L1/L2 IBL upgrade

Il lavoro di questa tesi riguarda principalmente l'upgrade, la simulazione e il test di schede VME chiamate ReadOut Driver (ROD), che sono parte della catena di elaborazione ed acquisizione dati di IBL (Insertable B-Layer). IBL è il nuovo componente del Pixel Detector dell'esperimento ATLAS al Cern che è stato inserito nel detector durante lo shut down di LHC; fino al 2012 infatti il Pixel Detector era costituito da tre layer, chiamati (partendo dal più interno): Barrel Layer 0, Layer 1 e Layer 2. Tuttavia, l'aumento di luminosità di LHC, l'invecchiamento dei pixel e la richiesta di avere misure sempre più precise, portarono alla necessità di migliorare il rivelatore. Così, a partire dall'inizio del 2013, IBL (che fino a quel momento era stato un progetto sviluppato e finanziato separatamente dal Pixel Detector) è diventato parte del Pixel Detector di ATLAS ed è stato installato tra la beam-pipe e il layer B0. Questa tesi fornirà innanzitutto una panoramica generale dell'esperimento ATLAS al CERN, includendo aspetti sia fisici sia tecnici, poi tratterà in dettaglio le varie parti del rivelatore, con particolare attenzione su Insertable B-Layer. Su quest'ultimo punto la tesi si focalizzerà sui motivi che ne hanno portato alla costruzione, sugli aspetti di design, sulle tecnologie utilizzate (volte a rendere nel miglior modo possibile compatibili IBL e il resto del Pixel Detector) e sulle scelte di sviluppo e fabbricazione. La tesi tratterà poi la catena di read-out dei dati, descrivendo le tecniche di interfacciamento con i chip di front-end, ed in particolare si concentrerà sul lavoro svolto per l'upgrade e lo sviluppo delle schede ReadOut Drivers (ROD) introducendo le migliorie da me apportate, volte a eliminare eventuali difetti, migliorare le prestazioni ed a predisporre il sistema ad una analisi prestazionale del rivelatore. Allo stato attuale le schede sono state prodotte e montate e sono già parte del sistema di acquisizione dati del Pixel Detector di ATLAS, ma il firmware è in continuo aggiornamento. Il mio lavoro si è principalmente focalizzato sul debugging e il miglioramento delle schede ROD; in particolare ho aggiunto due features: - programmazione parallela delle FPGA} delle ROD via VME. IBL richiede l'utilizzo di 15 schede ROD e programmandole tutte insieme (invece che una alla volta) porta ad un sensibile guadagno nei tempi di programmazione. Questo è utile soprattutto in fase di test; - reset del Phase-Locked Loop (PLL)} tramite VME. Il PLL è un chip presente nelle ROD che distribuisce il clock a tutte le componenti della scheda. Avere la possibilità di resettare questo chip da remoto permette di risolvere problemi di sincronizzazione. Le ReadOut Driver saranno inoltre utilizzate da più layer del Pixel Detector. Infatti oltre ad IBL anche i dati provenienti dai layer 1 e 2 dei sensori a pixel dell’esperimento ATLAS verranno acquisiti sfruttando la catena hardware progettata, realizzata e testata a Bologna.

Find to play Android App

L’argomento centrale della tesi sono i centri sportivi, l’applicazione permette quindi all’utente di cercare un centro sportivo per nome, per città o per provincia. Consente inoltre di visualizzare la disponibilità per ogni campo offerto dalle strutture ed eventualmente di effettuare una prenotazione. Il centro sportivo renderà disponibili informazioni altrimenti difficilmente reperibili come gli orari, il numero telefonico, l’indirizzo, ecc.. Il progetto si compone di una parte front end e una parte back end. Il front consiste in un’applicazione android nativo (sviluppata in java). Il back-end invece vede un applicativo basato su ASP.NET Web API 2, con db Entity Framework Code First. Per la gestione degli user è stato scelto il framework ASP.NET Identity 2.1.

Metodologie di sviluppo agile per il corporate banking

L’applicazione dei metodi tradizionali dell’ingegneria del software non garantiscono il successo di un progetto, per questo motivo da circa quindici anni è emersa una nuova filosofia di sviluppo nota come Agile Software Development. In questa tesi è stata decritta una panoramica sulle metodologie agili, con particolare attenzione al framework Scrum e un caso di studio reale al quale Scrum è stato applicato. Il caso di studio riguarda l’implementazione di una applicazione web per la gestione del front-end di un Corporate Banking. L’applicazione di Scrum ha permesso di ottenere la soddisfazione del cliente finale, la crescita dello Scrum Team e un tasso di manutenzione correttiva accettabile.

SMARTDIAB: a communication and information technology approach for the intelligent monitoring, management and follow-up of type 1 diabetes patients

SMARTDIAB is a platform designed to support the monitoring, management, and treatment of patients with type 1 diabetes mellitus (T1DM), by combining state-of-the-art approaches in the fields of database (DB) technologies, communications, simulation algorithms, and data mining. SMARTDIAB consists mainly of two units: 1) the patient unit (PU); and 2) the patient management unit (PMU), which communicate with each other for data exchange. The PMU can be accessed by the PU through the internet using devices, such as PCs/laptops with direct internet access or mobile phones via a Wi-Fi/General Packet Radio Service access network. The PU consists of an insulin pump for subcutaneous insulin infusion to the patient and a continuous glucose measurement system. The aforementioned devices running a user-friendly application gather patient's related information and transmit it to the PMU. The PMU consists of a diabetes data management system (DDMS), a decision support system (DSS) that provides risk assessment for long-term diabetes complications, and an insulin infusion advisory system (IIAS), which reside on a Web server. The DDMS can be accessed from both medical personnel and patients, with appropriate security access rights and front-end interfaces. The DDMS, apart from being used for data storage/retrieval, provides also advanced tools for the intelligent processing of the patient's data, supporting the physician in decision making, regarding the patient's treatment. The IIAS is used to close the loop between the insulin pump and the continuous glucose monitoring system, by providing the pump with the appropriate insulin infusion rate in order to keep the patient's glucose levels within predefined limits. The pilot version of the SMARTDIAB has already been implemented, while the platform's evaluation in clinical environment is being in progress.

Corpus-Based Speech Enhancement With Uncertainty Modeling and Cepstral Smoothing

We present a new approach for corpus-based speech enhancement that significantly improves over a method published by Xiao and Nickel in 2010. Corpus-based enhancement systems do not merely filter an incoming noisy signal, but resynthesize its speech content via an inventory of pre-recorded clean signals. The goal of the procedure is to perceptually improve the sound of speech signals in background noise. The proposed new method modifies Xiao's method in four significant ways. Firstly, it employs a Gaussian mixture model (GMM) instead of a vector quantizer in the phoneme recognition front-end. Secondly, the state decoding of the recognition stage is supported with an uncertainty modeling technique. With the GMM and the uncertainty modeling it is possible to eliminate the need for noise dependent system training. Thirdly, the post-processing of the original method via sinusoidal modeling is replaced with a powerful cepstral smoothing operation. And lastly, due to the improvements of these modifications, it is possible to extend the operational bandwidth of the procedure from 4 kHz to 8 kHz. The performance of the proposed method was evaluated across different noise types and different signal-to-noise ratios. The new method was able to significantly outperform traditional methods, including the one by Xiao and Nickel, in terms of PESQ scores and other objective quality measures. Results of subjective CMOS tests over a smaller set of test samples support our claims.

Design and implementation of a 3D computer game controller using inertial MEMS sensors

Though 3D computer graphics has seen tremendous advancement in the past two decades, most available mechanisms for computer interaction in 3D are high cost and targeted for industry and virtual reality applications. Recent advances in Micro-Electro-Mechanical-System (MEMS) devices have brought forth a variety of new low-cost, low-power, miniature sensors with high accuracy, which are well suited for hand-held devices. In this work a novel design for a 3D computer game controller using inertial sensors is proposed, and a prototype device based on this design is implemented. The design incorporates MEMS accelerometers and gyroscopes from Analog Devices to measure the three components of the acceleration and angular velocity. From these sensor readings, the position and orientation of the hand-held compartment can be calculated using numerical methods. The implemented prototype is utilizes a USB 2.0 compliant interface for power and communication with the host system. A Microchip dsPIC microcontroller is used in the design. This microcontroller integrates the analog to digital converters, the program memory flash, as well as the core processor, on a single integrated circuit. A PC running Microsoft Windows operating system is used as the host machine. Prototype firmware for the microcontroller is developed and tested to establish the communication between the design and the host, and perform the data acquisition and initial filtering of the sensor data. A PC front-end application with a graphical interface is developed to communicate with the device, and allow real-time visualization of the acquired data.

Fourier optics study of traveling-wave excitation at short- wavelength plasma-lasing

Traveling-wave excitation close to the speed of light implies small-angle target-irradiation. Yet, short-wavelength lasing needs large irradiation angles. Pulse-front back-tilt is considered to overcome such trade-off. Pulse-front tilt by means of compressor misalignment was found effective only if coupled with a strong front-end imaging/focusing component.

A Baseline Wander Tracking System for Artifact Rejection in Long-Term Electrocardiography

Long-term electrocardiogram (ECG) signals might suffer from relevant baseline disturbances during physical activity. Motion artifacts in particular are more pronounced with dry surface or esophageal electrodes which are dedicated to prolonged ECG recording. In this paper we present a method called baseline wander tracking (BWT) that tracks and rejects strong baseline disturbances and avoids concurrent saturation of the analog front-end. The proposed algorithm shifts the baseline level of the ECG signal to the middle of the dynamic input range. Due to the fast offset shifts, that produce much steeper signal portions than the normal ECG waves, the true ECG signal can be reconstructed offline and filtered using computationally intensive algorithms. Based on Monte Carlo simulations we observed reconstruction errors mainly caused by the non-linearity inaccuracies of the DAC. However, the signal to error ratio of the BWT is higher compared to an analog front-end featuring a dynamic input ranges above 15 mV if a synthetic ECG signal was used. The BWT is additionally able to suppress (electrode) offset potentials without introducing long transients. Due to its structural simplicity, memory efficiency and the DC coupling capability, the BWT is dedicated to high integration required in long-term and low-power ECG recording systems.