Type Systems for Distributed Programs: Components and Sessions

Modern software systems, in particular distributed ones, are everywhere around us and are at the basis of our everyday activities. Hence, guaranteeing their cor- rectness, consistency and safety is of paramount importance. Their complexity makes the verification of such properties a very challenging task. It is natural to expect that these systems are reliable and above all usable. i) In order to be reliable, compositional models of software systems need to account for consistent dynamic reconfiguration, i.e., changing at runtime the communication patterns of a program. ii) In order to be useful, compositional models of software systems need to account for interaction, which can be seen as communication patterns among components which collaborate together to achieve a common task. The aim of the Ph.D. was to develop powerful techniques based on formal methods for the verification of correctness, consistency and safety properties related to dynamic reconfiguration and communication in complex distributed systems. In particular, static analysis techniques based on types and type systems appeared to be an adequate methodology, considering their success in guaranteeing not only basic safety properties, but also more sophisticated ones like, deadlock or livelock freedom in a concurrent setting. The main contributions of this dissertation are twofold. i) On the components side: we design types and a type system for a concurrent object-oriented calculus to statically ensure consistency of dynamic reconfigurations related to modifications of communication patterns in a program during execution time. ii) On the communication side: we study advanced safety properties related to communication in complex distributed systems like deadlock-freedom, livelock- freedom and progress. Most importantly, we exploit an encoding of types and terms of a typical distributed language, session π-calculus, into the standard typed π- calculus, in order to understand their expressive power.

Analog Signal Acquisition and Conditioning for Near-Field Capacitive Communication and Active Combined EEG-EIT Monitoring

The work of the present thesis is focused on the implementation of microelectronic voltage sensing devices, with the purpose of transmitting and extracting analog information between devices of different nature at short distances or upon contact. Initally, chip-to-chip communication has been studied, and circuitry for 3D capacitive coupling has been implemented. Such circuits allow the communication between dies fabricated in different technologies. Due to their novelty, they are not standardized and currently not supported by standard CAD tools. In order to overcome such burden, a novel approach for the characterization of such communicating links has been proposed. This results in shorter design times and increased accuracy. Communication between an integrated circuit (IC) and a probe card has been extensively studied as well. Today wafer probing is a costly test procedure with many drawbacks, which could be overcome by a different communication approach such as capacitive coupling. For this reason wireless wafer probing has been investigated as an alternative approach to standard on-contact wafer probing. Interfaces between integrated circuits and biological systems have also been investigated. Active electrodes for simultaneous electroencephalography (EEG) and electrical impedance tomography (EIT) have been implemented for the first time in a 0.35 um process. Number of wires has been minimized by sharing the analog outputs and supply on a single wire, thus implementing electrodes that require only 4 wires for their operation. Minimization of wires reduces the cable weight and thus limits the patient's discomfort. The physical channel for communication between an IC and a biological medium is represented by the electrode itself. As this is a very crucial point for biopotential acquisitions, large efforts have been carried in order to investigate the different electrode technologies and geometries and an electromagnetic model is presented in order to characterize the properties of the electrode to skin interface.

Innovative architecture of on-board and on-ground radio systems for space communication

The radio communication system is one of the most critical system of the overall satellite platform: it often represents the only way of communication, between a spacecraft and the Ground Segment or among a constellation of satellites. This thesis focuses on specific innovative architectures for on-board and on-ground radio systems. In particular, this work is an integral part of a space program started in 2004 at the University of Bologna, Forlì campus, which led to the completion of the microsatellite ALMASat-1, successfully launched on-board the VEGA maiden flight. The success of this program led to the development of a second microsatellite, named ALMASat-EO, a three-axis stabilized microsatellite able to capture images of the Earth surface. Therefore, the first objective of this study was focused on the investigation of an innovative, efficient and low cost architecture for on-board radio communication systems. The TT&C system and the high data rate transmitter for images downlink design and realization are thoroughly described in this work, together with the development of the embedded hardware and the adopted antenna systems. Moreover, considering the increasing interest in the development of constellations of microsatellite, in particular those flying in close formations, a careful analysis has been carried out for the development of innovative communication protocols for inter-satellite links. Furthermore, in order to investigate the system aspects of space communications, a study has been carried out at ESOC having as objective the design, implementation and test of two experimental devices for the enhancement of the ESA GS. Thus, a significant portion of this thesis is dedicated to the description of the results of a method for improving the phase stability of GS radio frequency equipments by means of real-time phase compensation and a new way to perform two antennas arraying tracking using already existing ESA tracking stations facilities.

