Specification, execution and verification of interaction protocols: an approach based on computational logic

Interaction protocols establish how different computational entities can interact with each other. The interaction can be finalized to the exchange of data, as in 'communication protocols', or can be oriented to achieve some result, as in 'application protocols'. Moreover, with the increasing complexity of modern distributed systems, protocols are used also to control such a complexity, and to ensure that the system as a whole evolves with certain features. However, the extensive use of protocols has raised some issues, from the language for specifying them to the several verification aspects. Computational Logic provides models, languages and tools that can be effectively adopted to address such issues: its declarative nature can be exploited for a protocol specification language, while its operational counterpart can be used to reason upon such specifications. In this thesis we propose a proof-theoretic framework, called SCIFF, together with its extensions. SCIFF is based on Abductive Logic Programming, and provides a formal specification language with a clear declarative semantics (based on abduction). The operational counterpart is given by a proof procedure, that allows to reason upon the specifications and to test the conformance of given interactions w.r.t. a defined protocol. Moreover, by suitably adapting the SCIFF Framework, we propose solutions for addressing (1) the protocol properties verification (g-SCIFF Framework), and (2) the a-priori conformance verification of peers w.r.t. the given protocol (AlLoWS Framework). We introduce also an agent based architecture, the SCIFF Agent Platform, where the same protocol specification can be used to program and to ease the implementation task of the interacting peers.

Design and Performance Evaluation of Network-on-Chip Communication Protocols and Architectures

The scale down of transistor technology allows microelectronics manufacturers such as Intel and IBM to build always more sophisticated systems on a single microchip. The classical interconnection solutions based on shared buses or direct connections between the modules of the chip are becoming obsolete as they struggle to sustain the increasing tight bandwidth and latency constraints that these systems demand. The most promising solution for the future chip interconnects are the Networks on Chip (NoC). NoCs are network composed by routers and channels used to inter- connect the different components installed on the single microchip. Examples of advanced processors based on NoC interconnects are the IBM Cell processor, composed by eight CPUs that is installed on the Sony Playstation III and the Intel Teraflops pro ject composed by 80 independent (simple) microprocessors. On chip integration is becoming popular not only in the Chip Multi Processor (CMP) research area but also in the wider and more heterogeneous world of Systems on Chip (SoC). SoC comprehend all the electronic devices that surround us such as cell-phones, smart-phones, house embedded systems, automotive systems, set-top boxes etc... SoC manufacturers such as ST Microelectronics , Samsung, Philips and also Universities such as Bologna University, M.I.T., Berkeley and more are all proposing proprietary frameworks based on NoC interconnects. These frameworks help engineers in the switch of design methodology and speed up the development of new NoC-based systems on chip. In this Thesis we propose an introduction of CMP and SoC interconnection networks. Then focusing on SoC systems we propose: • a detailed analysis based on simulation of the Spidergon NoC, a ST Microelectronics solution for SoC interconnects. The Spidergon NoC differs from many classical solutions inherited from the parallel computing world. Here we propose a detailed analysis of this NoC topology and routing algorithms. Furthermore we propose aEqualized a new routing algorithm designed to optimize the use of the resources of the network while also increasing its performance; • a methodology flow based on modified publicly available tools that combined can be used to design, model and analyze any kind of System on Chip; • a detailed analysis of a ST Microelectronics-proprietary transport-level protocol that the author of this Thesis helped developing; • a simulation-based comprehensive comparison of different network interface designs proposed by the author and the researchers at AST lab, in order to integrate shared-memory and message-passing based components on a single System on Chip; • a powerful and flexible solution to address the time closure exception issue in the design of synchronous Networks on Chip. Our solution is based on relay stations repeaters and allows to reduce the power and area demands of NoC interconnects while also reducing its buffer needs; • a solution to simplify the design of the NoC by also increasing their performance and reducing their power and area consumption. We propose to replace complex and slow virtual channel-based routers with multiple and flexible small Multi Plane ones. This solution allows us to reduce the area and power dissipation of any NoC while also increasing its performance especially when the resources are reduced. This Thesis has been written in collaboration with the Advanced System Technology laboratory in Grenoble France, and the Computer Science Department at Columbia University in the city of New York.

Cross-Talk tra Bifidobacterium e intestino umano: impatto sulle attività health promoting

