Formalizing languages for service oriented computing

Service Oriented Computing is a new programming paradigm for addressing distributed system design issues. Services are autonomous computational entities which can be dynamically discovered and composed in order to form more complex systems able to achieve different kinds of task. E-government, e-business and e-science are some examples of the IT areas where Service Oriented Computing will be exploited in the next years. At present, the most credited Service Oriented Computing technology is that of Web Services, whose specifications are enriched day by day by industrial consortia without following a precise and rigorous approach. This PhD thesis aims, on the one hand, at modelling Service Oriented Computing in a formal way in order to precisely define the main concepts it is based upon and, on the other hand, at defining a new approach, called bipolar approach, for addressing system design issues by synergically exploiting choreography and orchestration languages related by means of a mathematical relation called conformance. Choreography allows us to describe systems of services from a global view point whereas orchestration supplies a means for addressing such an issue from a local perspective. In this work we present SOCK, a process algebra based language inspired by the Web Service orchestration language WS-BPEL which catches the essentials of Service Oriented Computing. From the definition of SOCK we will able to define a general model for dealing with Service Oriented Computing where services and systems of services are related to the design of finite state automata and process algebra concurrent systems, respectively. Furthermore, we introduce a formal language for dealing with choreography. Such a language is equipped with a formal semantics and it forms, together with a subset of the SOCK calculus, the bipolar framework. Finally, we present JOLIE which is a Java implentation of a subset of the SOCK calculus and it is part of the bipolar framework we intend to promote.

A communication infrastructure to support knowledge level agents on the web

Agent Communication Languages (ACLs) have been developed to provide a way for agents to communicate with each other supporting cooperation in Multi-Agent Systems. In the past few years many ACLs have been proposed for Multi-Agent Systems, such as KQML and FIPA-ACL. The goal of these languages is to support high-level, human like communication among agents, exploiting Knowledge Level features rather than symbol level ones. Adopting these ACLs, and mainly the FIPA-ACL specifications, many agent platforms and prototypes have been developed. Despite these efforts, an important issue in the research on ACLs is still open and concerns how these languages should deal (at the Knowledge Level) with possible failures of agents. Indeed, the notion of Knowledge Level cannot be straightforwardly extended to a distributed framework such as MASs, because problems concerning communication and concurrency may arise when several Knowledge Level agents interact (for example deadlock or starvation). The main contribution of this Thesis is the design and the implementation of NOWHERE, a platform to support Knowledge Level Agents on the Web. NOWHERE exploits an advanced Agent Communication Language, FT-ACL, which provides high-level fault-tolerant communication primitives and satisfies a set of well defined Knowledge Level programming requirements. NOWHERE is well integrated with current technologies, for example providing full integration for Web services. Supporting different middleware used to send messages, it can be adapted to various scenarios. In this Thesis we present the design and the implementation of the architecture, together with a discussion of the most interesting details and a comparison with other emerging agent platforms. We also present several case studies where we discuss the benefits of programming agents using the NOWHERE architecture, comparing the results with other solutions. Finally, the complete source code of the basic examples can be found in appendix.

Rich media content adaptation in e-learning systems

