Physical model of PD behavior and relevant damage growth from micro-cavities in polyethylene-based material under AC voltage

In the framework of developing defect-based life models, in which breakdown is explicitly associated with partial discharge (PD)-induced damage growth from a defect, ageing tests and PD measurements were carried out in the lab on polyethylene (PE) layered specimens containing artificial cavities. PD activity was monitored continuously during aging. A quasi-deterministic series of stages can be observed in the behavior of the main PD parameters (i.e. discharge repetition rate and amplitude). Phase-resolved PD patterns at various ageing stages were reproduced by numerical simulation which is based on a physical discharge model devoid of adaptive parameters. The evolution of the simulation parameters provides insight into the physical-chemical changes taking place at the dielectric/cavity interface during the aging process. PD activity shows similar time behavior under constant cavity gas volume and constant cavity gas pressure conditions, suggesting that the variation of PD parameters may not be attributed to the variation of the gas pressure. Brownish PD byproducts, consisting of oxygen containing moieties, and degradation pits were found at the dielectric/cavity interface. It is speculated that the change of PD activity is related to the composition of the cavity gas, as well as to the properties of dielectric/cavity interface.

User interaction widgets for interactive theorem proving

Matita (that means pencil in Italian) is a new interactive theorem prover under development at the University of Bologna. When compared with state-of-the-art proof assistants, Matita presents both traditional and innovative aspects. The underlying calculus of the system, namely the Calculus of (Co)Inductive Constructions (CIC for short), is well-known and is used as the basis of another mainstream proof assistant—Coq—with which Matita is to some extent compatible. In the same spirit of several other systems, proof authoring is conducted by the user as a goal directed proof search, using a script for storing textual commands for the system. In the tradition of LCF, the proof language of Matita is procedural and relies on tactic and tacticals to proceed toward proof completion. The interaction paradigm offered to the user is based on the script management technique at the basis of the popularity of the Proof General generic interface for interactive theorem provers: while editing a script the user can move forth the execution point to deliver commands to the system, or back to retract (or “undo”) past commands. Matita has been developed from scratch in the past 8 years by several members of the Helm research group, this thesis author is one of such members. Matita is now a full-fledged proof assistant with a library of about 1.000 concepts. Several innovative solutions spun-off from this development effort. This thesis is about the design and implementation of some of those solutions, in particular those relevant for the topic of user interaction with theorem provers, and of which this thesis author was a major contributor. Joint work with other members of the research group is pointed out where needed. The main topics discussed in this thesis are briefly summarized below. Disambiguation. Most activities connected with interactive proving require the user to input mathematical formulae. Being mathematical notation ambiguous, parsing formulae typeset as mathematicians like to write down on paper is a challenging task; a challenge neglected by several theorem provers which usually prefer to fix an unambiguous input syntax. Exploiting features of the underlying calculus, Matita offers an efficient disambiguation engine which permit to type formulae in the familiar mathematical notation. Step-by-step tacticals. Tacticals are higher-order constructs used in proof scripts to combine tactics together. With tacticals scripts can be made shorter, readable, and more resilient to changes. Unfortunately they are de facto incompatible with state-of-the-art user interfaces based on script management. Such interfaces indeed do not permit to position the execution point inside complex tacticals, thus introducing a trade-off between the usefulness of structuring scripts and a tedious big step execution behavior during script replaying. In Matita we break this trade-off with tinycals: an alternative to a subset of LCF tacticals which can be evaluated in a more fine-grained manner. Extensible yet meaningful notation. Proof assistant users often face the need of creating new mathematical notation in order to ease the use of new concepts. The framework used in Matita for dealing with extensible notation both accounts for high quality bidimensional rendering of formulae (with the expressivity of MathMLPresentation) and provides meaningful notation, where presentational fragments are kept synchronized with semantic representation of terms. Using our approach interoperability with other systems can be achieved at the content level, and direct manipulation of formulae acting on their rendered forms is possible too. Publish/subscribe hints. Automation plays an important role in interactive proving as users like to delegate tedious proving sub-tasks to decision procedures or external reasoners. Exploiting the Web-friendliness of Matita we experimented with a broker and a network of web services (called tutors) which can try independently to complete open sub-goals of a proof, currently being authored in Matita. The user receives hints from the tutors on how to complete sub-goals and can interactively or automatically apply them to the current proof. Another innovative aspect of Matita, only marginally touched by this thesis, is the embedded content-based search engine Whelp which is exploited to various ends, from automatic theorem proving to avoiding duplicate work for the user. We also discuss the (potential) reusability in other systems of the widgets presented in this thesis and how we envisage the evolution of user interfaces for interactive theorem provers in the Web 2.0 era.

Semantic-based middleware solutions to support context-aware service provisioning in pervasive environments

