Automatic code generation: from process algebraic architectural descriptions to multithreaded java programs

Process algebraic architectural description languages provide a formal means for modeling software systems and assessing their properties. In order to bridge the gap between system modeling and system im- plementation, in this thesis an approach is proposed for automatically generating multithreaded object-oriented code from process algebraic architectural descriptions, in a way that preserves – under certain assumptions – the properties proved at the architectural level. The approach is divided into three phases, which are illustrated by means of a running example based on an audio processing system. First, we develop an architecture-driven technique for thread coordination management, which is completely automated through a suitable package. Second, we address the translation of the algebraically-specified behavior of the individual software units into thread templates, which will have to be filled in by the software developer according to certain guidelines. Third, we discuss performance issues related to the suitability of synthesizing monitors rather than threads from software unit descriptions that satisfy specific constraints. In addition to the running example, we present two case studies about a video animation repainting system and the implementation of a leader election algorithm, in order to summarize the whole approach. The outcome of this thesis is the implementation of the proposed approach in a translator called PADL2Java and its integration in the architecture-centric verification tool TwoTowers.

Modeling hydrothermal system: deriving observables and hydrothermal instability in volcanic and non-volcanic setting

Hydrothermal fluids are a fundamental resource for understanding and monitoring volcanic and non-volcanic systems. This thesis is focused on the study of hydrothermal system through numerical modeling with the geothermal simulator TOUGH2. Several simulations are presented, and geophysical and geochemical observables, arising from fluids circulation, are analyzed in detail throughout the thesis. In a volcanic setting, fluids feeding fumaroles and hot spring may play a key role in the hazard evaluation. The evolution of the fluids circulation is caused by a strong interaction between magmatic and hydrothermal systems. A simultaneous analysis of different geophysical and geochemical observables is a sound approach for interpreting monitored data and to infer a consistent conceptual model. Analyzed observables are ground displacement, gravity changes, electrical conductivity, amount, composition and temperature of the emitted gases at surface, and extent of degassing area. Results highlight the different temporal response of the considered observables, as well as the different radial pattern of variation. However, magnitude, temporal response and radial pattern of these signals depend not only on the evolution of fluid circulation, but a main role is played by the considered rock properties. Numerical simulations highlight differences that arise from the assumption of different permeabilities, for both homogeneous and heterogeneous systems. Rock properties affect hydrothermal fluid circulation, controlling both the range of variation and the temporal evolution of the observable signals. Low temperature fumaroles and low discharge rate may be affected by atmospheric conditions. Detailed parametric simulations were performed, aimed to understand the effects of system properties, such as permeability and gas reservoir overpressure, on diffuse degassing when air temperature and barometric pressure changes are applied to the ground surface. Hydrothermal circulation, however, is not only a characteristic of volcanic system. Hot fluids may be involved in several mankind problems, such as studies on geothermal engineering, nuclear waste propagation in porous medium, and Geological Carbon Sequestration (GCS). The current concept for large-scale GCS is the direct injection of supercritical carbon dioxide into deep geological formations which typically contain brine. Upward displacement of such brine from deep reservoirs driven by pressure increases resulting from carbon dioxide injection may occur through abandoned wells, permeable faults or permeable channels. Brine intrusion into aquifers may degrade groundwater resources. Numerical results show that pressure rise drives dense water up to the conduits, and does not necessarily result in continuous flow. Rather, overpressure leads to new hydrostatic equilibrium if fluids are initially density stratified. If warm and salty fluid does not cool passing through the conduit, an oscillatory solution is then possible. Parameter studies delineate steady-state (static) and oscillatory solutions.

Kinematics of the Sicily and Calabria Subduction System from Elastic Block Modeling of GPS Data