Wireless Networks for Body-Centric Communications

Progress in miniaturization of electronic components and design of wireless systems paved the way towards ubiquitous and pervasive communications, enabling anywhere and anytime connectivity. Wireless devices present on, inside, around the human body are becoming commonly used, leading to the class of body-centric communications. The presence of the body with all its peculiar characteristics has to be properly taken into account in the development and design of wireless networks in this context. This thesis addresses various aspects of body-centric communications, with the aim of investigating network performance achievable in different scenarios. The main original contributions pertain to the performance evaluation for Wireless Body Area Networks (WBANs) at the Medium Access Control layer: the application of Link Adaptation to these networks is proposed, Carrier Sense Multiple Access with Collision Avoidance algorithms used for WBAN are extensively investigated, coexistence with other wireless systems is examined. Then, an analytical model for interference in wireless access network is developed, which can be applied to the study of communication between devices located on humans and fixed nodes of an external infrastructure. Finally, results on experimental activities regarding the investigation of human mobility and sociality are presented.

Presa di decisione in situazioni rischiose: effetto della rabbia

The current studies assessed the role of trait anger and anger expression styles on risk decision-making in adulthood, adolescence and childhood. In the first experiment 158 adults completed the STAXI-2 and an inventory consisting of a battery of hypothetical everyday decision-making scenarios. Participants were also asked to evaluate the perception of risk for each chosen option and some contextual characteristics, that are familiarity and salience for each scenario. The study provides evidence for a relationship between individual differences in the tendency to feel and express anger and risky decisions and for mediation effects of familiarity and salience appraisals. Moreover, results indicated that trait anger was predictive of risk perception and they provide evidence for a positive relationship between risk decision-making and risk perception. In the second study, we examined the relationship between specific components of anger (i.e., cognitive, affective and behavioural) and risk decision-making in adolescents. 101 subjects completed specific tasks, measuring risk decision-making, assessed using hypothetical choice scenarios, and anger, evaluated through the STAXI-CA and the MSAI-R. Results showed that adolescents higher on hostility, anger experience and destructive expression, make more risky decisions in everyday life situations. Moreover, regression analyses indicated that destructive expression of anger and hostility were predictive of adolescents’ risky decisions. In the third experiment, 104 children completed three tasks: the STAXI-CA, the MSAI-R and a task measuring risk decision-making in everyday situations. Subjects were also asked to evaluate the degree of danger, benefit, fun and fear perceived for each risky choice. Analyses indicated that: (a) risk decision-making was predicted by both trait anger and outward expression of anger; (b) destructive expression o anger was predictive of children’s risky decisions; (c) appraisal of danger fully mediated the relation between trait anger and risk; (d) perceptions of benefit, scare and fun partially mediated the relationship between trait anger and risk; and (e) appraisal of danger partially mediated the relationship between outward expression of anger and risk decision-making. The results provide evidence for a relationship between dispositional anger and risk decision-making during childhood, suggesting a possible explanation of the mechanisms below. In particular, risk decision-making can be viewed as the output of cognitive and emotive processes, linked to dispositional anger that leads children to be amused, optimistic and fearless in potentially risky situations. These findings substantiate the importance of incorporating cognitive and emotive factors in theories that seek to explain the relationship between personality traits and risk decision making across a broad range of age.

