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.

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.

EXAM-S: an Analysis tool for Multi-Domain Policy Sets

As distributed collaborative applications and architectures are adopting policy based management for tasks such as access control, network security and data privacy, the management and consolidation of a large number of policies is becoming a crucial component of such policy based systems. In large-scale distributed collaborative applications like web services, there is the need of analyzing policy interactions and integrating policies. In this thesis, we propose and implement EXAM-S, a comprehensive environment for policy analysis and management, which can be used to perform a variety of functions such as policy property analyses, policy similarity analysis, policy integration etc. As part of this environment, we have proposed and implemented new techniques for the analysis of policies that rely on a deep study of state of the art techniques. Moreover, we propose an approach for solving heterogeneity problems that usually arise when considering the analysis of policies belonging to different domains. Our work focuses on analysis of access control policies written in the dialect of XACML (Extensible Access Control Markup Language). We consider XACML policies because XACML is a rich language which can represent many policies of interest to real world applications and is gaining widespread adoption in the industry.

Implementazione di un modulo HTTPS in JOLIE per l'orchestrazione dei servizi

La tesi è relativa all'implementazione di un modulo per la comunicazione sicura tramite SSL/TLS sviluppato in JAVA che aggiunge il supporto del protocollo HTTPS a JOLIE. Le politiche di SSL/TLS vengono applicate mediante l'utilizzo dell'API SSLEngine, che viene descritta accuratamente. La tesi contiene inoltre un caso d'uso in cui viene utilizzato JOLIE per sviluppare un servizio di autenticazione integrata (single sign-on) tra l'ELMS Webstore del programma Microsoft MSDNAA e l'Università di Bologna.

Semantic coordination through programmable Tuple spaces