The wide use of e-technologies represents a great opportunity for underserved segments of the population, especially with the aim of reintegrating excluded individuals back into society through education. This is particularly true for people with different types of disabilities who may have difficulties while attending traditional on-site learning programs that are typically based on printed learning resources. The creation and provision of accessible e-learning contents may therefore become a key factor in enabling people with different access needs to enjoy quality learning experiences and services. Another e-learning challenge is represented by m-learning (which stands for mobile learning), which is emerging as a consequence of mobile terminals diffusion and provides the opportunity to browse didactical materials everywhere, outside places that are traditionally devoted to education. Both such situations share the need to access materials in limited conditions and collide with the growing use of rich media in didactical contents, which are designed to be enjoyed without any restriction. Nowadays, Web-based teaching makes great use of multimedia technologies, ranging from Flash animations to prerecorded video-lectures. Rich media in e-learning can offer significant potential in enhancing the learning environment, through helping to increase access to education, enhance the learning experience and support multiple learning styles. Moreover, they can often be used to improve the structure of Web-based courses. These highly variegated and structured contents may significantly improve the quality and the effectiveness of educational activities for learners. For example, rich media contents allow us to describe complex concepts and process flows. Audio and video elements may be utilized to add a “human touch” to distance-learning courses. Finally, real lectures may be recorded and distributed to integrate or enrich on line materials. A confirmation of the advantages of these approaches can be seen in the exponential growth of video-lecture availability on the net, due to the ease of recording and delivering activities which take place in a traditional classroom. Furthermore, the wide use of assistive technologies for learners with disabilities injects new life into e-learning systems. E-learning allows distance and flexible educational activities, thus helping disabled learners to access resources which would otherwise present significant barriers for them. For instance, students with visual impairments have difficulties in reading traditional visual materials, deaf learners have trouble in following traditional (spoken) lectures, people with motion disabilities have problems in attending on-site programs. As already mentioned, the use of wireless technologies and pervasive computing may really enhance the educational learner experience by offering mobile e-learning services that can be accessed by handheld devices. This new paradigm of educational content distribution maximizes the benefits for learners since it enables users to overcome constraints imposed by the surrounding environment. While certainly helpful for users without disabilities, we believe that the use of newmobile technologies may also become a fundamental tool for impaired learners, since it frees them from sitting in front of a PC. In this way, educational activities can be enjoyed by all the users, without hindrance, thus increasing the social inclusion of non-typical learners. While the provision of fully accessible and portable video-lectures may be extremely useful for students, it is widely recognized that structuring and managing rich media contents for mobile learning services are complex and expensive tasks. Indeed, major difficulties originate from the basic need to provide a textual equivalent for each media resource composing a rich media Learning Object (LO). Moreover, tests need to be carried out to establish whether a given LO is fully accessible to all kinds of learners. Unfortunately, both these tasks are truly time-consuming processes, depending on the type of contents the teacher is writing and on the authoring tool he/she is using. Due to these difficulties, online LOs are often distributed as partially accessible or totally inaccessible content. Bearing this in mind, this thesis aims to discuss the key issues of a system we have developed to deliver accessible, customized or nomadic learning experiences to learners with different access needs and skills. To reduce the risk of excluding users with particular access capabilities, our system exploits Learning Objects (LOs) which are dynamically adapted and transcoded based on the specific needs of non-typical users and on the barriers that they can encounter in the environment. The basic idea is to dynamically adapt contents, by selecting them from a set of media resources packaged in SCORM-compliant LOs and stored in a self-adapting format. The system schedules and orchestrates a set of transcoding processes based on specific learner needs, so as to produce a customized LO that can be fully enjoyed by any (impaired or mobile) student.

3-D reconstruction of the human skeleton during motion

