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.

Ottimizzazione del consumo dei grassi durante esercizio fisico: studio di un test per il target mirato di allenamento individuale

Il primo studio ha verificato l'affidabilità del software Polimedicus e gli effetti indotti d'allenamento arobico all’intensità del FatMax. 16 soggetti sovrappeso, di circa 40-55anni, sono stati arruolati e sottoposti a un test incrementale fino a raggiungere un RER di 0,95, e da quel momento il carico è stato aumentato di 1 km/ h ogni minuto fino a esaurimento. Successivamente, è stato verificato se i valori estrapolati dal programma erano quelli che si possono verificare durante a un test a carico costante di 1ora. I soggetti dopo 8 settimane di allenamento hanno fatto un altro test incrementale. Il dati hanno mostrato che Polimedicus non è molto affidabile, soprattutto l'HR. Nel secondo studio è stato sviluppato un nuovo programma, Inca, ed i risultati sono stati confrontati con i dati ottenuti dal primo studio con Polimedicus. I risultati finali hanno mostrato che Inca è più affidabile. Nel terzo studio, abbiamo voluto verificare l'esattezza del calcolo del FatMax con Inca e il test FATmaxwork. 25 soggetti in sovrappeso, tra 40-55 anni, sono stati arruolati e sottoposti al FATmaxwork test. Successivamente, è stato verificato se i valori estrapolati da INCA erano quelli che possono verificarsi durante un carico di prova costante di un'ora. L'analisi ha mostrato una precisione del calcolo della FatMax durante il carico di lavoro. Conclusione: E’ emersa una certa difficoltà nel determinare questo parametro, sia per la variabilità inter-individuale che intra-individuale. In futuro bisognerà migliorare INCA per ottenere protocolli di allenamento ancora più validi.