Analysis and mathematical modeling of wave-structure interaction

The aim of this thesis, included within the THESEUS project, is the development of a mathematical model 2DV two-phase, based on the existing code IH-2VOF developed by the University of Cantabria, able to represent together the overtopping phenomenon and the sediment transport. Several numerical simulations were carried out in order to analyze the flow characteristics on a dike crest. The results show that the seaward/landward slope does not affect the evolution of the flow depth and velocity over the dike crest whereas the most important parameter is the relative submergence. Wave heights decrease and flow velocities increase while waves travel over the crest. In particular, by increasing the submergence, the wave height decay and the increase of the velocity are less marked. Besides, an appropriate curve able to fit the variation of the wave height/velocity over the dike crest were found. Both for the wave height and for the wave velocity different fitting coefficients were determined on the basis of the submergence and of the significant wave height. An equation describing the trend of the dimensionless coefficient c_h for the wave height was derived. These conclusions could be taken into consideration for the design criteria and the upgrade of the structures. In the second part of the thesis, new equations for the representation of the sediment transport in the IH-2VOF model were introduced in order to represent beach erosion while waves run-up and overtop the sea banks during storms. The new model allows to calculate sediment fluxes in the water column together with the sediment concentration. Moreover it is possible to model the bed profile evolution. Different tests were performed under low-intensity regular waves with an homogeneous layer of sand on the bottom of a channel in order to analyze the erosion-deposition patterns and verify the model results.

Neural network modelling of the wave-structure interaction processes

This thesis presents a new Artificial Neural Network (ANN) able to predict at once the main parameters representative of the wave-structure interaction processes, i.e. the wave overtopping discharge, the wave transmission coefficient and the wave reflection coefficient. The new ANN has been specifically developed in order to provide managers and scientists with a tool that can be efficiently used for design purposes. The development of this ANN started with the preparation of a new extended and homogeneous database that collects all the available tests reporting at least one of the three parameters, for a total amount of 16’165 data. The variety of structure types and wave attack conditions in the database includes smooth, rock and armour unit slopes, berm breakwaters, vertical walls, low crested structures, oblique wave attacks. Some of the existing ANNs were compared and improved, leading to the selection of a final ANN, whose architecture was optimized through an in-depth sensitivity analysis to the training parameters of the ANN. Each of the selected 15 input parameters represents a physical aspect of the wave-structure interaction process, describing the wave attack (wave steepness and obliquity, breaking and shoaling factors), the structure geometry (submergence, straight or non-straight slope, with or without berm or toe, presence or not of a crown wall), or the structure type (smooth or covered by an armour layer, with permeable or impermeable core). The advanced ANN here proposed provides accurate predictions for all the three parameters, and demonstrates to overcome the limits imposed by the traditional formulae and approach adopted so far by some of the existing ANNs. The possibility to adopt just one model to obtain a handy and accurate evaluation of the overall performance of a coastal or harbor structure represents the most important and exportable result of the work.

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.

Studies on the interaction of surfactants and neutral cyclodextrins by capillary electrophoresis. Application to chiral analysis

In the present study, mixed systems composed of SDS in the presence of neutral cyclodextrins were considered. Firstly, the effect of the CDs on the CMC of the surfactant was evaluated by CE experiments. Furthermore, a new CE approach based on electric current measurement was developed for the estimation of the stoichiometry as well as of the binding constants of SDS-CDs complexes. The results of these investigations were compared to those obtained with a different technique, electronic paramagnetic resonance (EPR). The obtained results suggested that methylated CDs, in particular (2,6-di-O-methyl)-beta-cyclodextrin (DM-beta-CD), strongly affect the micellization of SDS in comparison to the other studied CDs. This effect also paralleled the chiral CD-MEKC performance, as indicated by the enantioresolution of (+/-)-Catechin, which was firstly selected as a model compound representative of important chiral phytomarkers. Then a CD-MEKC system, composed of sodium dodecyl sulfate as surfactant (90 mM) and hydroxypropyl-beta-cyclodextrin (25 mM) as chiral selector, under acidic conditions (25 mM borate – phosphate buffer, pH 2.5) was applied to study the thermal epimerisation of epi-structured catechins, (-)-Epicatechin and (-)-Epigallocatechin, to non epi-structured (-)-Catechin and (-)-Gallocatechin. The latter compounds, being non-native molecules, were for the first time regarded as useful phytomarkers of tea sample degradation. The proposed method was applied to the analysis of more than twenty tea samples of different geographical origins (China, Japan, Ceylon), having undergone different storage conditions and manufacturing processes.

Multilevel Domain Decomposition Algorithms for Monolithic Fluid-Structure Interaction Problems with Application to Haemodynamics

Finite element techniques for solving the problem of fluid-structure interaction of an elastic solid material in a laminar incompressible viscous flow are described. The mathematical problem consists of the Navier-Stokes equations in the Arbitrary Lagrangian-Eulerian formulation coupled with a non-linear structure model, considering the problem as one continuum. The coupling between the structure and the fluid is enforced inside a monolithic framework which computes simultaneously for the fluid and the structure unknowns within a unique solver. We used the well-known Crouzeix-Raviart finite element pair for discretization in space and the method of lines for discretization in time. A stability result using the Backward-Euler time-stepping scheme for both fluid and solid part and the finite element method for the space discretization has been proved. The resulting linear system has been solved by multilevel domain decomposition techniques. Our strategy is to solve several local subproblems over subdomain patches using the Schur-complement or GMRES smoother within a multigrid iterative solver. For validation and evaluation of the accuracy of the proposed methodology, we present corresponding results for a set of two FSI benchmark configurations which describe the self-induced elastic deformation of a beam attached to a cylinder in a laminar channel flow, allowing stationary as well as periodically oscillating deformations, and for a benchmark proposed by COMSOL multiphysics where a narrow vertical structure attached to the bottom wall of a channel bends under the force due to both viscous drag and pressure. Then, as an example of fluid-structure interaction in biomedical problems, we considered the academic numerical test which consists in simulating the pressure wave propagation through a straight compliant vessel. All the tests show the applicability and the numerical efficiency of our approach to both two-dimensional and three-dimensional problems.