Bifidobacteria constitute up to 3% of the total microbiota and represent one of the most important healthpromoting bacterial groups of the human intestinal microflora. The presence of Bifidobacterium in the human gastrointestinal tract has been directly related to several health-promoting activities; however, to date, no information about the specific mechanisms of interaction with the host is available. The first health-promoting activities studied in these job was the oxalate-degrading activity. Oxalic acid occurs extensively in nature and plays diverse roles, especially in pathological processes. Due to its highly oxidizing effects, hyper absorption or abnormal synthesis of oxalate can cause serious acute disorders in mammals and be lethal in extreme cases. Intestinal oxalate-degrading bacteria could therefore be pivotal in maintaining oxalate homeostasis, reducing the risk of kidney stone development. In this study, the oxalate-degrading activity of 14 bifidobacterial strains was measured by a capillary electrophoresis technique. The oxc gene, encoding oxalyl-CoA decarboxylase, a key enzyme in oxalate catabolism, was isolated by probing a genomic library of B. animalis subsp. lactis BI07, which was one of the most active strains in the preliminary screening. The genetic and transcriptional organization of oxc flanking regions was determined, unravelling the presence of other two independently transcribed open reading frames, potentially responsible for B. animalis subsp. lactis ability to degrade oxalate. Transcriptional analysis, using real-time quantitative reverse transcription PCR, revealed that these genes were highly induced in cells first adapted to subinhibitory concentrations of oxalate and then exposed to pH 4.5. Acidic conditions were also a prerequisite for a significant oxalate degradation rate, which dramatically increased in oxalate pre-adapted cells, as demonstrated in fermentation experiments with different pH-controlled batch cultures. These findings provide new insights in the characterization of oxalate-degrading probiotic bacteria and may support the use of B. animalis subsp. lactis as a promising adjunct for the prophylaxis and management of oxalate-related kidney disease. In order to provide some insight into the molecular mechanisms involved in the interaction with the host, in the second part of the job, we investigated whether Bifidobacterium was able to capture human plasminogen on the cell surface. The binding of human plasminogen to Bifidobacterium was dependent on lysine residues of surface protein receptors. By using a proteomic approach, we identified six putative plasminogen-binding proteins in the cell wall fraction of three strain of Bifidobacterium. The data suggest that plasminogen binding to Bifidobactrium is due to the concerted action of a number of proteins located on the bacterial cell surface, some of which are highly conserved cytoplasmic proteins which have other essential cellular functions. Our findings represent a step forward in understanding the mechanisms involved in the Bifidobacterium-host interaction. In these job w studied a new approach based on to MALDI-TOF MS to measure the interaction between entire bacterial cells and host molecular target. MALDI-TOF (Matrix Assisted Laser Desorption Ionization-Time of Flight)—mass spectrometry has been applied, for the first time, in the investigation of whole Bifidobacterium cells-host target proteins interaction. In particular, by means of this technique, a dose dependent human plasminogen-binding activity has been shown for Bifidobacterium. The involvement of lysine binding sites on the bacterial cell surface has been proved. The obtained result was found to be consistent with that from well-established standard methodologies, thus the proposed MALDI-TOF approach has the potential to enter as a fast alternative method in the field of biorecognition studies involving in bacterial cells and proteins of human origin.

Study of the components of quality in SO2-free wines obtained by innovative vinification protocols. Evaluation of the pre-fermentative addition of lysozyme and oenological tannins.