Two of the main features of today complex software systems like pervasive computing systems and Internet-based applications are distribution and openness. Distribution revolves around three orthogonal dimensions: (i) distribution of control|systems are characterised by several independent computational entities and devices, each representing an autonomous and proactive locus of control; (ii) spatial distribution|entities and devices are physically distributed and connected in a global (such as the Internet) or local network; and (iii) temporal distribution|interacting system components come and go over time, and are not required to be available for interaction at the same time. Openness deals with the heterogeneity and dynamism of system components: complex computational systems are open to the integration of diverse components, heterogeneous in terms of architecture and technology, and are dynamic since they allow components to be updated, added, or removed while the system is running. The engineering of open and distributed computational systems mandates for the adoption of a software infrastructure whose underlying model and technology could provide the required level of uncoupling among system components. This is the main motivation behind current research trends in the area of coordination middleware to exploit tuple-based coordination models in the engineering of complex software systems, since they intrinsically provide coordinated components with communication uncoupling and further details in the references therein. An additional daunting challenge for tuple-based models comes from knowledge-intensive application scenarios, namely, scenarios where most of the activities are based on knowledge in some form|and where knowledge becomes the prominent means by which systems get coordinated. Handling knowledge in tuple-based systems induces problems in terms of syntax - e.g., two tuples containing the same data may not match due to differences in the tuple structure - and (mostly) of semantics|e.g., two tuples representing the same information may not match based on a dierent syntax adopted. Till now, the problem has been faced by exploiting tuple-based coordination within a middleware for knowledge intensive environments: e.g., experiments with tuple-based coordination within a Semantic Web middleware (surveys analogous approaches). However, they appear to be designed to tackle the design of coordination for specic application contexts like Semantic Web and Semantic Web Services, and they result in a rather involved extension of the tuple space model. The main goal of this thesis was to conceive a more general approach to semantic coordination. In particular, it was developed the model and technology of semantic tuple centres. It is adopted the tuple centre model as main coordination abstraction to manage system interactions. A tuple centre can be seen as a programmable tuple space, i.e. an extension of a Linda tuple space, where the behaviour of the tuple space can be programmed so as to react to interaction events. By encapsulating coordination laws within coordination media, tuple centres promote coordination uncoupling among coordinated components. Then, the tuple centre model was semantically enriched: a main design choice in this work was to try not to completely redesign the existing syntactic tuple space model, but rather provide a smooth extension that { although supporting semantic reasoning { keep the simplicity of tuple and tuple matching as easier as possible. By encapsulating the semantic representation of the domain of discourse within coordination media, semantic tuple centres promote semantic uncoupling among coordinated components. The main contributions of the thesis are: (i) the design of the semantic tuple centre model; (ii) the implementation and evaluation of the model based on an existent coordination infrastructure; (iii) a view of the application scenarios in which semantic tuple centres seem to be suitable as coordination media.

Analyse von Middleware-Technologien bzgl. Performanz und ihrer Eignung für lose und eng gekoppelte verteilte Anwendungen

Die vorliegende Dissertation analysiert die Middleware- Technologien CORBA (Common Object Request Broker Architecture), COM/DCOM (Component Object Model/Distributed Component Object Model), J2EE (Java-2-Enterprise Edition) und Web Services (inklusive .NET) auf ihre Eignung bzgl. eng und lose gekoppelten verteilten Anwendungen. Zusätzlich werden primär für CORBA die dynamischen CORBA-Komponenten DII (Dynamic Invocation Interface), IFR (Interface Repository) und die generischen Datentypen Any und DynAny (dynamisches Any) im Detail untersucht. Ziel ist es, a. konkrete Aussagen über diese Komponenten zu erzielen, und festzustellen, in welchem Umfeld diese generischen Ansätze ihre Berechtigung finden. b. das zeitliche Verhalten der dynamischen Komponenten bzgl. der Informationsgewinnung über die unbekannten Objekte zu analysieren. c. das zeitliche Verhalten der dynamischen Komponenten bzgl. ihrer Kommunikation zu messen. d. das zeitliche Verhalten bzgl. der Erzeugung von generischen Datentypen und das Einstellen von Daten zu messen und zu analysieren. e. das zeitliche Verhalten bzgl. des Erstellens von unbekannten, d. h. nicht in IDL beschriebenen Datentypen zur Laufzeit zu messen und zu analysieren. f. die Vorzüge/Nachteile der dynamischen Komponenten aufzuzeigen, ihre Einsatzgebiete zu definieren und mit anderen Technologien wie COM/DCOM, J2EE und den Web Services bzgl. ihrer Möglichkeiten zu vergleichen. g. Aussagen bzgl. enger und loser Koppelung zu tätigen. CORBA wird als standardisierte und vollständige Verteilungsplattform ausgewählt, um die o. a. Problemstellungen zu untersuchen. Bzgl. seines dynamischen Verhaltens, das zum Zeitpunkt dieser Ausarbeitung noch nicht oder nur unzureichend untersucht wurde, sind CORBA und die Web Services richtungsweisend bzgl. a. Arbeiten mit unbekannten Objekten. Dies kann durchaus Implikationen bzgl. der Entwicklung intelligenter Softwareagenten haben. b. der Integration von Legacy-Applikationen. c. der Möglichkeiten im Zusammenhang mit B2B (Business-to-Business). Diese Problemstellungen beinhalten auch allgemeine Fragen zum Marshalling/Unmarshalling von Daten und welche Aufwände hierfür notwendig sind, ebenso wie allgemeine Aussagen bzgl. der Echtzeitfähigkeit von CORBA-basierten, verteilten Anwendungen. Die Ergebnisse werden anschließend auf andere Technologien wie COM/DCOM, J2EE und den Web Services, soweit es zulässig ist, übertragen. Die Vergleiche CORBA mit DCOM, CORBA mit J2EE und CORBA mit Web Services zeigen im Detail die Eignung dieser Technologien bzgl. loser und enger Koppelung. Desweiteren werden aus den erzielten Resultaten allgemeine Konzepte bzgl. der Architektur und der Optimierung der Kommunikation abgeleitet. Diese Empfehlungen gelten uneingeschränkt für alle untersuchten Technologien im Zusammenhang mit verteilter Verarbeitung.

Cloud Computing: analisi dei modelli architetturali e delle tecnologie per lo sviluppo di applicazioni

Uno dei temi più discussi ed interessanti nel mondo dell’informatica al giorno d’oggi è sicuramente il Cloud Computing. Nuove organizzazioni che offrono servizi di questo tipo stanno nascendo ovunque e molte aziende oggi desiderano imparare ad utilizzarli, migrando i loro centri di dati e le loro applicazioni nel Cloud. Ciò sta avvenendo anche grazie alla spinta sempre più forte che stanno imprimendo le grandi compagnie nella comunità informatica: Google, Amazon, Microsoft, Apple e tante altre ancora parlano sempre più frequentemente di Cloud Computing e si stanno a loro volta ristrutturando profondamente per poter offrire servizi Cloud adeguandosi così a questo grande cambiamento che sta avvenendo nel settore dell’informatica. Tuttavia il grande movimento di energie, capitali, investimenti ed interesse che l’avvento del Cloud Computing sta causando non aiuta a comprendere in realtà che cosa esso sia, al punto tale che oggi non ne esiste ancora una definizione univoca e condivisa. La grande pressione inoltre che esso subisce da parte del mondo del mercato fa sì che molte delle sue più peculiari caratteristiche, dal punto di vista dell’ingegneria del software, vengano nascoste e soverchiate da altre sue proprietà, architetturalmente meno importanti, ma con un più grande impatto sul pubblico di potenziali clienti. L’obbiettivo che ci poniamo con questa tesi è quindi quello di esplorare il nascente mondo del Cloud Computing, cercando di comprenderne a fondo le principali caratteristiche architetturali e focalizzando l’attenzione in particolare sullo sviluppo di applicazioni in ambiente Cloud, processo che sotto alcuni aspetti si differenzia molto dallo sviluppo orientato ad ambienti più classici. La tesi è così strutturata: nel primo capitolo verrà fornita una panoramica sul Cloud Computing nella quale saranno date anche le prime definizioni e verranno esposti tutti i temi fondamentali sviluppati nei capitoli successivi. Il secondo capitolo costituisce un approfondimento su un argomento specifico, quello dei Cloud Operating System, componenti fondamentali che permettono di trasformare una qualunque infrastruttura informatica in un’infrastruttura Cloud. Essi verranno presentati anche per mezzo di molte analogie con i classici sistemi operativi desktop. Con il terzo capitolo ci si addentra più a fondo nel cuore del Cloud Computing, studiandone il livello chiamato Infrastructure as a Service tramite un esempio concreto di Cloud provider: Amazon, che fornisce i suoi servizi nel progetto Amazon Web Services. A questo punto, più volte nel corso della trattazione di vari temi saremo stati costretti ad affrontare le problematiche relative alla gestione di enormi moli di dati, che spesso sono il punto centrale di molte applicazioni Cloud. Ci è parso quindi importante approfondire questo argomento in un capitolo appositamente dedicato, il quarto, supportando anche in questo caso la trattazione teorica con un esempio concreto: BigTable, il sistema di Google per la gestione della memorizzazione di grandi quantità di dati. Dopo questo intermezzo, la trattazione procede risalendo lungo i livelli dell’architettura Cloud, ricalcando anche quella che è stata l’evoluzione temporale del Cloud Computing: nel quinto capitolo, dal livello Infrastructure as a Service si passa quindi a quello Platform as a Service, tramite lo studio dei servizi offerti da Google Cloud Platform. Il sesto capitolo costituisce invece il punto centrale della tesi, quello che ne soddisfa l’obbiettivo principale: esso contiene infatti uno studio approfondito sullo sviluppo di applicazioni orientate all’ambiente Cloud. Infine, il settimo capitolo si pone come un ponte verso possibili sviluppi futuri, analizzando quali sono i limiti principali delle tecnologie, dei modelli e dei linguaggi che oggi supportano il Cloud Computing. In esso viene proposto come possibile soluzione il modello ad attori; inoltre viene anche presentato il framework Orleans, che Microsoft sta sviluppando negli ultimi anni con lo scopo appunto di supportare lo sviluppo di applicazioni in ambiente Cloud.

Jolie - un linguaggio Service Oriented

Nella tesi vengono descritte le caratteristiche principali del linguaggio di programmazione service-oriented Jolie, analizzandone ampiamente la sintassi e proponendo esempi di utilizzo degli operatori e dei costrutti. Viene fatta una panoramica di SOC, SOA, Web Services, Cloud Computing, Orchestrazione, Coreografia, Deployment e Behaviour, gli ultimi due analizzati in diversi capitoli. La tesi si conclude con un esempio di conversione di servizi WSDL in Jolie, producendo un esempio di utilizzo del Web Service convertito. Nel documento vengono accennati i progressi storici del linguaggio ed i loro sviluppatori, nonché le API fornite dal linguaggio.

Notifiche push in applicativi Android: uso di gcm ed una soluzione alternativa basata su long-polling http

Vengono presentate due soluzioni per le notifiche push in ambiente Android: le soluzioni trattate riguardano l'uso di GCM (Google Cloud Messaging) ed una implementazione che impiega il Long-Polling HTTP come alternativa al servizio GCM.

Groupme: city data and multi-preference activity allocation

Classic group recommender systems focus on providing suggestions for a fixed group of people. Our work tries to give an inside look at design- ing a new recommender system that is capable of making suggestions for a sequence of activities, dividing people in subgroups, in order to boost over- all group satisfaction. However, this idea increases problem complexity in more dimensions and creates great challenge to the algorithm’s performance. To understand the e↵ectiveness, due to the enhanced complexity and pre- cise problem solving, we implemented an experimental system from data collected from a variety of web services concerning the city of Paris. The sys- tem recommends activities to a group of users from two di↵erent approaches: Local Search and Constraint Programming. The general results show that the number of subgroups can significantly influence the Constraint Program- ming Approaches’s computational time and e�cacy. Generally, Local Search can find results much quicker than Constraint Programming. Over a lengthy period of time, Local Search performs better than Constraint Programming, with similar final results.

Elasticity in Cloud Computing: Tecnologia e applicazione aziendale presso Onit

Il Cloud Computing permette di utilizzare al meglio le risorse distribuite allo scopo di risolvere problemi di computazione su larga scala, e viene distribuito dai provider all'utente finale sotto forma di servizio. Presentati i diversi modelli di distribuzione dei servizi Cloud, si discutono le varie tipologie di servizi offerti. Efficaci meccanismi di elasticità e scalabilità hanno permesso al Cloud Computing di superare lo scoglio iniziale di utilizzo medio dei server al 10%. L'elasticità (rapid elasticity) è l’abilità di acquisire e rilasciare le risorse di un'infrastruttura Cloud su richiesta, l’abilità di un'applicazione di cambiare le sue dimensione durante il suo tempo di esecuzione; la scalabilità è un prerequisito per ottenere una buona elasticità per il sistema, ed è l'abilità che ha un layer di sostenere carichi di lavoro variabili continuando ad adempiere agli obblighi imposti dallo SLA allocando o disallocando risorse computazionali. Le diverse modalità di scaling e il loro utilizzo determinano la scalabilità e di conseguenza l'elasticità del sistema, e sfruttano la virtualizzazione per poter funzionare. Ciò ha portato notevoli benefici perchè aumenta l'utilizzo dei server, migliora l'efficienza del sistema, e dona flessibilità in caso di errori massimizzando il tempo di funzionamento. Sono stati introdotti due esempi di sistemi elastici basati ovviamente sulla virtualizzazione come Amazon Web Services e Microsoft Azure, che dominano il mercato del Cloud Computing e fanno uso dei più efficenti meccanismi d'elasticità. Il cuore di questo elaborato è l'analisi dell'ampliamento dell'adozione del Cloud Computing in azienda Onit Group srl. L'obiettivo è trattare i punti fondamentali per il Cloud Computing, analizzarli e immagazzinare tutte queste conoscenze per analizzare lo stato attuale del Cloud nell'azienda focalizzando l'attenzione sui vantaggi e sugli svantaggi che un sostanziale ampliamento dell'adozione ai sistemi Cloud poteva apportare.

Managing server energy and reducing operational cost for online service providers

The past decade has seen the energy consumption in servers and Internet Data Centers (IDCs) skyrocket. A recent survey estimated that the worldwide spending on servers and cooling have risen to above $30 billion and is likely to exceed spending on the new server hardware . The rapid rise in energy consumption has posted a serious threat to both energy resources and the environment, which makes green computing not only worthwhile but also necessary. This dissertation intends to tackle the challenges of both reducing the energy consumption of server systems and by reducing the cost for Online Service Providers (OSPs). Two distinct subsystems account for most of IDC’s power: the server system, which accounts for 56% of the total power consumption of an IDC, and the cooling and humidifcation systems, which accounts for about 30% of the total power consumption. The server system dominates the energy consumption of an IDC, and its power draw can vary drastically with data center utilization. In this dissertation, we propose three models to achieve energy effciency in web server clusters: an energy proportional model, an optimal server allocation and frequency adjustment strategy, and a constrained Markov model. The proposed models have combined Dynamic Voltage/Frequency Scaling (DV/FS) and Vary-On, Vary-off (VOVF) mechanisms that work together for more energy savings. Meanwhile, corresponding strategies are proposed to deal with the transition overheads. We further extend server energy management to the IDC’s costs management, helping the OSPs to conserve, manage their own electricity cost, and lower the carbon emissions. We have developed an optimal energy-aware load dispatching strategy that periodically maps more requests to the locations with lower electricity prices. A carbon emission limit is placed, and the volatility of the carbon offset market is also considered. Two energy effcient strategies are applied to the server system and the cooling system respectively. With the rapid development of cloud services, we also carry out research to reduce the server energy in cloud computing environments. In this work, we propose a new live virtual machine (VM) placement scheme that can effectively map VMs to Physical Machines (PMs) with substantial energy savings in a heterogeneous server cluster. A VM/PM mapping probability matrix is constructed, in which each VM request is assigned with a probability running on PMs. The VM/PM mapping probability matrix takes into account resource limitations, VM operation overheads, server reliability as well as energy effciency. The evolution of Internet Data Centers and the increasing demands of web services raise great challenges to improve the energy effciency of IDCs. We also express several potential areas for future research in each chapter.

Zellulare Fördertechnik

Dieser Artikel beschreibt die Vision einer vollständig service-orientierten Architektur zur Steuerung von Materialflusssystemen. Dies setzt eine intelligente Umgebung voraus, innerhalb derer die adäquaten (Web) Services zum Anlauf gebracht werden können. Verteilte Server übernehmen das Management und die Organisation des Systems innerhalb dieser Umgebung. In letzter Konsequenz ermöglicht dies die vollständige Selbstorganisation von Materialflusssystemen, deren Fördertechnik folgerichtig eine zellulare Struktur und als Vision künftiger Fördertechnik eine organische Anpassung an dynamische Anforderungsprofile ermöglicht.

User and Machine Authentication and Authorization Infrastructure for Distributed Wireless Sensor Network Testbeds

The intention of an authentication and authorization infrastructure (AAI) is to simplify and unify access to different web resources. With a single login, a user can access web applications at multiple organizations. The Shibboleth authentication and authorization infrastructure is a standards-based, open source software package for web single sign-on (SSO) across or within organizational boundaries. It allows service providers to make fine-grained authorization decisions for individual access of protected online resources. The Shibboleth system is a widely used AAI, but only supports protection of browser-based web resources. We have implemented a Shibboleth AAI extension to protect web services using Simple Object Access Protocol (SOAP). Besides user authentication for browser-based web resources, this extension also provides user and machine authentication for web service-based resources. Although implemented for a Shibboleth AAI, the architecture can be easily adapted to other AAIs.

Customized mashups for improved reputation visualization

This document describes a possible use for the YouReputation API. A mashup combining the YouReputation and the Flickr APIs attempts to improve the visualization of reputation. First, this paper gives an introduction to Web services and APIs and further explains the developed prototype. This paper introduces an API that can be easily combined with other APIs to improve the representation of reputation terms and therefore enhance usability and design.