We use data from about 700 GPS stations in the EuroMediterranen region to investigate the present-day behavior of the the Calabrian subduction zone within the Mediterranean-scale plates kinematics and to perform local scale studies about the strain accumulation on active structures. We focus attenction on the Messina Straits and Crati Valley faults where GPS data show extentional velocity gradients of ∼3 mm/yr and ∼2 mm/yr, respectively. We use dislocation model and a non-linear constrained optimization algorithm to invert for fault geometric parameters and slip-rates and evaluate the associated uncertainties adopting a bootstrap approach. Our analysis suggest the presence of two partially locked normal faults. To investigate the impact of elastic strain contributes from other nearby active faults onto the observed velocity gradient we use a block modeling approach. Our models show that the inferred slip-rates on the two analyzed structures are strongly impacted by the assumed locking width of the Calabrian subduction thrust. In order to frame the observed local deformation features within the present- day central Mediterranean kinematics we realyze a statistical analysis testing the indipendent motion (w.r.t. the African and Eurasias plates) of the Adriatic, Cal- abrian and Sicilian blocks. Our preferred model confirms a microplate like behaviour for all the investigated blocks. Within these kinematic boundary conditions we fur- ther investigate the Calabrian Slab interface geometry using a combined approach of block modeling and χ2ν statistic. Almost no information is obtained using only the horizontal GPS velocities that prove to be a not sufficient dataset for a multi-parametric inversion approach. Trying to stronger constrain the slab geometry we estimate the predicted vertical velocities performing suites of forward models of elastic dislocations varying the fault locking depth. Comparison with the observed field suggest a maximum resolved locking depth of 25 km.

Numerical optimization,modeling and system evaluation of a thermophotovoltaic hybrid panel

Photovoltaic (PV) solar panels generally produce electricity in the 6% to 16% efficiency range, the rest being dissipated in thermal losses. To recover this amount, hybrid photovoltaic thermal systems (PVT) have been devised. These are devices that simultaneously convert solar energy into electricity and heat. It is thus interesting to study the PVT system globally from different point of views in order to evaluate advantages and disadvantages of this technology and its possible uses. In particular in Chapter II, the development of the PVT absorber numerical optimization by a genetic algorithm has been carried out analyzing different internal channel profiles in order to find a right compromise between performance and technical and economical feasibility. Therefore in Chapter III ,thanks to a mobile structure built into the university lab, it has been compared experimentally electrical and thermal output power from PVT panels with separated photovoltaic and solar thermal productions. Collecting a lot of experimental data based on different seasonal conditions (ambient temperature,irradiation, wind...),the aim of this mobile structure has been to evaluate average both thermal and electrical increasing and decreasing efficiency values obtained respect to separate productions through the year. In Chapter IV , new PVT and solar thermal equation based models in steady state conditions have been developed by software Dymola that uses Modelica language. This permits ,in a simplified way respect to previous system modelling softwares, to model and evaluate different concepts about PVT panel regarding its structure before prototyping and measuring it. Chapter V concerns instead the definition of PVT boundary conditions into a HVAC system . This was made trough year simulations by software Polysun in order to finally assess the best solar assisted integrated structure thanks to F_save(solar saving energy)factor. Finally, Chapter VI presents the conclusion and the perspectives of this PhD work.

From Radio Channel Modeling to a System Level Perspective in Body-Centric Communications

Body-centric communications are emerging as a new paradigm in the panorama of personal communications. Being concerned with human behaviour, they are suitable for a wide variety of applications. The advances in the miniaturization of portable devices to be placed on or around the body, foster the diffusion of these systems, where the human body is the key element defining communication characteristics. This thesis investigates the human impact on body-centric communications under its distinctive aspects. First of all, the unique propagation environment defined by the body is described through a scenario-based channel modeling approach, according to the communication scenario considered, i.e., on- or on- to off-body. The novelty introduced pertains to the description of radio channel features accounting for multiple sources of variability at the same time. Secondly, the importance of a proper channel characterisation is shown integrating the on-body channel model in a system level simulator, allowing a more realistic comparison of different Physical and Medium Access Control layer solutions. Finally, the structure of a comprehensive simulation framework for system performance evaluation is proposed. It aims at merging in one tool, mobility and social features typical of the human being, together with the propagation aspects, in a scenario where multiple users interact sharing space and resources.

Motor control system in Parkinson’s disease: a modeling approach