L’analisi del movimento umano ha come obiettivo la descrizione del movimento assoluto e relativo dei segmenti ossei del soggetto e, ove richiesto, dei relativi tessuti molli durante l’esecuzione di esercizi fisici. La bioingegneria mette a disposizione dell’analisi del movimento gli strumenti ed i metodi necessari per una valutazione quantitativa di efficacia, funzione e/o qualità del movimento umano, consentendo al clinico l’analisi di aspetti non individuabili con gli esami tradizionali. Tali valutazioni possono essere di ausilio all’analisi clinica di pazienti e, specialmente con riferimento a problemi ortopedici, richiedono una elevata accuratezza e precisione perché il loro uso sia valido. Il miglioramento della affidabilità dell’analisi del movimento ha quindi un impatto positivo sia sulla metodologia utilizzata, sia sulle ricadute cliniche della stessa. Per perseguire gli obiettivi scientifici descritti, è necessario effettuare una stima precisa ed accurata della posizione e orientamento nello spazio dei segmenti ossei in esame durante l’esecuzione di un qualsiasi atto motorio. Tale descrizione può essere ottenuta mediante la definizione di un modello della porzione del corpo sotto analisi e la misura di due tipi di informazione: una relativa al movimento ed una alla morfologia. L’obiettivo è quindi stimare il vettore posizione e la matrice di orientamento necessari a descrivere la collocazione nello spazio virtuale 3D di un osso utilizzando le posizioni di punti, definiti sulla superficie cutanea ottenute attraverso la stereofotogrammetria. Le traiettorie dei marker, così ottenute, vengono utilizzate per la ricostruzione della posizione e dell’orientamento istantaneo di un sistema di assi solidale con il segmento sotto esame (sistema tecnico) (Cappozzo et al. 2005). Tali traiettorie e conseguentemente i sistemi tecnici, sono affetti da due tipi di errore, uno associato allo strumento di misura e l’altro associato alla presenza di tessuti molli interposti tra osso e cute. La propagazione di quest’ultimo ai risultati finali è molto più distruttiva rispetto a quella dell’errore strumentale che è facilmente minimizzabile attraverso semplici tecniche di filtraggio (Chiari et al. 2005). In letteratura è stato evidenziato che l’errore dovuto alla deformabilità dei tessuti molli durante l’analisi del movimento umano provoca inaccuratezze tali da mettere a rischio l’utilizzabilità dei risultati. A tal proposito Andriacchi scrive: “attualmente, uno dei fattori critici che rallentano il progresso negli studi del movimento umano è la misura del movimento scheletrico partendo dai marcatori posti sulla cute” (Andriacchi et al. 2000). Relativamente alla morfologia, essa può essere acquisita, ad esempio, attraverso l’utilizzazione di tecniche per bioimmagini. Queste vengono fornite con riferimento a sistemi di assi locali in generale diversi dai sistemi tecnici. Per integrare i dati relativi al movimento con i dati morfologici occorre determinare l’operatore che consente la trasformazione tra questi due sistemi di assi (matrice di registrazione) e di conseguenza è fondamentale l’individuazione di particolari terne di riferimento, dette terne anatomiche. L’identificazione di queste terne richiede la localizzazione sul segmento osseo di particolari punti notevoli, detti repere anatomici, rispetto ad un sistema di riferimento solidale con l’osso sotto esame. Tale operazione prende il nome di calibrazione anatomica. Nella maggior parte dei laboratori di analisi del movimento viene implementata una calibrazione anatomica a “bassa risoluzione” che prevede la descrizione della morfologia dell’osso a partire dall’informazione relativa alla posizione di alcuni repere corrispondenti a prominenze ossee individuabili tramite palpazione. Attraverso la stereofotogrammetria è quindi possibile registrare la posizione di questi repere rispetto ad un sistema tecnico. Un diverso approccio di calibrazione anatomica può essere realizzato avvalendosi delle tecniche ad “alta risoluzione”, ovvero attraverso l’uso di bioimmagini. In questo caso è necessario disporre di una rappresentazione digitale dell’osso in un sistema di riferimento morfologico e localizzare i repere d’interesse attraverso palpazione in ambiente virtuale (Benedetti et al. 1994 ; Van Sint Jan et al. 2002; Van Sint Jan et al. 2003). Un simile approccio è difficilmente applicabile nella maggior parte dei laboratori di analisi del movimento, in quanto normalmente non si dispone della strumentazione necessaria per ottenere le bioimmagini; inoltre è noto che tale strumentazione in alcuni casi può essere invasiva. Per entrambe le calibrazioni anatomiche rimane da tenere in considerazione che, generalmente, i repere anatomici sono dei punti definiti arbitrariamente all’interno di un’area più vasta e irregolare che i manuali di anatomia definiscono essere il repere anatomico. L’identificazione dei repere attraverso una loro descrizione verbale è quindi povera in precisione e la difficoltà nella loro identificazione tramite palpazione manuale, a causa della presenza dei tessuti molli interposti, genera errori sia in precisione che in accuratezza. Tali errori si propagano alla stima della cinematica e della dinamica articolare (Ramakrishnan et al. 1991; Della Croce et al. 1999). Della Croce (Della Croce et al. 1999) ha inoltre evidenziato che gli errori che influenzano la collocazione nello spazio delle terne anatomiche non dipendono soltanto dalla precisione con cui vengono identificati i repere anatomici, ma anche dalle regole che si utilizzano per definire le terne. E’ infine necessario evidenziare che la palpazione manuale richiede tempo e può essere effettuata esclusivamente da personale altamente specializzato, risultando quindi molto onerosa (Simon 2004). La presente tesi prende lo spunto dai problemi sopra elencati e ha come obiettivo quello di migliorare la qualità delle informazioni necessarie alla ricostruzione della cinematica 3D dei segmenti ossei in esame affrontando i problemi posti dall’artefatto di tessuto molle e le limitazioni intrinseche nelle attuali procedure di calibrazione anatomica. I problemi sono stati affrontati sia mediante procedure di elaborazione dei dati, sia apportando modifiche ai protocolli sperimentali che consentano di conseguire tale obiettivo. Per quanto riguarda l’artefatto da tessuto molle, si è affrontato l’obiettivo di sviluppare un metodo di stima che fosse specifico per il soggetto e per l’atto motorio in esame e, conseguentemente, di elaborare un metodo che ne consentisse la minimizzazione. Il metodo di stima è non invasivo, non impone restrizione al movimento dei tessuti molli, utilizza la sola misura stereofotogrammetrica ed è basato sul principio della media correlata. Le prestazioni del metodo sono state valutate su dati ottenuti mediante una misura 3D stereofotogrammetrica e fluoroscopica sincrona (Stagni et al. 2005), (Stagni et al. 2005). La coerenza dei risultati raggiunti attraverso i due differenti metodi permette di considerare ragionevoli le stime dell’artefatto ottenute con il nuovo metodo. Tale metodo fornisce informazioni sull’artefatto di pelle in differenti porzioni della coscia del soggetto e durante diversi compiti motori, può quindi essere utilizzato come base per un piazzamento ottimo dei marcatori. Lo si è quindi utilizzato come punto di partenza per elaborare un metodo di compensazione dell’errore dovuto all’artefatto di pelle che lo modella come combinazione lineare degli angoli articolari di anca e ginocchio. Il metodo di compensazione è stato validato attraverso una procedura di simulazione sviluppata ad-hoc. Relativamente alla calibrazione anatomica si è ritenuto prioritario affrontare il problema associato all’identificazione dei repere anatomici perseguendo i seguenti obiettivi: 1. migliorare la precisione nell’identificazione dei repere e, di conseguenza, la ripetibilità dell’identificazione delle terne anatomiche e della cinematica articolare, 2. diminuire il tempo richiesto, 3. permettere che la procedura di identificazione possa essere eseguita anche da personale non specializzato. Il perseguimento di tali obiettivi ha portato alla implementazione dei seguenti metodi: • Inizialmente è stata sviluppata una procedura di palpazione virtuale automatica. Dato un osso digitale, la procedura identifica automaticamente i punti di repere più significativi, nella maniera più precisa possibile e senza l'ausilio di un operatore esperto, sulla base delle informazioni ricavabili da un osso digitale di riferimento (template), preliminarmente palpato manualmente. • E’ stato poi condotto uno studio volto ad indagare i fattori metodologici che influenzano le prestazioni del metodo funzionale nell’individuazione del centro articolare d’anca, come prerequisito fondamentale per migliorare la procedura di calibrazione anatomica. A tale scopo sono stati confrontati diversi algoritmi, diversi cluster di marcatori ed è stata valutata la prestazione del metodo in presenza di compensazione dell’artefatto di pelle. • E’stato infine proposto un metodo alternativo di calibrazione anatomica basato sull’individuazione di un insieme di punti non etichettati, giacenti sulla superficie dell’osso e ricostruiti rispetto ad un TF (UP-CAST). A partire dalla posizione di questi punti, misurati su pelvi coscia e gamba, la morfologia del relativo segmento osseo è stata stimata senza identificare i repere, bensì effettuando un’operazione di matching dei punti misurati con un modello digitale dell’osso in esame. La procedura di individuazione dei punti è stata eseguita da personale non specializzato nell’individuazione dei repere anatomici. Ai soggetti in esame è stato richiesto di effettuare dei cicli di cammino in modo tale da poter indagare gli effetti della nuova procedura di calibrazione anatomica sulla determinazione della cinematica articolare. I risultati ottenuti hanno mostrato, per quel che riguarda la identificazione dei repere, che il metodo proposto migliora sia la precisione inter- che intraoperatore, rispetto alla palpazione convenzionale (Della Croce et al. 1999). E’ stato inoltre riscontrato un notevole miglioramento, rispetto ad altri protocolli (Charlton et al. 2004; Schwartz et al. 2004), nella ripetibilità della cinematica 3D di anca e ginocchio. Bisogna inoltre evidenziare che il protocollo è stato applicato da operatori non specializzati nell’identificazione dei repere anatomici. Grazie a questo miglioramento, la presenza di diversi operatori nel laboratorio non genera una riduzione di ripetibilità. Infine, il tempo richiesto per la procedura è drasticamente diminuito. Per una analisi che include la pelvi e i due arti inferiori, ad esempio, l’identificazione dei 16 repere caratteristici usando la calibrazione convenzionale richiede circa 15 minuti, mentre col nuovo metodo tra i 5 e i 10 minuti.

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.

Support infrastructures for multimedia services with guaranteed continuity and QoS

Advances in wireless networking and content delivery systems are enabling new challenging provisioning scenarios where a growing number of users access multimedia services, e.g., audio/video streaming, while moving among different points of attachment to the Internet, possibly with different connectivity technologies, e.g., Wi-Fi, Bluetooth, and cellular 3G. That calls for novel middlewares capable of dynamically personalizing service provisioning to the characteristics of client environments, in particular to discontinuities in wireless resource availability due to handoffs. This dissertation proposes a novel middleware solution, called MUM, that performs effective and context-aware handoff management to transparently avoid service interruptions during both horizontal and vertical handoffs. To achieve the goal, MUM exploits the full visibility of wireless connections available in client localities and their handoff implementations (handoff awareness), of service quality requirements and handoff-related quality degradations (QoS awareness), and of network topology and resources available in current/future localities (location awareness). The design and implementation of the all main MUM components along with extensive on the field trials of the realized middleware architecture confirmed the validity of the proposed full context-aware handoff management approach. In particular, the reported experimental results demonstrate that MUM can effectively maintain service continuity for a wide range of different multimedia services by exploiting handoff prediction mechanisms, adaptive buffering and pre-fetching techniques, and proactive re-addressing/re-binding.