AE06. Esercizi risolti sulla dinamica del punto materiale

Trasparenze presentate a lezione. Si consiglia agli studenti di stamparne una copia prima della lezione e di portarla con sé onde riportare su di essa ulteriori annotazioni.

AE07. Esercizi risolti sulla dinamica del corpo rigido

Trasparenze presentate a lezione. Si consiglia agli studenti di stamparne una copia prima della lezione e di portarla con sé onde riportare su di essa ulteriori annotazioni.

AE08. Esercizi risolti sui principi di conservazione.

Trasparenze presentate a lezione. Si consiglia agli studenti di stamparne una copia prima della lezione e di portarla con sé onde riportare su di essa ulteriori annotazioni.

EE01. Esercizi di esame di Meccanica con risultati.

Esercizi di esame per i corsi di Fisica Generale. I compiti di esame contengono esercizi sorteggiati da questa lista, nell'ultima versione disponibile sul Web 15 giorni prima della data di esame. I punteggi riportati a fianco dei quesiti/esercizi sono calcolati dinamicamente sulla base dei precedenti risultati nelle prove di esame, in modo da rendere il secondo terzile della distribuzione dei voti sul singolo esercizio pari a 3/3. In altre parole il punteggio assegnato al singolo quesito/esercizio è tale da assicurare che un terzo degli studenti che hanno affrontato l'esercizio ottenga la massima valutazione. Il punteggio degli esercizi riportato sul file è indicativo. Esso si modifica dinamicamente a ogni esame, in modo che a ogni esame diviene una valutazione più precisa della difficoltà dell'esercizio (all'aumentare della statistica sperimentale l'errore di misura diminuisce).

EQ01. Quesiti di esame di Meccanica

Quesiti di esame per i corsi di Fisica Generale. I compiti di esame contengono quesiti sorteggiati da questa lista, nell'ultima versione disponibile sul Web 15 giorni prima della data di esame. I punteggi riportati a fianco dei quesiti/esercizi sono calcolati dinamicamente sulla base dei precedenti risultati nelle prove di esame, in modo da rendere il secondo terzile della distribuzione dei voti sul singolo esercizio pari a 3/3. In altre parole il punteggio assegnato al singolo quesito/esercizio è tale da assicurare che un terzo degli studenti che hanno affrontato l'esercizio ottenga la massima valutazione. Il punteggio degli esercizi riportato sul file è indicativo. Esso si modifica dinamicamente a ogni esame, in modo che a ogni esame diviene una valutazione più precisa della difficoltà dell'esercizio (all'aumentare della statistica sperimentale l'errore di misura diminuisce).

Il foglio elettronico: strumenti, funzioni ed applicazioni

Utilizzare i lucidi come supporto alle lezioni e gli esempli appicativi come sussidi ed esempi da comprendere ed imitare

Secure gossiping techniques and components

Gossip protocols have proved to be a viable solution to set-up and manage largescale P2P services or applications in a fully decentralised scenario. The gossip or epidemic communication scheme is heavily based on stochastic behaviors and it is the fundamental idea behind many large-scale P2P protocols. It provides many remarkable features, such as scalability, robustness to failures, emergent load balancing capabilities, fast spreading, and redundancy of information. In some sense, these services or protocols mimic natural system behaviors in order to achieve their goals. The key idea of this work is that the remarkable properties of gossip hold when all the participants follow the rules dictated by the actual protocols. If one or more malicious nodes join the network and start cheating according to some strategy, the result can be catastrophic. In order to study how serious the threat posed by malicious nodes can be and what can be done to prevent attackers from cheating, we focused on a general attack model aimed to defeat a key service in gossip overlay networks (the Peer Sampling Service [JGKvS04]). We also focused on the problem of protecting against forged information exchanged in gossip services. We propose a solution technique for each problem; both techniques are general enough to be applied to distinct service implementations. As gossip protocols, our solutions are based on stochastic behavior and are fully decentralized. In addition, each technique’s behaviour is abstracted by a general primitive function extending the basic gossip scheme; this approach allows the adoptions of our solutions with minimal changes in different scenarios. We provide an extensive experimental evaluation to support the effectiveness of our techniques. Basically, these techniques aim to be building blocks or P2P architecture guidelines in building more resilient and more secure P2P services.

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.

L'analisi di rischio nel trasporto stradale di merci pericolose: due software a confronto

