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.

Physiology and Biotechnology of the Hydrogen Production with the Green Microalga Chlamydomonas reinhardtii

The hydrogen production in the green microalga Chlamydomonas reinhardtii was evaluated by means of a detailed physiological and biotechnological study. First, a wide screening of the hydrogen productivity was done on 22 strains of C. reinhardtii, most of which mutated at the level of the D1 protein. The screening revealed for the first time that mutations upon the D1 protein may result on an increased hydrogen production. Indeed, productions ranged between 0 and more than 500 mL hydrogen per liter of culture (Torzillo, Scoma et al., 2007a), the highest producer (L159I-N230Y) being up to 5 times more performant than the strain cc124 widely adopted in literature (Torzillo, Scoma, et al., 2007b). Improved productivities by D1 protein mutants were generally a result of high photosynthetic capabilities counteracted by high respiration rates. Optimization of culture conditions were addressed according to the results of the physiological study of selected strains. In a first step, the photobioreactor (PBR) was provided with a multiple-impeller stirring system designed, developed and tested by us, using the strain cc124. It was found that the impeller system was effectively able to induce regular and turbulent mixing, which led to improved photosynthetic yields by means of light/dark cycles. Moreover, improved mixing regime sustained higher respiration rates, compared to what obtained with the commonly used stir bar mixing system. As far as the results of the initial screening phase are considered, both these factors are relevant to the hydrogen production. Indeed, very high energy conversion efficiencies (light to hydrogen) were obtained with the impeller device, prooving that our PBR was a good tool to both improve and study photosynthetic processes (Giannelli, Scoma et al., 2009). In the second part of the optimization, an accurate analysis of all the positive features of the high performance strain L159I-N230Y pointed out, respect to the WT, it has: (1) a larger chlorophyll optical cross-section; (2) a higher electron transfer rate by PSII; (3) a higher respiration rate; (4) a higher efficiency of utilization of the hydrogenase; (5) a higher starch synthesis capability; (6) a higher per cell D1 protein amount; (7) a higher zeaxanthin synthesis capability (Torzillo, Scoma et al., 2009). These information were gathered with those obtained with the impeller mixing device to find out the best culture conditions to optimize productivity with strain L159I-N230Y. The main aim was to sustain as long as possible the direct PSII contribution, which leads to hydrogen production without net CO2 release. Finally, an outstanding maximum rate of 11.1 ± 1.0 mL/L/h was reached and maintained for 21.8 ± 7.7 hours, when the effective photochemical efficiency of PSII (ΔF/F'm) underwent a last drop to zero. If expressed in terms of chl (24.0 ± 2.2 µmoles/mg chl/h), these rates of production are 4 times higher than what reported in literature to date (Scoma et al., 2010a submitted). DCMU addition experiments confirmed the key role played by PSII in sustaining such rates. On the other hand, experiments carried out in similar conditions with the control strain cc124 showed an improved final productivity, but no constant PSII direct contribution. These results showed that, aside from fermentation processes, if proper conditions are supplied to selected strains, hydrogen production can be substantially enhanced by means of biophotolysis. A last study on the physiology of the process was carried out with the mutant IL. Although able to express and very efficiently utilize the hydrogenase enzyme, this strain was unable to produce hydrogen when sulfur deprived. However, in a specific set of experiments this goal was finally reached, pointing out that other than (1) a state 1-2 transition of the photosynthetic apparatus, (2) starch storage and (3) anaerobiosis establishment, a timely transition to the hydrogen production is also needed in sulfur deprivation to induce the process before energy reserves are driven towards other processes necessary for the survival of the cell. This information turned out to be crucial when moving outdoor for the hydrogen production in a tubular horizontal 50-liter PBR under sunlight radiation. First attempts with laboratory grown cultures showed that no hydrogen production under sulfur starvation can be induced if a previous adaptation of the culture is not pursued outdoor. Indeed, in these conditions the hydrogen production under direct sunlight radiation with C. reinhardtii was finally achieved for the first time in literature (Scoma et al., 2010b submitted). Experiments were also made to optimize productivity in outdoor conditions, with respect to the light dilution within the culture layers. Finally, a brief study of the anaerobic metabolism of C. reinhardtii during hydrogen oxidation has been carried out. This study represents a good integration to the understanding of the complex interplay of pathways that operate concomitantly in this microalga.

Use of Biotechnology to increase the content of bioactive compounds in fermented foods of plant origin

The objectives of this PhD research were: i) to evaluate the use of bread making process to increase the content of β-glucans, resistant starch, fructans, dietary fibers and phenolic compounds of kamut khorasan and wheat breads made with flours obtained from kernels at different maturation stage (at milky stage and fully ripe) and ii) to study the impact of whole grains consumption in the human gut. The fermentation and the stages of kernel development or maturation had a great impact on the amount of resistant starch, fructans and β-glucans as well as their interactions resulted highly statistically significant. The amount of fructans was high in kamut bread (2.1g/100g) at the fully ripe stage compared to wheat during industrial fermentation (baker’s yeast). The sourdough increases the content of polyphenols more than industrial fermentation especially in bread made by flour at milky stage. From the analysis of volatile compounds it resulted that the sensors of electronic nose perceived more aromatic compound in kamut products, as well as the SPME-GC-MS, thus we can assume that kamut is more aromatic than wheat, so using it in sourdough process can be a successful approach to improve the bread taste and flavor. The determination of whole grain biormakers such as alkylresorcinols and others using FIE-MS AND GC-tof-MS is a valuable alternative for further metabolic investigations. The decrease of N-acetyl-glucosamine and 3-methyl-hexanedioic acid in kamut faecal samples suggests that kamut can have a role in modulating mucus production/degradation or even gut inflammation. This work gives a new approach to the innovation strategies in bakery functional foods, that can help to choose the right or best combination between stages of kernel maturation-fermentation process and baking temperature.

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.