Studio e sviluppo di sistemi RFID in banda UHF

The recent widespread diffusion of radio-frequency identification (RFID) applications operating in the UHF band has been supported by both the request for greater interrogation ranges and greater and faster data exchange. UHF-RFID systems, exploiting a physical interaction based on Electromagnetic propagation, introduce many problems that have not been fully explored for the previous generations of RFID systems (e.g. HF). Therefore, the availability of reliable tools for modeling and evaluating the radio-communication between Reader and Tag within an RFID radio-link are needed. The first part of the thesis discuss the impact of real environment on system performance. In particular an analytical closed form formulation for the back-scattered field from the Tag antenna and the formulation for the lower bound of the BER achievable at the Reader side will be presented, considering different possible electromagnetic impairments. By means of the previous formulations, of the analysis of the RFID link operating in near filed conditions and of some electromagnetic/system-level co-simulations, an in-depth study of the dimensioning parameters and the actual performance of the systems will be discussed and analyzed, showing some relevant properties and trade-offs in transponder and reader design. Moreover a new low cost approach to extend the read range of the RFID UHF passive systems will be discussed. Within the scope to check the reliability of the analysis approaches and of innovative proposals, some reference transponder antennas have been designed and extensive measurement campaign has been carried out with satisfactory results. Finally, some commercial ad-hoc transponder for industrial application have been designed within the cooperation with Datalogic s.p.a., some guidelines and results will be briefly presented.

Role of BDNF secretion and signaling in the activity-dependent refinement of synaptic connections

Neuronal networks exhibit diverse types of plasticity, including the activity-dependent regulation of synaptic functions and refinement of synaptic connections. In addition, continuous generation of new neurons in the “adult” brain (adult neurogenesis) represents a powerful form of structural plasticity establishing new connections and possibly implementing pre-existing neuronal circuits (Kempermann et al, 2000; Ming and Song, 2005). Neurotrophins, a family of neuronal growth factors, are crucially involved in the modulation of activity-dependent neuronal plasticity. The first evidence for the physiological importance of this role evolved from the observations that the local administration of neurotrophins has dramatic effects on the activity-dependent refinement of synaptic connections in the visual cortex (McAllister et al, 1999; Berardi et al, 2000; Thoenen, 1995). Moreover, the local availability of critical amounts of neurotrophins appears to be relevant for the ability of hippocampal neurons to undergo long-term potentiation (LTP) of the synaptic transmission (Lu, 2004; Aicardi et al, 2004). To achieve a comprehensive understanding of the modulatory role of neurotrophins in integrated neuronal systems, informations on the mechanisms about local neurotrophins synthesis and secretion as well as ditribution of their cognate receptors are of crucial importance. In the first part of this doctoral thesis I have used electrophysiological approaches and real-time imaging tecniques to investigate additional features about the regulation of neurotrophins secretion, namely the capability of the neurotrophin brain-derived neurotrophic factor (BDNF) to undergo synaptic recycling. In cortical and hippocampal slices as well as in dissociated cell cultures, neuronal activity rapidly enhances the neuronal expression and secretion of BDNF which is subsequently taken up by neurons themselves but also by perineuronal astrocytes, through the selective activation of BDNF receptors. Moreover, internalized BDNF becomes part of the releasable source of the neurotrophin, which is promptly recruited for activity-dependent recycling. Thus, we described for the first time that neurons and astrocytes contain an endocytic compartment competent for BDNF recycling, suggesting a specialized form of bidirectional communication between neurons and glia. The mechanism of BDNF recycling is reminiscent of that for neurotransmitters and identifies BDNF as a new modulator implicated in neuro- and glio-transmission. In the second part of this doctoral thesis I addressed the role of BDNF signaling in adult hippocampal neurogenesis. I have generated a transgenic mouse model to specifically investigate the influence of BDNF signaling on the generation, differentiation, survival and connectivity of newborn neurons into the adult hippocampal network. I demonstrated that the survival of newborn neurons critically depends on the activation of the BDNF receptor TrkB. The TrkB-dependent decision regarding life or death in these newborn neurons takes place right at the transition point of their morphological and functional maturation Before newborn neurons start to die, they exhibit a drastic reduction in dendritic complexity and spine density compared to wild-type newborn neurons, indicating that this receptor is required for the connectivity of newborn neurons. Both the failure to become integrated and subsequent dying lead to impaired LTP. Finally, mice lacking a functional TrkB in the restricted population of newborn neurons show behavioral deficits, namely increased anxiety-like behavior. These data suggest that the integration and establishment of proper connections by newly generated neurons into the pre-existing network are relevant features for regulating the emotional state of the animal.