Parkinson’s disease is a neurodegenerative disorder due to the death of the dopaminergic neurons of the substantia nigra of the basal ganglia. The process that leads to these neural alterations is still unknown. Parkinson’s disease affects most of all the motor sphere, with a wide array of impairment such as bradykinesia, akinesia, tremor, postural instability and singular phenomena such as freezing of gait. Moreover, in the last few years the fact that the degeneration in the basal ganglia circuitry induces not only motor but also cognitive alterations, not necessarily implicating dementia, and that dopamine loss induces also further implications due to dopamine-driven synaptic plasticity got more attention. At the present moment, no neuroprotective treatment is available, and even if dopamine-replacement therapies as well as electrical deep brain stimulation are able to improve the life conditions of the patients, they often present side effects on the long term, and cannot recover the neural loss, which instead continues to advance. In the present thesis both motor and cognitive aspects of Parkinson’s disease and basal ganglia circuitry were investigated, at first focusing on Parkinson’s disease sensory and balance issues by means of a new instrumented method based on inertial sensor to provide further information about postural control and postural strategies used to attain balance, then applying this newly developed approach to assess balance control in mild and severe patients, both ON and OFF levodopa replacement. Given the inability of levodopa to recover balance issues and the new physiological findings than underline the importance in Parkinson’s disease of non-dopaminergic neurotransmitters, it was therefore developed an original computational model focusing on acetylcholine, the most promising neurotransmitter according to physiology, and its role in synaptic plasticity. The rationale of this thesis is that a multidisciplinary approach could gain insight into Parkinson’s disease features still unresolved.

Molecular interactions: metal ions and protein chaperones in the urease system from Helicobacter pylori

Although nickel is a toxic metal for living organisms in its soluble form, its importance in many biological processes recently emerged. In this view, the investigation of the nickel-dependent enzymes urease and [NiFe]-hydrogenase, especially the mechanism of nickel insertion into their active sites, represent two intriguing case studies to understand other analogous systems and therefore to lead to a comprehension of the nickel trafficking inside the cell. Moreover, these two enzymes have been demonstrated to ensure survival and colonization of the human pathogen H. pylori, the only known microorganism able to proliferate in the gastric niche. The right nickel delivering into the urease active site requires the presence of at least four accessory proteins, UreD, UreE, UreF and UreG. Similarly, analogous process is principally mediated by HypA and HypB proteins in the [NiFe]-hydrogenase system. Indeed, HpHypA and HpHypB also have been proposed to act in the activation of the urease enzyme from H. pylori, probably mobilizing nickel ions from HpHypA to the HpUreE-HpUreG complex. A complete comprehension of the interaction mechanism between the accessory proteins and the crosstalk between urease and hydrogenase accessory systems requires the determination of the role of each protein chaperone that strictly depends on their structural and biochemical properties. The availability of HpUreE, HpUreG and HpHypA proteins in a pure form is a pre-requisite to perform all the subsequent protein characterizations, thus their purification was the first aim of this work. Subsequently, the structural and biochemical properties of HpUreE were investigated using multi-angle and quasi-elastic light scattering, as well as NMR and circular dichroism spectroscopy. The thermodynamic parameters of Ni2+ and Zn2+ binding to HpUreE were principally established using isothermal titration calorimetry and the importance of key histidine residues in the process of binding metal ions was studied using site-directed mutagenesis. The molecular details of the HpUreE-HpUreG and HpUreE-HpHypA protein-protein assemblies were also elucidated. The interaction between HpUreE and HpUreG was investigated using ITC and NMR spectroscopy, and the influence of Ni2+ and Zn2+ metal ions on the stabilization of this association was established using native gel electrophoresis, light scattering and thermal denaturation scanning followed by CD spectroscopy. Preliminary HpUreE-HpHypA interaction studies were conducted using ITC. Finally, the possible structural architectures of the two protein-protein assemblies were rationalized using homology modeling and docking computational approaches. All the obtained data were interpreted in order to achieve a more exhaustive picture of the urease activation process, and the correlation with the accessory system of the hydrogenase enzyme, considering the specific role and activity of the involved protein players. A possible function for Zn2+ in the chaperone network involved in Ni2+ trafficking and urease activation is also envisaged.

Modeling, design and experimental characterization of Micro-Electro-Mechanical-Systems for gas chromatographic applications