Confronto tra due software specifici per l'analisi di rischio nel trasporto stradale di merci pericolose (TRAT GIS 4.1 e QRAM 3.6) mediante applicazione a un caso di studio semplice e al caso reale di Casalecchio di Reno, comune della provincia di Bologna.

Models for the study of neuronal activity during cognitive tasks

Assessment of brain connectivity among different brain areas during cognitive or motor tasks is a crucial problem in neuroscience today. Aim of this research study is to use neural mass models to assess the effect of various connectivity patterns in cortical EEG power spectral density (PSD), and investigate the possibility to derive connectivity circuits from EEG data. To this end, two different models have been built. In the first model an individual region of interest (ROI) has been built as the parallel arrangement of three populations, each one exhibiting a unimodal spectrum, at low, medium or high frequency. Connectivity among ROIs includes three parameters, which specify the strength of connection in the different frequency bands. Subsequent studies demonstrated that a single population can exhibit many different simultaneous rhythms, provided that some of these come from external sources (for instance, from remote regions). For this reason in the second model an individual ROI is simulated only with a single population. Both models have been validated by comparing the simulated power spectral density with that computed in some cortical regions during cognitive and motor tasks. Another research study is focused on multisensory integration of tactile and visual stimuli in the representation of the near space around the body (peripersonal space). This work describes an original neural network to simulate representation of the peripersonal space around the hands, in basal conditions and after training with a tool used to reach the far space. The model is composed of three areas for each hand, two unimodal areas (visual and tactile) connected to a third bimodal area (visual-tactile), which is activated only when a stimulus falls within the peripersonal space. Results show that the peripersonal space, which includes just a small visual space around the hand in normal conditions, becomes elongated in the direction of the tool after training, thanks to a reinforcement of synapses.

Tools and methods for the quality assurance of force platforms in human movement analysis

The human movement analysis (HMA) aims to measure the abilities of a subject to stand or to walk. In the field of HMA, tests are daily performed in research laboratories, hospitals and clinics, aiming to diagnose a disease, distinguish between disease entities, monitor the progress of a treatment and predict the outcome of an intervention [Brand and Crowninshield, 1981; Brand, 1987; Baker, 2006]. To achieve these purposes, clinicians and researchers use measurement devices, like force platforms, stereophotogrammetric systems, accelerometers, baropodometric insoles, etc. This thesis focus on the force platform (FP) and in particular on the quality assessment of the FP data. The principal objective of our work was the design and the experimental validation of a portable system for the in situ calibration of FPs. The thesis is structured as follows: Chapter 1. Description of the physical principles used for the functioning of a FP: how these principles are used to create force transducers, such as strain gauges and piezoelectrics transducers. Then, description of the two category of FPs, three- and six-component, the signals acquisition (hardware structure), and the signals calibration. Finally, a brief description of the use of FPs in HMA, for balance or gait analysis. Chapter 2. Description of the inverse dynamics, the most common method used in the field of HMA. This method uses the signals measured by a FP to estimate kinetic quantities, such as joint forces and moments. The measures of these variables can not be taken directly, unless very invasive techniques; consequently these variables can only be estimated using indirect techniques, as the inverse dynamics. Finally, a brief description of the sources of error, present in the gait analysis. Chapter 3. State of the art in the FP calibration. The selected literature is divided in sections, each section describes: systems for the periodic control of the FP accuracy; systems for the error reduction in the FP signals; systems and procedures for the construction of a FP. In particular is detailed described a calibration system designed by our group, based on the theoretical method proposed by ?. This system was the “starting point” for the new system presented in this thesis. Chapter 4. Description of the new system, divided in its parts: 1) the algorithm; 2) the device; and 3) the calibration procedure, for the correct performing of the calibration process. The algorithm characteristics were optimized by a simulation approach, the results are here presented. In addiction, the different versions of the device are described. Chapter 5. Experimental validation of the new system, achieved by testing it on 4 commercial FPs. The effectiveness of the calibration was verified by measuring, before and after calibration, the accuracy of the FPs in measuring the center of pressure of an applied force. The new system can estimate local and global calibration matrices; by local and global calibration matrices, the non–linearity of the FPs was quantified and locally compensated. Further, a non–linear calibration is proposed. This calibration compensates the non– linear effect in the FP functioning, due to the bending of its upper plate. The experimental results are presented. Chapter 6. Influence of the FP calibration on the estimation of kinetic quantities, with the inverse dynamics approach. Chapter 7. The conclusions of this thesis are presented: need of a calibration of FPs and consequential enhancement in the kinetic data quality. Appendix: Calibration of the LC used in the presented system. Different calibration set–up of a 3D force transducer are presented, and is proposed the optimal set–up, with particular attention to the compensation of non–linearities. The optimal set–up is verified by experimental results.