The research performed during the PhD candidature was intended to evaluate the quality of white wines, as a function of the reduction in SO2 use during the first steps of the winemaking process. In order to investigate the mechanism and intensity of interactions occurring between lysozyme and the principal macro-components of musts and wines, a series of experiments on model wine solutions were undertaken, focusing attention on the polyphenols, SO2, oenological tannins, pectines, ethanol, and sugar components. In the second part of this research program, a series of conventional sulphite added vinifications were compared to vinifications in which sulphur dioxide was replaced by lysozyme and consequently define potential winemaking protocols suitable for the production of SO2-free wines. To reach the final goal, the technological performance of two selected yeast strains with a low aptitude to produce SO2 during fermentation were also evaluated. The data obtained suggested that the addition of lysozyme and oenological tannins during the alcoholic fermentation could represent a promising alternative to the use of sulphur dioxide and a reliable starting point for the production of SO2-free wines. The different vinification protocols studied influenced the composition of the volatile profile in wines at the end of the alcoholic fermentation, especially with regards to alcohols and ethyl esters also a consequence of the yeast’s response to the presence or absence of sulphites during fermentation, contributing in different ways to the sensory profiles of wines. In fact, the aminoacids analysis showed that lysozyme can affect the consumption of nitrogen as a function of the yeast strain used in fermentation. During the bottle storage, the evolution of volatile compounds is affected by the presence of SO2 and oenological tannins, confirming their positive role in scaveging oxygen and maintaining the amounts of esters over certain levels, avoiding a decline in the wine’s quality. Even though a natural decrease was found on phenolic profiles due to oxidation effects caused by the presence of oxygen dissolved in the medium during the storage period, the presence of SO2 together with tannins contrasted the decay of phenolic content at the end of the fermentation. Tannins also showed a central role in preserving the polyphenolic profile of wines during the storage period, confirming their antioxidant property, acting as reductants. Our study focused on the fundamental chemistry relevant to the oxidative phenolic spoilage of white wines has demonstrated the suitability of glutathione to inhibit the production of yellow xanthylium cation pigments generated from flavanols and glyoxylic acid at the concentration that it typically exists in wine. The ability of glutathione to bind glyoxylic acid rather than acetaldehyde may enable glutathione to be used as a ‘switch’ for glyoxylic acid-induced polymerisation mechanisms, as opposed to the equivalent acetaldehyde polymerisation, in processes such as microoxidation. Further research is required to assess the ability of glutathione to prevent xanthylium cation production during the in-situ production of glyoxylic acid and in the presence of sulphur dioxide.

Development of motion analysis protocols based on inertial sensors

The aim of this thesis was to describe the development of motion analysis protocols for applications on upper and lower limb extremities, by using inertial sensors-based systems. Inertial sensors-based systems are relatively recent. Knowledge and development of methods and algorithms for the use of such systems for clinical purposes is therefore limited if compared with stereophotogrammetry. However, their advantages in terms of low cost, portability, small size, are a valid reason to follow this direction. When developing motion analysis protocols based on inertial sensors, attention must be given to several aspects, like the accuracy of inertial sensors-based systems and their reliability. The need to develop specific algorithms/methods and software for using these systems for specific applications, is as much important as the development of motion analysis protocols based on them. For this reason, the goal of the 3-years research project described in this thesis was achieved first of all trying to correctly design the protocols based on inertial sensors, in terms of exploring and developing which features were suitable for the specific application of the protocols. The use of optoelectronic systems was necessary because they provided a gold standard and accurate measurement, which was used as a reference for the validation of the protocols based on inertial sensors. The protocols described in this thesis can be particularly helpful for rehabilitation centers in which the high cost of instrumentation or the limited working areas do not allow the use of stereophotogrammetry. Moreover, many applications requiring upper and lower limb motion analysis to be performed outside the laboratories will benefit from these protocols, for example performing gait analysis along the corridors. Out of the buildings, the condition of steady-state walking or the behavior of the prosthetic devices when encountering slopes or obstacles during walking can also be assessed. The application of inertial sensors on lower limb amputees presents conditions which are challenging for magnetometer-based systems, due to ferromagnetic material commonly adopted for the construction of idraulic components or motors. INAIL Prostheses Centre stimulated and, together with Xsens Technologies B.V. supported the development of additional methods for improving the accuracy of MTx in measuring the 3D kinematics for lower limb prostheses, with the results provided in this thesis. In the author’s opinion, this thesis and the motion analysis protocols based on inertial sensors here described, are a demonstration of how a strict collaboration between the industry, the clinical centers, the research laboratories, can improve the knowledge, exchange know-how, with the common goal to develop new application-oriented systems.

Enabling a direct path from end-user specifications to executable protocols in a biology laboratory environment