The dynamicity and heterogeneity that characterize pervasive environments raise new challenges in the design of mobile middleware. Pervasive environments are characterized by a significant degree of heterogeneity, variability, and dynamicity that conventional middleware solutions are not able to adequately manage. Originally designed for use in a relatively static context, such middleware systems tend to hide low-level details to provide applications with a transparent view on the underlying execution platform. In mobile environments, however, the context is extremely dynamic and cannot be managed by a priori assumptions. Novel middleware should therefore support mobile computing applications in the task of adapting their behavior to frequent changes in the execution context, that is, it should become context-aware. In particular, this thesis has identified the following key requirements for novel context-aware middleware that existing solutions do not fulfil yet. (i) Middleware solutions should support interoperability between possibly unknown entities by providing expressive representation models that allow to describe interacting entities, their operating conditions and the surrounding world, i.e., their context, according to an unambiguous semantics. (ii) Middleware solutions should support distributed applications in the task of reconfiguring and adapting their behavior/results to ongoing context changes. (iii) Context-aware middleware support should be deployed on heterogeneous devices under variable operating conditions, such as different user needs, application requirements, available connectivity and device computational capabilities, as well as changing environmental conditions. Our main claim is that the adoption of semantic metadata to represent context information and context-dependent adaptation strategies allows to build context-aware middleware suitable for all dynamically available portable devices. Semantic metadata provide powerful knowledge representation means to model even complex context information, and allow to perform automated reasoning to infer additional and/or more complex knowledge from available context data. In addition, we suggest that, by adopting proper configuration and deployment strategies, semantic support features can be provided to differentiated users and devices according to their specific needs and current context. This thesis has investigated novel design guidelines and implementation options for semantic-based context-aware middleware solutions targeted to pervasive environments. These guidelines have been applied to different application areas within pervasive computing that would particularly benefit from the exploitation of context. Common to all applications is the key role of context in enabling mobile users to personalize applications based on their needs and current situation. The main contributions of this thesis are (i) the definition of a metadata model to represent and reason about context, (ii) the definition of a model for the design and development of context-aware middleware based on semantic metadata, (iii) the design of three novel middleware architectures and the development of a prototypal implementation for each of these architectures, and (iv) the proposal of a viable approach to portability issues raised by the adoption of semantic support services in pervasive applications.

Rag2-/-;gammac-/- immunodeficient mice, a new preclinical model to study antitumor approaches

Animal models have been relevant to study the molecular mechanisms of cancer and to develop new antitumor agents. Anyway, the huge divergence in mouse and human evolution made difficult the translation of the gained achievements in preclinical mouse based studies. The generation of clinically relevant murine models requires their humanization both concerning the creation of transgenic models and the generation of humanized mice in which to engraft a functional human immune system, and reproduce the physiological effects and molecular mechanisms of growth and metastasization of human tumors. In particular, the availability of genotypically stable immunodepressed mice able to accept tumor injection and allow human tumor growth and metastasization would be important to develop anti-tumor and anti-metastatic strategies. Recently, Rag2-/-;gammac-/- mice, double knockout for genes involved in lymphocyte differentiation, had been developed (CIEA, Central Institute for Experimental Animals, Kawasaki, Japan). Studies of human sarcoma metastasization in Rag2-/-; gammac-/- mice (lacking B, T and NK functionality) revealed their high metastatic efficiency and allowed the expression of human metastatic phenotypes not detectable in the conventionally used nude murine model. In vitro analysis to investigate the molecular mechanisms involved in the specific pattern of human sarcomas metastasization revealed the importance of liver-produced growth and motility factors, in particular the insulin-like growth factors (IGFs). The involvement of this growth factor was then demonstrated in vivo through inhibition of IGF signalling pathway. Due to the high growth and metastatic propensity of tumor cells, Rag2-/-;gammac-/- mice were used as model to investigate the metastatic behavior of rhabdomyosarcoma cells engineered to improve the differentiation. It has been recently shown that this immunodeficient model can be reconstituted with a human immune system through the injection of human cord blood progenitor cells. The work illustrated in this thesis revealed that the injection of different human progenitor cells (CD34+ or CD133+) showed peculiar engraftment and differentiation abilities. Experiments of cell vaccination were performed to investigate the functionality of the engrafted human immune system and the induction of specific human immune responses. Results from such experiments will allow to collect informations about human immune responses activated during cell vaccination and to define the best reconstitution and experimental conditions to create a humanized model in which to study, in a preclinical setting, immunological antitumor strategies.

Crashworthiness and composite materials: development of an experimental test method for the energy absorption determination and implementation of the relative numerical model

In this PhD thesis the crashworthiness topic is studied with the perspective of the development of a small-scale experimental test able to characterize a material in terms of energy absorption. The material properties obtained are then used to validate a nu- merical model of the experimental test itself. Consequently, the numerical model, calibrated on the specific ma- terial, can be extended to more complex structures and used to simulate their energy absorption behavior. The experimental activity started at University of Washington in Seattle, WA (USA) and continued at Second Faculty of Engi- neering, University of Bologna, Forl`ı (Italy), where the numerical model for the simulation of the experimental test was implemented and optimized.