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.

Biomeccanica del servizio e del diritto nel tennis: confronto fra atleti di livello di gioco differente

Il tennis è uno sport molto diffuso che negli ultimi trent’anni ha subito molti cambiamenti. Con l’avvento di nuovi materiali più leggeri e maneggevoli la velocità della palla è aumentata notevolmente, rendendo così necessario una modifica a livello tecnico dei colpi fondamentali. Dalla ricerca bibliografica sono emerse interessanti indicazioni su angoli e posizioni corporee ideali da mantenere durante le varie fasi dei colpi, confrontando i giocatori di altissimo livello. Non vi sono invece indicazioni per i maestri di tennis su quali siano i parametri più importanti da allenare a seconda del livello di gioco del proprio atleta. Lo scopo di questa tesi è quello di individuare quali siano le variabili tecniche che influenzano i colpi del diritto e del servizio confrontando atleti di genere differente, giocatori di livello di gioco diverso (esperti, intermedi, principianti) e dopo un anno di attività programmata. Confrontando giocatori adulti di genere diverso, è emerso che le principali differenze sono legate alle variabili di prestazione (velocità della palla e della racchetta) per entrambi i colpi. Questi dati sono simili a quelli riscontrati nel test del lancio della palla, un gesto non influenzato dalla tecnica del colpo. Le differenze tecniche di genere sono poco rilevanti ed attribuibili alla diversa interpretazione dei soggetti. Nel confronto di atleti di vario livello di gioco le variabili di prestazione presentano evidenti differenze, che possono essere messe in relazione con alcune differenze tecniche rilevate nei gesti specifici. Nel servizio i principianti tendono a direzionare l’arto superiore dominante verso la zona bersaglio, abducendo maggiormente la spalla ed avendo il centro della racchetta più a destra rispetto al polso. Inoltre, effettuano un caricamento minore degli arti inferiori, del tronco e del gomito. Per quanto riguarda il diritto si possono evidenziare queste differenze: l’arto superiore è sempre maggiormente esteso per il gruppo dei principianti; il tronco, nei giocatori più abili viene utilizzato in maniera più marcata, durante la fase di caricamento, in movimenti di torsione e di inclinazione laterale. Gli altri due gruppi hanno maggior difficoltà nell’eseguire queste azioni preparatorie, in particolare gli atleti principianti. Dopo un anno di attività programmata sono stati evidenziati miglioramenti prestativi. Anche dal punto di vista tecnico sono state notate delle differenze che possono spiegare il miglioramento della performance nei colpi. Nel servizio l’arto superiore si estende maggiormente per colpire la palla più in alto possibile. Nel diritto sono da sottolineare soprattutto i miglioramenti dei movimenti del tronco in torsione ed in inclinazione laterale. Quindi l’atleta si avvicina progressivamente ad un’esecuzione tecnica corretta. In conclusione, dal punto di vista tecnico non sono state rilevate grosse differenze tra i due generi che possano spiegare le differenze di performance. Perciò questa è legata più ad un fattore di forza che dovrà essere allenata con un programma specifico. Nel confronto fra i vari livelli di gioco e gli effetti di un anno di pratica si possono individuare variabili tecniche che mostrano differenze significative tra i gruppi sperimentali. Gli evoluti utilizzano tutto il corpo per effettuare dei colpi più potenti, utilizzando in maniera tecnicamente più valida gli arti inferiori, il tronco e l’arto superiore. I principianti utilizzano prevalentemente l’arto superiore con contributi meno evidenti degli altri segmenti. Dopo un anno di attività i soggetti esaminati hanno dimostrato di saper utilizzare meglio il tronco e l’arto superiore e ciò può spiegare il miglioramento della performance. Si può ipotizzare che, per il corretto utilizzo degli arti inferiori, sia necessario un tempo più lungo di apprendimento oppure un allenamento più specifico.

Analisi biomeccanica del MAWASHI GERI JODAN in cinture nere di Karate: modelli tecnici a confronto