Biomedical analyses are becoming increasingly complex, with respect to both the type of the data to be produced and the procedures to be executed. This trend is expected to continue in the future. The development of information and protocol management systems that can sustain this challenge is therefore becoming an essential enabling factor for all actors in the field. The use of custom-built solutions that require the biology domain expert to acquire or procure software engineering expertise in the development of the laboratory infrastructure is not fully satisfactory because it incurs undesirable mutual knowledge dependencies between the two camps. We propose instead an infrastructure concept that enables the domain experts to express laboratory protocols using proper domain knowledge, free from the incidence and mediation of the software implementation artefacts. In the system that we propose this is made possible by basing the modelling language on an authoritative domain specific ontology and then using modern model-driven architecture technology to transform the user models in software artefacts ready for execution in a multi-agent based execution platform specialized for biomedical laboratories.

Airway Basal Cell Vascular Endothelial Growth Factor-mediated Cross-Talk Regulates Endothelial Cell Dependent Growth Support of Human Airway Basal Cells

The human airway epithelium is a pseudostratified heterogenous layer comprised of cili-ated, secretory, intermediate and basal cells. As the stem/progenitor population of the airway epi-thelium, airway basal cells differentiate into ciliated and secretory cells to replenish the airway epithelium during physiological turnover and repair. Transcriptome analysis of airway basal cells revealed high expression of vascular endothelial growth factor A (VEGFA), a gene not typically associated with the function of this cell type. Using cultures of primary human airway basal cells, we demonstrate that basal cells express all of the 3 major isoforms of VEGFA (121, 165 and 189) but lack functional expression of the classical VEGFA receptors VEGFR1 and VEGFR2. The VEGFA is actively secreted by basal cells and while it appears to have no direct autocrine function on basal cell growth and proliferation, it functions in a paracrine manner to activate MAPK signaling cascades in endothelium via VEGFR2 dependent signaling pathways. Using a cytokine- and serum-free co-culture system of primary human airway basal cells and human endothelial cells revealed that basal cell secreted VEGFA activated endothelium to ex-press mediators that, in turn, stimulate and support basal cell proliferation and growth. These data demonstrate novel VEGFA mediated cross-talk between airway basal cells and endothe-lium, the purpose of which is to modulate endothelial activation and in turn stimulate and sustain basal cell growth.

Application Platforms for the Internet of Things: Theory, Architecture, Protocols, Data Formats, and Privacy

The Internet of Things (IoT) is the next industrial revolution: we will interact naturally with real and virtual devices as a key part of our daily life. This technology shift is expected to be greater than the Web and Mobile combined. As extremely different technologies are needed to build connected devices, the Internet of Things field is a junction between electronics, telecommunications and software engineering. Internet of Things application development happens in silos, often using proprietary and closed communication protocols. There is the common belief that only if we can solve the interoperability problem we can have a real Internet of Things. After a deep analysis of the IoT protocols, we identified a set of primitives for IoT applications. We argue that each IoT protocol can be expressed in term of those primitives, thus solving the interoperability problem at the application protocol level. Moreover, the primitives are network and transport independent and make no assumption in that regard. This dissertation presents our implementation of an IoT platform: the Ponte project. Privacy issues follows the rise of the Internet of Things: it is clear that the IoT must ensure resilience to attacks, data authentication, access control and client privacy. We argue that it is not possible to solve the privacy issue without solving the interoperability problem: enforcing privacy rules implies the need to limit and filter the data delivery process. However, filtering data require knowledge of how the format and the semantics of the data: after an analysis of the possible data formats and representations for the IoT, we identify JSON-LD and the Semantic Web as the best solution for IoT applications. Then, this dissertation present our approach to increase the throughput of filtering semantic data by a factor of ten.

Cell death mechanisms triggered by monoclonal antibodies against CD99 in Ewing sarcoma: Cross-talk between MDM2, IGF-1R and Ras/MAPK

CD99 is a 32 kDa transmembrane protein whose high expression characterizes Ewing sarcoma (ES), a very aggressive pediatric bone tumor. In addition to its diagnostic value, CD99 has therapeutic potential since it leads to rapid and massive ES cell death when engaged with specific antibodies. Here a novel mechanism of cell death triggered via CD99 is shown, leading, ultimately, to the appearance of macropinocytotic vescicles. Anti-CD99 mAb 0662 induces MDM2 ubiquitination and degradation, which causes not only a p53 reactivation but also the IGF-1R induction and its subsequent internalization; CD99 results internalized together with IGF-1R inside endosomes, but then the two molecules display a different sorting: CD99 is degraded, while IGF-1R is recycled on the surface, causing, as a final step, the up-regulation of RAS-MAPK. High-expressing CD99 mesenchymal stem cells show mild Ras induction but no p53 activation and escape cell death, but in presence of EWS/FLI1 mesenchymal stem cells expressing CD99 show a stronger Ras induction and a p53 reactivation, leading to a significant cell death rate. We propose that CD99 triggering in a EWS/FLI1-driven oncogenetic context creates a synergy between RAS upregulation and p53 activation in ES cells, leading to cell death. Moreover, our data rule out possible concerns on toxicity related to the broad CD99 expression in normal tissues and provide the rationale for the therapeutic use of anti-CD99 MAbs in the clinic.