Correlazioni tra proprietá reologiche, struttura e processabilitá di blend di LLDPE/LDPE

Polymer blends constitute a valuable way to produce relatively low cost new materials. A still open question concerns the miscibility of polyethylene blends. Deviations from the log-additivity rule of the newtonian viscosity are often taken as a signature of immiscibility of the two components. The aim of this thesis is to characterize the rheological behavior in shear and elongation of five series of LLDPE/LDPE blends whose parent polymers have been chosen with different viscosity and SCB content and length. Synergistic effects have been measured for both zero shear viscosity and melt strength. Both SCB length and viscosity ratio between the components have been found to be key parameters for the miscibility of the pure polymers. In particular the miscibility increases with increasing SCB length and with decreasing the LDPE molecular weight and viscosity. This rheological behavior has significant effects on the processability window of these blends when the uni or biaxial elongational flows are involved. The film blowing is one of the processes for which the synergistic effects above mentioned can be crucial. Small scale experiments of film blowing performed for one of the series of blends has demonstrated that the positive deviation of the melt strength enlarges the processability window. In particular, the bubble stability was found to improve or disappear when the melt strength of the samples increased. The blending of LDPE and LLDPE can even reduce undesired melt flow instability phenomena widening, as a consequence, the processability window in extrusion. One of the series of blends has been characterized by means of capillary rheometry in order to allow a careful morphological analysis of the surface of the extruded polymer jets by means of Scanning Electron Microscopy (SEM) with the aim to detect the very early stages of the small scale melt instabilty at low shear rates (sharksin) and to follow its subsequent evolution as long as the shear rate was increased. With this experimental procedure it was possible to evaluate the shear rate ranges corresponding to different flow regions: smooth extrudate surface (absence of instability), sharkskin (small scale instability produced at the capillary exit), stick-slip transition (instability involving the whole capillary wall) and gross melt fracture (i.e. a large scale "upstream" instability originating from the entrance region of the capillary). A quantitative map was finally worked out using which an assessment of the flow type for a given shear rate and blend composition can be predicted.

A hybrid technology for parallel recording of single ion channels

Hybrid technologies, thanks to the convergence of integrated microelectronic devices and new class of microfluidic structures could open new perspectives to the way how nanoscale events are discovered, monitored and controlled. The key point of this thesis is to evaluate the impact of such an approach into applications of ion-channel High Throughput Screening (HTS)platforms. This approach offers promising opportunities for the development of new classes of sensitive, reliable and cheap sensors. There are numerous advantages of embedding microelectronic readout structures strictly coupled to sensing elements. On the one hand the signal-to-noise-ratio is increased as a result of scaling. On the other, the readout miniaturization allows organization of sensors into arrays, increasing the capability of the platform in terms of number of acquired data, as required in the HTS approach, to improve sensing accuracy and reliabiity. However, accurate interface design is required to establish efficient communication between ionic-based and electronic-based signals. The work made in this thesis will show a first example of a complete parallel readout system with single ion channel resolution, using a compact and scalable hybrid architecture suitable to be interfaced to large array of sensors, ensuring simultaneous signal recording and smart control of the signal-to-noise ratio and bandwidth trade off. More specifically, an array of microfluidic polymer structures, hosting artificial lipid bilayers blocks where single ion channel pores are embededed, is coupled with an array of ultra-low noise current amplifiers for signal amplification and data processing. As demonstrating working example, the platform was used to acquire ultra small currents derived by single non-covalent molecular binding between alpha-hemolysin pores and beta-cyclodextrin molecules in artificial lipid membranes.