In martial arts there are several ways to perform the turning kick . Following the martial arts or different learning models many types of kicks take shape. Mawashi geri is the karate turning kick. At the moment there are two models of mawashi geri, one comes from the traditional karate (OLD), and the other newer (NEW), who agrees to the change of the rules of W.K.F. (World Karate Federation) happened in 2000 (Macan J. et all 2006) . In this study we are focus on the differences about two models the mawashi geri jodan of karate. The purpose of this study is to analyse cinematic and kinetic parameters of mawashi geri jodan. Timing of the striking and supporting leg actions were also evaluated A Vicon system 460 IR with 6 cameras at sample frequency of 200 Hz was used. 37 reflective markers have been set on the skin of the subjects following the “PlugInGait-total body model”. The participants performed five repetitions of mawashi geri jodan at maximum rapidity with their dominant leg against a ball suspended in front of them placed at ear height. Fourteen skilled subjects (mean level black belt 1,7 dan; age 20,9±4,8 yrs; height 171,4±7,3 cm; weight 60,9±10,2 Kg) practicing karate have been split in two group through the hierarchical cluster analysis following their technical characteristics. By means of the Mann Whitney-U test (Spss-package) the differences between the two groups were verified in preparatory and execution phase. Kicking knee at start, kicking hip and knee at take-off were different between the two groups (p < 0,05). Striking hip flexion during the spin of the supporting foot was different between the two groups (p < 0,05). Peak angular velocity of hip flexion were different between the two groups (p < 0,05). Groups showed differences also in timing of the supporting spin movement. While Old group spin the supporting foot at 30% of the trial, instead New start spinning at 44% of the trial. Old group showed a greater supporting foot spin than New (Old 110° Vs New 82°). Abduction values didn’t show any differences between the two groups. At the hit has been evaluated a 120° of double hips abduction, for the entire sample. Striking knee extension happened for everybody after the kicking hip flexion and confirm the proximal-distal action of the striking leg (Sorensen H. 1996). In contrast with Pearson J.N. 1997 and Landeo R 2007, peak velocity of the striking foot is not useful to describe kick performance because affected by the stature. Two groups are different either in preparatory phase or in execution phase. The body is set in difference manner already before the take-off of the kicking foot. The groups differ for the timing of the supporting foot action Trainer should pay attention to starting posture and on abduction capacities of the athletes.

Three-dimensional joint kinematics of swimming using body-worn inertial and magnetic sensors

Wearable inertial and magnetic measurements units (IMMU) are an important tool for underwater motion analysis because they are swimmer-centric, they require only simple measurement set-up and they provide the performance results very quickly. In order to estimate 3D joint kinematics during motion, protocols were developed to transpose the IMMU orientation estimation to a biomechanical model. The aim of the thesis was to validate a protocol originally propositioned to estimate the joint angles of the upper limbs during one-degree-of-freedom movements in dry settings and herein modified to perform 3D kinematics analysis of shoulders, elbows and wrists during swimming. Eight high-level swimmers were assessed in the laboratory by means of an IMMU while simulating the front crawl and breaststroke movements. A stereo-photogrammetric system (SPS) was used as reference. The joint angles (in degrees) of the shoulders (flexion-extension, abduction-adduction and internal-external rotation), the elbows (flexion-extension and pronation-supination), and the wrists (flexion-extension and radial-ulnar deviation) were estimated with the two systems and compared by means of root mean square errors (RMSE), relative RMSE, Pearson’s product-moment coefficient correlation (R) and coefficient of multiple correlation (CMC). Subsequently, the athletes were assessed during pool swimming trials through the IMMU. Considering both swim styles and all joint degrees of freedom modeled, the comparison between the IMMU and the SPS showed median values of RMSE lower than 8°, representing 10% of overall joint range of motion, high median values of CMC (0.97) and R (0.96). These findings suggest that the protocol accurately estimated the 3D orientation of the shoulders, elbows and wrists joint during swimming with accuracy adequate for the purposes of research. In conclusion, the proposed method to evaluate the 3D joint kinematics through IMMU was revealed to be a useful tool for both sport and clinical contexts.