IGF system, CD99 and tumor-specific chromosomal translocations: evaluation of their cross-talk and definition of their role in Ewing sarcoma and prostate cancer

Aberrant expression of ETS transcription factors, including FLI1 and ERG, due to chromosomal translocations has been described as a driver event in initiation and progression of different tumors. In this study, the impact of prostate cancer (PCa) fusion gene TMPRSS2-ERG was evaluated on components of the insulin-like growth factor (IGF) system and the CD99 molecule, two well documented targets of EWS-FLI1, the hallmark of Ewing sarcoma (ES). The aim of this study was to identify common or distinctive ETS-related mechanisms which could be exploited at biological and clinical level. The results demonstrate that IGF-1R represents a common target of ETS rearrangements as ERG and FLI1 bind IGF-1R gene promoter and their modulation causes alteration in IGF-1R protein levels. At clinical level, this mechanism provides basis for a more rationale use of anti-IGF-1R inhibitors as PCa cells expressing the fusion gene better respond to anti-IGF-1R agents. EWS-FLI1/IGF-1R axis provides rationale for combination of anti-IGF-1R agents with trabectedin, an alkylator agent causing enhanced EWS-FLI1 occupancy on the IGF-1R promoter. TMPRSS2-ERG also influences prognosis relevance of IGF system as high IGF-1R correlates with a better biochemical progression free survival (BPFS) in PCa patients negative for the fusion gene while marginal or no association was found in the total cases or TMPRSS2-ERG-positive cases, respectively. This study indicates CD99 is differentially regulated between ETS-related tumors as CD99 is not a target of ERG. In PCa, CD99 did not show differential expression between TMPRSS2-ERG-positive and –negative cells. A direct correlation was anyway found between ERG and CD99 proteins both in vitro and in patients putatively suggesting that ERG target genes comprehend regulators of CD99. Despite a little trend suggesting a correlation between CD99 expression and a better BPFS, no clinical relevance for CD99 was found in the field of prognostic biomarkers.

Development of functional MRI protocols in the study of neurodegenerative diseases: MRI study in patients with REM sleep behavior disorder, idiopathic Parkinson's disease and multisystem atrophy

In the central nervous system, iron in several proteins is involved in many important processes: oxygen transportation, oxidative phosphorylation, mitochondrial respiration, myelin production, the synthesis and metabolism of neurotransmitters. Abnormal iron homoeostasis can induce cellular damage through hydroxyl radical production, which can cause the oxidation, modification of lipids, proteins, carbohydrates, and DNA, lead to neurotoxicity. Moreover increased levels of iron are harmful and iron accumulations are typical hallmarks of brain ageing and several neurodegenerative disorders particularly PD. Numerous studies on post mortem tissue report on an increased amount of total iron in the substantia nigra in patients with PD also supported by large body of in vivo findings from Magnetic Resonance Imaging (MRI) studies. The importance and approaches for in vivo brain iron assessment using multiparametric MRI is increased over last years. Quantitative MRI may provide useful biomarkers for brain integrity assessment in iron-related neurodegeneration. Particularly, a prominent change in iron- sensitive T2* MRI contrast within the sub areas of the SN overlapping with nigrosome 1 were shown to be a hallmark of Parkinson's Disease with high diagnostic accuracy. Moreover, differential diagnosis between Parkinson's Disease (PD) and atypical parkinsonian syndromes (APS) remains challenging, mainly in the early phases of the disease. Advanced brain MR imaging enables to detect the pathological changes of nigral and extranigral structures at the onset of clinical manifestations and during the course of the disease. The Nigrosome-1 (N1) is a substructure of the healthy Substantia Nigra pars compacta enriched by dopaminergic neurons; their loss in Parkinson’s disease and atypical parkinsonian syndromes is related to the iron accumulation. N1 changes are supportive MR biomarkers for diagnosis of these neurodegenerative disorders, but its detection is hard with conventional sequences, also using high field (3T) scanner. Quantitative susceptibility mapping (QSM), an iron-sensitive technique, enables the direct detection of Neurodegeneration