Design parameters, process flows, electro-thermal-fluidic simulations and experimental characterizations of Micro-Electro-Mechanical-Systems (MEMS) suited for gas-chromatographic (GC) applications are presented and thoroughly described in this thesis, whose topic belongs to the research activities the Institute for Microelectronics and Microsystems (IMM)-Bologna is involved since several years, i.e. the development of micro-systems for chemical analysis, based on silicon micro-machining techniques and able to perform analysis of complex gaseous mixtures, especially in the field of environmental monitoring. In this regard, attention has been focused on the development of micro-fabricated devices to be employed in a portable mini-GC system for the analysis of aromatic Volatile Organic Compounds (VOC) like Benzene, Toluene, Ethyl-benzene and Xylene (BTEX), i.e. chemical compounds which can significantly affect environment and human health because of their demonstrated carcinogenicity (benzene) or toxicity (toluene, xylene) even at parts per billion (ppb) concentrations. The most significant results achieved through the laboratory functional characterization of the mini-GC system have been reported, together with in-field analysis results carried out in a station of the Bologna air monitoring network and compared with those provided by a commercial GC system. The development of more advanced prototypes of micro-fabricated devices specifically suited for FAST-GC have been also presented (silicon capillary columns, Ultra-Low-Power (ULP) Metal OXide (MOX) sensor, Thermal Conductivity Detector (TCD)), together with the technological processes for their fabrication. The experimentally demonstrated very high sensitivity of ULP-MOX sensors to VOCs, coupled with the extremely low power consumption, makes the developed ULP-MOX sensor the most performing metal oxide sensor reported up to now in literature, while preliminary test results proved that the developed silicon capillary columns are capable of performances comparable to those of the best fused silica capillary columns. Finally, the development and the validation of a coupled electro-thermal Finite Element Model suited for both steady-state and transient analysis of the micro-devices has been described, and subsequently implemented with a fluidic part to investigate devices behaviour in presence of a gas flowing with certain volumetric flow rates.

InSAR deformation measurements of the earthquake cycle in transcurrent tectonic domains, analytical and analog modeling

I applied the SBAS-DInSAR method to the Mattinata Fault (MF) (Southern Italy) and to the Doruneh Fault System (DFS) (Central Iran). In the first case, I observed limited internal deformation and determined the right lateral kinematic pattern with a compressional pattern in the northern sector of the fault. Using the Okada model I inverted the observed velocities defining a right lateral strike slip solution for the MF. Even if it fits the data within the uncertainties, the modeled slip rate of 13-15 mm yr-1 seems too high with respect to the geological record. Concerning the Western termination of DFS, SAR data confirms the main left lateral transcurrent kinematics of this fault segment, but reveal a compressional component. My analytical model fits successfully the observed data and quantifies the slip in ~4 mm yr-1 and ~2.5 mm yr-1 of pure horizontal and vertical displacement respectively. The horizontal velocity is compatible with geological record. I applied classic SAR interferometry to the October–December 2008 Balochistan (Central Pakistan) seismic swarm; I discerned the different contributions of the three Mw > 5.7 earthquakes determining fault positions, lengths, widths, depths and slip distributions, constraining the other source parameters using different Global CMT solutions. A well constrained solution has been obtained for the 09/12/2008 aftershock, whereas I tested two possible fault solutions for the 28-29/10/08 mainshocks. It is not possible to favor one of the solutions without independent constraints derived from geological data. Finally I approached the study of the earthquake-cycle in transcurrent tectonic domains using analog modeling, with alimentary gelatins like crust analog material. I successfully joined the study of finite deformation with the earthquake cycle study and sudden dislocation. A lot of seismic cycles were reproduced in which a characteristic earthquake is recognizable in terms of displacement, coseismic velocity and recurrence time.

Computational Modeling of Cardiac Excitation-Contraction Coupling in Physiological and Pathological Conditions

