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.

Architettura delle centrali idroelettriche italiane 1910-1940. L'esperienza di Giovanni Muzio e Piero Portaluppi

Oggetto della ricerca è il tema dello spazio delle centrali idroelettriche costruite nella prima metà del Novecento dagli architetti Giovanni Muzio e Piero Portaluppi. L’individuazione del tema sorge dalla volontà di indagare quali siano stati gli sviluppi dal punto di vista architettonico all’interno di un genere così specifico durante un periodo di tempo in cui gli stili architettonici e le tendenze hanno subito stravolgimenti ed evoluzioni che ancora oggi trovano una difficile connotazione e definizione precisa. L’analisi dell’architettura delle centrali idroelettriche, effettuata ripercorrendo le principali vicende del settore idroelettrico dalla fine del secolo scorso al secondo dopoguerra, oltre a considerare il rapporto con il contesto territoriale e culturale del nostro Paese vuole prendere in considerazione anche il particolare rapporto che in più casi si è venuto a creare tra committenti e progettisti. Compito della tesi è rileggere un settore poco indagato finora e capire se vi sia stata effettivamente una evoluzione architettonica dal punto di vista tipologico o se la centrale sia stata sempre affrontata come semplice esercizio di “vestizione” di un involucro precostituito da precise esigenze tecniche. La ricerca infatti si pone come obiettivo lo studio delle centrali non solo dal punto di vista tipologico e spaziale dei suoi principali elementi, ma si pone come obiettivo anche lo studio della loro distribuzione nel sito in cui sono sorte, distribuzione che spesso ha portato alla formazione di una sorta di vera e propria “città elettrica”, in cui la composizione dei vari elementi segue una logica compositiva ben precisa. Dal punto di vista del contributo originale la ricerca vuole proporre una serie di riflessioni ed elaborati inerenti alcune centrali non ancora indagate. Nel caso specifico di Portaluppi l’apporto originale consiste nell’aver portato alla luce notizie inerenti centrali che sono sempre state poste in secondo piano rispetto le ben più note e studiate centrali della Val d’Ossola. Nel caso invece di Muzio il contributo consiste in una analisi approfondita e in una comparazione di documenti che di solito sono sempre stati pubblicati come semplice apparato iconografico, ma che messi a confronto danno una lettura di quelle che sono state le fasi e le elaborazioni progettuali apportate dall’autore. Il tema della ricerca è stato affrontato poi attraverso una lettura delle fonti dirette relative agli scritti degli autori, con una contemporanea lettura di testi, articoli e interventi tratti dalle riviste appartenenti al periodo in esame per comprendere al meglio il panorama culturale e architettonico che hanno fatto da scenario alle esperienze di entrambe le figure oggetto di studio. Infine la ricerca si è concentrata sull’analisi di alcune opere in particolare - due centrali idroelettriche per ciascun autore oggetto della tesi - scelte perché considerate rappresentative sia per impianto spaziale e tipologico, sia per le scelte compositive e stilistiche adottate. La lettura dei manufatti architettonici scelti è stata condotta con l’analisi di copie di elaborati grafici originali, foto d’epoca e altri documenti reperiti grazie ad una ricerca condotta in vari archivi. Le centrali scelte nell’ambito delle esperienze maturate da Muzio e Portaluppi sono state individuate per rappresentare il quadro relativo allo sviluppo e alla ricerca di un nuovo linguaggio formale da adottare nell’ambito dell’architettura di questi manufatti. Per entrambi i protagonisti oggetto della ricerca sono state individuate due centrali in grado di dare una visione il più possibile completa dell’evoluzione della tematica delle centrali idroelettriche all’interno della loro esperienza, prendendo in considerazione soprattutto gli aspetti legati all’evoluzione del loro linguaggio compositivo e stilistico. L’individuazione delle centrali da analizzare è stata dettata prendendo in considerazione alcuni fattori come il tipo di impianto, le relazioni e confronto con il contesto geografico e naturale e le soluzioni adottate.

Expressiveness in biologically inspired languages

A very recent and exciting new area of research is the application of Concurrency Theory tools to formalize and analyze biological systems and one of the most promising approach comes from the process algebras (process calculi). A process calculus is a formal language that allows to describe concurrent systems and comes with well-established techniques for quantitative and qualitative analysis. Biological systems can be regarded as concurrent systems and therefore modeled by means of process calculi. In this thesis we focus on the process calculi approach to the modeling of biological systems and investigate, mostly from a theoretical point of view, several promising bio-inspired formalisms: Brane Calculi and k-calculus family. We provide several expressiveness results mostly by means of comparisons between calculi. We provide a lower bound to the computational power of the non Turing complete MDB Brane Calculi by showing an encoding of a simple P-System into MDB. We address the issue of local implementation within the k-calculus family: whether n-way rewrites can be simulated by binary interactions only. A solution introducing divergence is provided and we prove a deterministic solution preserving the termination property is not possible. We use the symmetric leader election problem to test synchronization capabilities within the k-calculus family. Several fragments of the original k-calculus are considered and we prove an impossibility result about encoding n-way synchronization into (n-1)-way synchronization. A similar impossibility result is obtained in a pure computer science context. We introduce CCSn, an extension of CCS with multiple input prefixes and show, using the dining philosophers problem, that there is no reasonable encoding of CCS(n+1) into CCSn.

Searching and retrieving in content-based repositories of formal mathematical knowledge

In this thesis, the author presents a query language for an RDF (Resource Description Framework) database and discusses its applications in the context of the HELM project (the Hypertextual Electronic Library of Mathematics). This language aims at meeting the main requirements coming from the RDF community. in particular it includes: a human readable textual syntax and a machine-processable XML (Extensible Markup Language) syntax both for queries and for query results, a rigorously exposed formal semantics, a graph-oriented RDF data access model capable of exploring an entire RDF graph (including both RDF Models and RDF Schemata), a full set of Boolean operators to compose the query constraints, fully customizable and highly structured query results having a 4-dimensional geometry, some constructions taken from ordinary programming languages that simplify the formulation of complex queries. The HELM project aims at integrating the modern tools for the automation of formal reasoning with the most recent electronic publishing technologies, in order create and maintain a hypertextual, distributed virtual library of formal mathematical knowledge. In the spirit of the Semantic Web, the documents of this library include RDF metadata describing their structure and content in a machine-understandable form. Using the author's query engine, HELM exploits this information to implement some functionalities allowing the interactive and automatic retrieval of documents on the basis of content-aware requests that take into account the mathematical nature of these documents.