Computational analyses on the structure-function relation in ion channels

Ion channels are protein molecules, embedded in the lipid bilayer of the cell membranes. They act as powerful sensing elements switching chemicalphysical stimuli into ion-fluxes. At a glance, ion channels are water-filled pores, which can open and close in response to different stimuli (gating), and one once open select the permeating ion species (selectivity). They play a crucial role in several physiological functions, like nerve transmission, muscular contraction, and secretion. Besides, ion channels can be used in technological applications for different purpose (sensing of organic molecules, DNA sequencing). As a result, there is remarkable interest in understanding the molecular determinants of the channel functioning. Nowadays, both the functional and the structural characteristics of ion channels can be experimentally solved. The purpose of this thesis was to investigate the structure-function relation in ion channels, by computational techniques. Most of the analyses focused on the mechanisms of ion conduction, and the numerical methodologies to compute the channel conductance. The standard techniques for atomistic simulation of complex molecular systems (Molecular Dynamics) cannot be routinely used to calculate ion fluxes in membrane channels, because of the high computational resources needed. The main step forward of the PhD research activity was the development of a computational algorithm for the calculation of ion fluxes in protein channels. The algorithm - based on the electrodiffusion theory - is computational inexpensive, and was used for an extensive analysis on the molecular determinants of the channel conductance. The first record of ion-fluxes through a single protein channel dates back to 1976, and since then measuring the single channel conductance has become a standard experimental procedure. Chapter 1 introduces ion channels, and the experimental techniques used to measure the channel currents. The abundance of functional data (channel currents) does not match with an equal abundance of structural data. The bacterial potassium channel KcsA was the first selective ion channels to be experimentally solved (1998), and after KcsA the structures of four different potassium channels were revealed. These experimental data inspired a new era in ion channel modeling. Once the atomic structures of channels are known, it is possible to define mathematical models based on physical descriptions of the molecular systems. These physically based models can provide an atomic description of ion channel functioning, and predict the effect of structural changes. Chapter 2 introduces the computation methods used throughout the thesis to model ion channels functioning at the atomic level. In Chapter 3 and Chapter 4 the ion conduction through potassium channels is analyzed, by an approach based on the Poisson-Nernst-Planck electrodiffusion theory. In the electrodiffusion theory ion conduction is modeled by the drift-diffusion equations, thus describing the ion distributions by continuum functions. The numerical solver of the Poisson- Nernst-Planck equations was tested in the KcsA potassium channel (Chapter 3), and then used to analyze how the atomic structure of the intracellular vestibule of potassium channels affects the conductance (Chapter 4). As a major result, a correlation between the channel conductance and the potassium concentration in the intracellular vestibule emerged. The atomic structure of the channel modulates the potassium concentration in the vestibule, thus its conductance. This mechanism explains the phenotype of the BK potassium channels, a sub-family of potassium channels with high single channel conductance. The functional role of the intracellular vestibule is also the subject of Chapter 5, where the affinity of the potassium channels hEag1 (involved in tumour-cell proliferation) and hErg (important in the cardiac cycle) for several pharmaceutical drugs was compared. Both experimental measurements and molecular modeling were used in order to identify differences in the blocking mechanism of the two channels, which could be exploited in the synthesis of selective blockers. The experimental data pointed out the different role of residue mutations in the blockage of hEag1 and hErg, and the molecular modeling provided a possible explanation based on different binding sites in the intracellular vestibule. Modeling ion channels at the molecular levels relates the functioning of a channel to its atomic structure (Chapters 3-5), and can also be useful to predict the structure of ion channels (Chapter 6-7). In Chapter 6 the structure of the KcsA potassium channel depleted from potassium ions is analyzed by molecular dynamics simulations. Recently, a surprisingly high osmotic permeability of the KcsA channel was experimentally measured. All the available crystallographic structure of KcsA refers to a channel occupied by potassium ions. To conduct water molecules potassium ions must be expelled from KcsA. The structure of the potassium-depleted KcsA channel and the mechanism of water permeation are still unknown, and have been investigated by numerical simulations. Molecular dynamics of KcsA identified a possible atomic structure of the potassium-depleted KcsA channel, and a mechanism for water permeation. The depletion from potassium ions is an extreme situation for potassium channels, unlikely in physiological conditions. However, the simulation of such an extreme condition could help to identify the structural conformations, so the functional states, accessible to potassium ion channels. The last chapter of the thesis deals with the atomic structure of the !- Hemolysin channel. !-Hemolysin is the major determinant of the Staphylococcus Aureus toxicity, and is also the prototype channel for a possible usage in technological applications. The atomic structure of !- Hemolysin was revealed by X-Ray crystallography, but several experimental evidences suggest the presence of an alternative atomic structure. This alternative structure was predicted, combining experimental measurements of single channel currents and numerical simulations. This thesis is organized in two parts, in the first part an overview on ion channels and on the numerical methods adopted throughout the thesis is provided, while the second part describes the research projects tackled in the course of the PhD programme. The aim of the research activity was to relate the functional characteristics of ion channels to their atomic structure. In presenting the different research projects, the role of numerical simulations to analyze the structure-function relation in ion channels is highlighted.