The cardiomyocyte is a complex biological system where many mechanisms interact non-linearly to regulate the coupling between electrical excitation and mechanical contraction. For this reason, the development of mathematical models is fundamental in the field of cardiac electrophysiology, where the use of computational tools has become complementary to the classical experimentation. My doctoral research has been focusing on the development of such models for investigating the regulation of ventricular excitation-contraction coupling at the single cell level. In particular, the following researches are presented in this thesis: 1) Study of the unexpected deleterious effect of a Na channel blocker on a long QT syndrome type 3 patient. Experimental results were used to tune a Na current model that recapitulates the effect of the mutation and the treatment, in order to investigate how these influence the human action potential. Our research suggested that the analysis of the clinical phenotype is not sufficient for recommending drugs to patients carrying mutations with undefined electrophysiological properties. 2) Development of a model of L-type Ca channel inactivation in rabbit myocytes to faithfully reproduce the relative roles of voltage- and Ca-dependent inactivation. The model was applied to the analysis of Ca current inactivation kinetics during normal and abnormal repolarization, and predicts arrhythmogenic activity when inhibiting Ca-dependent inactivation, which is the predominant mechanism in physiological conditions. 3) Analysis of the arrhythmogenic consequences of the crosstalk between β-adrenergic and Ca-calmodulin dependent protein kinase signaling pathways. The descriptions of the two regulatory mechanisms, both enhanced in heart failure, were integrated into a novel murine action potential model to investigate how they concur to the development of cardiac arrhythmias. These studies show how mathematical modeling is suitable to provide new insights into the mechanisms underlying cardiac excitation-contraction coupling and arrhythmogenesis.

Automotive diesel engine transient operation: modeling, optimization and control

Traditionally, the study of internal combustion engines operation has focused on the steady-state performance. However, the daily driving schedule of automotive engines is inherently related to unsteady conditions. There are various operating conditions experienced by (diesel) engines that can be classified as transient. Besides the variation of the engine operating point, in terms of engine speed and torque, also the warm up phase can be considered as a transient condition. Chapter 2 has to do with this thermal transient condition; more precisely the main issue is the performance of a Selective Catalytic Reduction (SCR) system during cold start and warm up phases of the engine. The proposal of the underlying work is to investigate and identify optimal exhaust line heating strategies, to provide a fast activation of the catalytic reactions on SCR. Chapters 3 and 4 focus the attention on the dynamic behavior of the engine, when considering typical driving conditions. The common approach to dynamic optimization involves the solution of a single optimal-control problem. However, this approach requires the availability of models that are valid throughout the whole engine operating range and actuator ranges. In addition, the result of the optimization is meaningful only if the model is very accurate. Chapter 3 proposes a methodology to circumvent those demanding requirements: an iteration between transient measurements to refine a purpose-built model and a dynamic optimization which is constrained to the model validity region. Moreover all numerical methods required to implement this procedure are presented. Chapter 4 proposes an approach to derive a transient feedforward control system in an automated way. It relies on optimal control theory to solve a dynamic optimization problem for fast transients. From the optimal solutions, the relevant information is extracted and stored in maps spanned by the engine speed and the torque gradient.

Modeling and simulations of nanoparticles in liquid crystalline systems

The aim of this work is to investigate, using extensive Monte Carlo computer simulations, composite materials consisting of liquid crystals doped with nanoparticles. These systems are currently of great interest as they offer the possibility of tuning the properties of liquid crystals used in displays and other devices as well as providing a way of obtaining regularly organized systems of nanoparticles exploiting the molecular organization of the liquid crystal medium. Surprisingly enough, there is however a lack of fundamental knowledge on the properties and phase behavior of these hybrid materials, making the route to their application an essentially empirical one. Here we wish to contribute to the much needed rationalization of these systems studying some basic effects induced by different nanoparticles on a liquid crystal host. We investigate in particular the effects of nanoparticle shape, size and polarity as well as of their affinity to the liquid crystal solvent on the stability of the system, monitoring phase transitions, order and molecular organizations. To do this we have proposed a coarse grained approach where nanoparticles are modelled as a suitably shaped (spherical, rod and disk like) collection of spherical Lennard-Jones beads, while the mesogens are represented with Gay-Berne particles. We find that the addition of apolar nanoparticles of different shape typically lowers the nematic–isotropic transition of a non-polar nematic, with the destabilization being greater for spherical nanoparticles. For polar mesogens we have studied the effect of solvent affinity of the nanoparticles showing that aggregation takes places for low solvation values. Interestingly, if the nanoparticles are polar the aggregates contribute to stabilizing the system, compensating the shape effect. We thus find the overall effects on stability to be a delicate balance of often contrasting contributions pointing to the relevance of simulations studies for understanding these complex systems.