Towards a sustainable approach for Cultural Heritage Conservation: developing micro-structured green materials and analytical protocols for their performance assessment

Cleaning is one of the most important and delicate procedures that are part of the restoration process. When developing new systems, it is fundamental to consider its selectivity towards the layer to-be-removed, non-invasiveness towards the one to-be-preserved, its sustainability and non-toxicity. Besides assessing its efficacy, it is important to understand its mechanism by analytical protocols that strike a balance between cost, practicality, and reliable interpretation of results. In this thesis, the development of cleaning systems based on the coupling of electrospun fabrics (ES) and greener organic solvents is proposed. Electrospinning is a versatile technique that allows the production of micro/nanostructured non-woven mats, which have already been used as absorbents in various scientific fields, but to date, not in the restoration field. The systems produced proved to be effective for the removal of dammar varnish from paintings, where the ES not only act as solvent-binding agents but also as adsorbents towards the partially solubilised varnish due to capillary rise, thus enabling a one-step procedure. They have also been successfully applied for the removal of spray varnish from marble substrates and wall paintings. Due to the materials' complexity, the procedure had to be adapted case-by-case and mechanical action was still necessary. According to the spinning solution, three types of ES mats have been produced: polyamide 6,6, pullulan and pullulan with melanin nanoparticles. The latter, under irradiation, allows for a localised temperature increase accelerating and facilitating the removal of less soluble layers (e.g. reticulated alkyd-based paints). All the systems produced, and the mock-ups used were extensively characterised using multi-analytical protocols. Finally, a monitoring protocol and image treatment based on photoluminescence macro-imaging is proposed. This set-up allowed the study of the removal mechanism of dammar varnish and semi-quantify its residues. These initial results form the basis for optimising the acquisition set-up and data processing.

Proximity detection protocols for IoT devices

In recent years, we have witnessed the growth of the Internet of Things paradigm, with its increased pervasiveness in our everyday lives. The possible applications are diverse: from a smartwatch able to measure heartbeat and communicate it to the cloud, to the device that triggers an event when we approach an exhibit in a museum. Present in many of these applications is the Proximity Detection task: for instance the heartbeat could be measured only when the wearer is near to a well defined location for medical purposes or the touristic attraction must be triggered only if someone is very close to it. Indeed, the ability of an IoT device to sense the presence of other devices nearby and calculate the distance to them can be considered the cornerstone of various applications, motivating research on this fundamental topic. The energy constraints of the IoT devices are often in contrast with the needs of continuous operations to sense the environment and to achieve high accurate distance measurements from the neighbors, thus making the design of Proximity Detection protocols a challenging task.

Grant-free protocols for massive multiple access

In next generation Internet-of-Things, the overhead introduced by grant-based multiple access protocols may engulf the access network as a consequence of the proliferation of connected devices. Grant-free access protocols are therefore gaining an increasing interest to support massive multiple access. In addition to scalability requirements, new demands have emerged for massive multiple access, including latency and reliability. The challenges envisaged for future wireless communication networks, particularly in the context of massive access, include: i) a very large population size of low power devices transmitting short packets; ii) an ever-increasing scalability requirement; iii) a mild fixed maximum latency requirement; iv) a non-trivial requirement on reliability. To this aim, we suggest the joint utilization of grant-free access protocols, massive MIMO at the base station side, framed schemes to let the contention start and end within a frame, and succesive interference cancellation techniques at the base station side. In essence, this approach is encapsulated in the concept of coded random access with massive MIMO processing. These schemes can be explored from various angles, spanning the protocol stack from the physical (PHY) to the medium access control (MAC) layer. In this thesis, we delve into both of these layers, examining topics ranging from symbol-level signal processing to succesive interference cancellation-based scheduling strategies. In parallel with proposing new schemes, our work includes a theoretical analysis aimed at providing valuable system design guidelines. As a main theoretical outcome, we propose a novel joint PHY and MAC layer design based on density evolution on sparse graphs.