Pavimentazione stradale: studio della regolarità

Lo scopo del presente elaborato è lo studio della regolarità stradale. La regolarità è una caratteristica fondamentale sia dal punto di vista dell’utenza, poiché da essa dipendono il comfort, ma soprattutto, la sicurezza della guida, sia dal punto di vista dell’ente proprietario della strada, perché dalla regolarità dipende la pianificazione della manutenzione della rete viaria, con tutti i pesi economici che essa comporta. Da questa piccola considerazione si comprende perché nell’ultimo secolo l’argomento abbia suscitato sempre maggiore interesse, vedendo la nascita, sin dagli anni ’50, di strumenti sempre più sofisticati, grazie allo sviluppo dell’elettronica, e sempre più veloci nell’acquisizione dei dati, per far fronte al contemporaneo sviluppo della rete viaria. Nel primo capitolo si affronterà la tematica della regolarità stradale, cercando di comprenderne la natura e i suoi livelli di degrado, dei quali viene fatta un’ampia descrizione, comprensiva di cause scatenanti. Inoltre si fa un accenno al Catasto Stradale, poiché costituisce uno strumento essenziale per la gestione dell’infrastruttura viaria e per l’ottimizzazione delle risorse destinate alla sua manutenzione e alla sua sicurezza; infine si parla delle tecnologie finalizzate al rilievo della regolarità. Il secondo capitolo è dedicato al panorama normativo in materia di regolarità stradale. Le varie norme sono commentate nel dettaglio, data l’importanza di una standardizzazione nella calibrazione e nell’uso degli strumenti di rilievo e nelle procedure di stima della regolarità. Il capitolo successivo contiene una trattazione sugli indici di regolarità, ma l’attenzione è in particolar modo rivolta all’IRI, l’indice internazionale di irregolarità. Per le caratteristiche con cui è stato concepito, cioè stabilità temporale, validità e compatibilità, è stato assunto come scala di riferimento internazionale, a cui gli altri indici possono riferirsi. Viene quindi illustrato il significato di IRI, il modello matematico su cui si basa la sua definizione, per passare poi al procedimento analitico e a quello informatico con il quale viene calcolato. Essendo la presente tesi avvenuta in collaborazione con la ditta Siteco Informatica di Bologna, nel capitolo quarto, sono stati analizzati gli strumenti installati sul veicolo ad alto rendimento (VAR) messo a disposizione dalla ditta stessa. Gli strumenti consistono principalmente in dispositivi per il calcolo del posizionamento e dell’assetto del veicolo, in un profilometro laser per il rilievo della regolarità stradale e in un laser scanner, di cui si è tentato di studiarne le potenzialità nell’ambito dell’oggetto di questa tesi. Il percorso di ricerca ha incluso l’esperienza diretta in sito tramite varie campagne di rilievo, per meglio comprendere il mezzo e la natura dei dati ottenuti. Si è quindi ripercorso l’intero processo di elaborazione dei dati grezzi di rilievo, così com’è strutturato per le finalità della ditta collaborante, per utilizzare poi il dato finito per finalità ingegneristiche.