Functional photoactive and electroactive nanodevices

Most of current ultra-miniaturized devices are obtained by the top-down approach, in which nanoscale components are fabricated by cutting down larger precursors. Since this physical-engineering method is reaching its limits, especially for components below 30 nm in size, alternative strategies are necessary. Of particular appeal to chemists is the supramolecular bottom-up approach to nanotechnology, a methodology that utilizes the principles of molecular recognition to build materials and devices from molecular components. The subject of this thesis is the photophysical and electrochemical investigation of nanodevices obtained harnessing the principles of supramolecular chemistry. These systems operate in solution-based environments and are investigated at the ensemble level. The majority of the chemical systems discussed here are based on pseudorotaxanes and catenanes. Such supramolecular systems represent prototypes of molecular machines since they are capable of performing simple controlled mechanical movements. Their properties and operation are strictly related to the supramolecular interactions between molecular components (generally photoactive or electroactive molecules) and to the possibility of modulating such interactions by means of external stimuli. The main issues addressed throughout the thesis are: (i) the analysis of the factors that can affect the architecture and perturb the stability of supramolecular systems; (ii) the possibility of controlling the direction of supramolecular motions exploiting the molecular information content; (iii) the development of switchable supramolecular polymers starting from simple host-guest complexes; (iv) the capability of some molecular machines to process information at molecular level, thus behaving as logic devices; (v) the behaviour of molecular machine components in a biological-type environment; (vi) the study of chemically functionalized metal nanoparticles by second harmonic generation spectroscopy.

Produzione automatizzata per nastratura di componenti strutturali in materiale composito

Questa dissertazione tratterà l’argomento dello studio di metodi di progettazione e processi tecnologici innovativi per l’industrializzazione in medio-grande serie di componenti strutturali in materiale composito. L’interesse della ricerca verso questo ambito è suscitato dai notevoli vantaggi che l’utilizzo di materiali dall’alto rapporto prestazioni meccaniche/peso danno nella ricerca di elevate prestazioni in applicazioni sportive e diminuzione dei consumi ed emissioni inquinanti in mezzi di trasporto di grande serie. Lo studio di componenti in materiale composito è caratterizzato dalla peculiarità di non poter disgiungere la progettazione della geometria della parte da quella del materiale e del processo, ed in questo senso nella figura del progettista si vanno a riassumere sinergicamente competenze riguardanti i tre ambiti. Lo scopo di questo lavoro è la proposizione di una metodologia di progettazione e produzione di componenti strutturali che permetta l’utilizzazione ottimale della natura fibrosa del materiale composito sia dal punto di vista del trasferimento dei carichi tra diversi componenti, sia dal punto di vista del processo di laminazione che avviene per nastratura automatizzata. Lo studio è volto a mostrare in quali termini tale tecnologia sia potenzialmente in grado di superare i vincoli di forma ed i limiti di efficienza meccanica delle giunzioni tra le parti e di garantire maggiore produttività e costi inferiori rispetti ai diversi metodi di produzione che rappresentano oggi lo stato dell’arte dell’industrializzazione in medio-grande serie. Particolare attenzione verrà posta sull’utilizzo della tecnologia oggetto di studio per la produzione di telai automobilistici.

Semantic Service Architectures for Smart Environments

Many industries and academic institutions share the vision that an appropriate use of information originated from the environment may add value to services in multiple domains and may help humans in dealing with the growing information overload which often seems to jeopardize our life. It is also clear that information sharing and mutual understanding between software agents may impact complex processes where many actors (humans and machines) are involved, leading to relevant socioeconomic benefits. Starting from these two input, architectural and technological solutions to enable “environment-related cooperative digital services” are here explored. The proposed analysis starts from the consideration that our environment is physical space and here diversity is a major value. On the other side diversity is detrimental to common technological solutions, and it is an obstacle to mutual understanding. An appropriate environment abstraction and a shared information model are needed to provide the required levels of interoperability in our heterogeneous habitat. This thesis reviews several approaches to support environment related applications and intends to demonstrate that smart-space-based, ontology-driven, information-sharing platforms may become a flexible and powerful solution to support interoperable services in virtually any domain and even in cross-domain scenarios. It also shows that semantic technologies can be fruitfully applied not only to represent application domain knowledge. For example semantic modeling of Human-Computer Interaction may support interaction interoperability and transformation of interaction primitives into actions, and the thesis shows how smart-space-based platforms driven by an interaction ontology may enable natural ad flexible ways of accessing resources and services, e.g, with gestures. An ontology for computational flow execution has also been built to represent abstract computation, with the goal of exploring new ways of scheduling computation flows with smart-space-based semantic platforms.

Automatic Deployment of Applications in the Cloud

In distributed systems like clouds or service oriented frameworks, applications are typically assembled by deploying and connecting a large number of heterogeneous software components, spanning from fine-grained packages to coarse-grained complex services. The complexity of such systems requires a rich set of techniques and tools to support the automation of their deployment process. By relying on a formal model of components, a technique is devised for computing the sequence of actions allowing the deployment of a desired configuration. An efficient algorithm, working in polynomial time, is described and proven to be sound and complete. Finally, a prototype tool implementing the proposed algorithm has been developed. Experimental results support the adoption of this novel approach in real life scenarios.

Modelli e strumenti di supporto alla scelta informata del paziente: un argine alla medicina difensiva

L’aumento esponenziale del contenzioso medico-legale – originatosi negli USA negli anni Sessanta in proporzioni tali da far parlare di medical liability crisis, e sviluppatosi in Italia a partire dalla metà degli anni Ottanta – ha comportato e continua a comportare, unitamente ad altre conseguenze negative, il ricorso sempre più frequente dei sanitari alle pratiche di medicina difensiva, con elevatissimi costi a carico del Servizio Sanitario Nazionale dovuti alla sovrabbondanza di trattamenti e ricoveri inutili e di procedure diagnostiche invasive non necessarie, peraltro produttive di stress emotivo nei pazienti. La causa dell’aumento della litigiosità deve essere ricercata in buona parte nella relazione medico-paziente, in particolar modo con riferimento al momento informativo che precede l’acquisizione del consenso informato al trattamento clinico. In Italia, i limiti che per lo più caratterizzano gli studi riguardanti il consenso informato derivano principalmente dal fatto che essi tendono a focalizzarsi unicamente sulla componente scritta del medesimo. Il fulcro del consenso informato, invece, deve ritenersi rappresentato da una comunicazione tra sanitario e paziente relativa ad un trattamento proposto ed alle possibili alternative, alla non sottoposizione ad alcun trattamento e ai rischi e benefici di ciascuna di queste opzioni. In un tale contesto il tema della comunicazione tra il professionista e la persona assistita sta suscitando interesse poiché ci si aspetta che esso conduca a miglioramenti degli outcome dei pazienti e alla diminuzione delle denunce da parte di questi ultimi per casi di responsabilità sanitaria. La maggiore attenzione al rapporto medico - paziente ha fatto emergere il bisogno di migliorare e potenziare le abilità comunicative dei medici, in un’ottica in cui il momento comunicativo possa essere percepito dal professionista come fulcro del rapporto medico-paziente, nella prospettiva di una elaborazione di strategie di prevenzione e contrasto ai fenomeni di medicina difensiva.