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.

Expressiveness of Concurrent Languages

The aim of this thesis is to go through different approaches for proving expressiveness properties in several concurrent languages. We analyse four different calculi exploiting for each one a different technique. We begin with the analysis of a synchronous language, we explore the expressiveness of a fragment of CCS! (a variant of Milner's CCS where replication is considered instead of recursion) w.r.t. the existence of faithful encodings (i.e. encodings that respect the behaviour of the encoded model without introducing unnecessary computations) of models of computability strictly less expressive than Turing Machines. Namely, grammars of types 1,2 and 3 in the Chomsky Hierarchy. We then move to asynchronous languages and we study full abstraction for two Linda-like languages. Linda can be considered as the asynchronous version of CCS plus a shared memory (a multiset of elements) that is used for storing messages. After having defined a denotational semantics based on traces, we obtain fully abstract semantics for both languages by using suitable abstractions in order to identify different traces which do not correspond to different behaviours. Since the ability of one of the two variants considered of recognising multiple occurrences of messages in the store (which accounts for an increase of expressiveness) reflects in a less complex abstraction, we then study other languages where multiplicity plays a fundamental role. We consider the language CHR (Constraint Handling Rules) a language which uses multi-headed (guarded) rules. We prove that multiple heads augment the expressive power of the language. Indeed we show that if we restrict to rules where the head contains at most n atoms we could generate a hierarchy of languages with increasing expressiveness (i.e. the CHR language allowing at most n atoms in the heads is more expressive than the language allowing at most m atoms, with m

A core calculus for the analysis and implementation of biologically inspired languages

The application of Concurrency Theory to Systems Biology is in its earliest stage of progress. The metaphor of cells as computing systems by Regev and Shapiro opened the employment of concurrent languages for the modelling of biological systems. Their peculiar characteristics led to the design of many bio-inspired formalisms which achieve higher faithfulness and specificity. In this thesis we present pi@, an extremely simple and conservative extension of the pi-calculus representing a keystone in this respect, thanks to its expressiveness capabilities. The pi@ calculus is obtained by the addition of polyadic synchronisation and priority to the pi-calculus, in order to achieve compartment semantics and atomicity of complex operations respectively. In its direct application to biological modelling, the stochastic variant of the calculus, Spi@, is shown able to model consistently several phenomena such as formation of molecular complexes, hierarchical subdivision of the system into compartments, inter-compartment reactions, dynamic reorganisation of compartment structure consistent with volume variation. The pivotal role of pi@ is evidenced by its capability of encoding in a compositional way several bio-inspired formalisms, so that it represents the optimal core of a framework for the analysis and implementation of bio-inspired languages. In this respect, the encodings of BioAmbients, Brane Calculi and a variant of P Systems in pi@ are formalised. The conciseness of their translation in pi@ allows their indirect comparison by means of their encodings. Furthermore it provides a ready-to-run implementation of minimal effort whose correctness is granted by the correctness of the respective encoding functions. Further important results of general validity are stated on the expressive power of priority. Several impossibility results are described, which clearly state the superior expressiveness of prioritised languages and the problems arising in the attempt of providing their parallel implementation. To this aim, a new setting in distributed computing (the last man standing problem) is singled out and exploited to prove the impossibility of providing a purely parallel implementation of priority by means of point-to-point or broadcast communication.

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.

Theoretical and implementation aspects in the mechanization of the metatheory of programming languages

Interactive theorem provers are tools designed for the certification of formal proofs developed by means of man-machine collaboration. Formal proofs obtained in this way cover a large variety of logical theories, ranging from the branches of mainstream mathematics, to the field of software verification. The border between these two worlds is marked by results in theoretical computer science and proofs related to the metatheory of programming languages. This last field, which is an obvious application of interactive theorem proving, poses nonetheless a serious challenge to the users of such tools, due both to the particularly structured way in which these proofs are constructed, and to difficulties related to the management of notions typical of programming languages like variable binding. This thesis is composed of two parts, discussing our experience in the development of the Matita interactive theorem prover and its use in the mechanization of the metatheory of programming languages. More specifically, part I covers: - the results of our effort in providing a better framework for the development of tactics for Matita, in order to make their implementation and debugging easier, also resulting in a much clearer code; - a discussion of the implementation of two tactics, providing infrastructure for the unification of constructor forms and the inversion of inductive predicates; we point out interactions between induction and inversion and provide an advancement over the state of the art. In the second part of the thesis, we focus on aspects related to the formalization of programming languages. We describe two works of ours: - a discussion of basic issues we encountered in our formalizations of part 1A of the Poplmark challenge, where we apply the extended inversion principles we implemented for Matita; - a formalization of an algebraic logical framework, posing more complex challenges, including multiple binding and a form of hereditary substitution; this work adopts, for the encoding of binding, an extension of Masahiko Sato's canonical locally named representation we designed during our visit to the Laboratory for Foundations of Computer Science at the University of Edinburgh, under the supervision of Randy Pollack.

Frugivores, seed dispersal and tree regeneration along a human disturbance gradient in East African tropical rainforests

Samenausbreitung und Regeneration von Bäumen sind wichtig für den langfristigen Bestand von Baum- und Frugivorengemeinschaften in tropischen Regenwäldern. Zunehmende Rohdung und Degradation gefährden den Ablauf dieser mutualistischen Prozesse in diesem Ökosystem. Um den Einfluss von kleinräumiger menschlicher Störung auf die Frugivorengemeinschaft und die zentralen Ökosystemprozesse Samenausbreitung und Regeneration zu erforschen, habe ich 1) die Frugivorengemeinschaft und die Samenausbreitungsrate von Celtis durandii (Ulmaceae) und 2) den Zusammenhang zwischen Baumarten mit fleischigen Früchten, Frugivoren und der Etablierung von Keimlingen dieser Baumarten in unterschiedlich stark gestörten Flächen dreier ostafrikanischer tropischer Regenwälder untersucht. Insgesamt konnte ich 40 frugivore Vogel- und Primatenarten in den drei untersuchten Waldgebieten nachweisen. Auf gering gestörten Flächen wurden mehr Frugivore als auf stark gestörten Flächen aufgenommen. Auch die Beobachtungen an C. durandii ergaben mehr frugivore Besucher in Bäumen auf gering gestörten als auf stark gestörten Flächen. Dies führte zu einer marginal signifikant höheren Samenausbreitungsrate auf den gering gestörten Flächen. Diese Ergebnisse waren auf regionaler Ebene in allen drei untersuchten Wäldern konsistent. Dies zeigt, dass kleinräumige Störung einen umfassenderen negativen Einfluss auf Frugivore und ihre Funktion als Samenausbreiter hat als zuvor angenommen. Bei der Vegetationserfassung nahm ich 131 verschiedene Baumarten mit fleischigen Früchten in den drei Regenwäldern auf. Kleinräumige menschliche Störung erhöhte den Artenreichtum dieser Baumarten marginal signifikant, hatte jedoch keinen direkten Einfluss auf die Frugivorendichte und den Artenreichtum von Keimlingen dieser Baumarten. Der Artenreichtum von Baumarten mit fleischigen Früchten zeigte einen marginal signifikant positiven Einfluss auf die Frugivorendichte, allerdings nicht auf die Keimlinge. Allerdings führte die Dichte der Frugivoren zu signifikant erhöhtem Artenreichtum der Keimlinge. Folglich scheint kleinräumige Störung die Keimlingsetablierung indirekt durch erhöhten Baumartenreichtum und erhöhte Frugivorendichte zu beeinflussen. Die Frugivorendichte hatte einen größeren Einfluss auf die Waldregeneration als kleinräumige Störung und Baumartenreichtum. Demnach scheint kleinräumige menschliche Störung sowohl positive als auch negative Effekte auf Samenausbreitung und Regeneration zu haben. Somit sind weitere Studien notwendig, die den Einfluss von kleinräumiger menschlicher Störung auf Mutualismen tropischer Regenwälder aufklären.

The role of the West African Monsoon in the tropical to mid-latitudes climate

The interaction between atmosphere–land–ocean–biosphere systems plays a prominent role on the atmospheric dynamics and on the convective rainfall distribution over the West Africa monsoon area during the boreal summer. In particular, the initialization of convective systems in the Sub – Sahelian region has been directly linked to soil moisture heterogeneities identified as the major triggering, development and propagation of convective systems. The present study aims at investigating African monsoon large scale convective dynamics and rainfall diurnal cycle through an exploration of the hypothesis behind the mechanisms of a monsoon phenomenon as an emergence of a collective dynamics of many propagating convective systems. Such hypothesis is based on the existence of an internal self – regulation mechanism among the various components. To achieve these results a multiple analysis was performed based on remote sensed rainfall dataset, and global and regional modelling data for a period of 5 seasons: 2004 - 2008. Satellite rainfall data and convective occurrence variability were studied for assessing typical spatio – temporal signatures and characteristics with an emphasis to the diurnal cycle footprint. A global model and regional model simulation datasets, specifically developed for this analysis and based on Regional Atmospheric Modelling System – RAMS, have been analysed. Results from numerical model datasets highlight the evidence of a synchronization between the destabilization of the convective boundary layer and rainfall occurrence due to the solar radiation forcing through the latent heat release. This supports the conclusion that the studied interacting systems are associated with a process of mutual adjustment of rhythms. Furthermore, this rainfall internal coherence was studied in relation to the West African Heat Low pressure system, which has a prominent role in the large scale summer variability over the Mediterranean area since it is acting as one of dynamic link between sub tropical and midlatitudes variability.

Evolutionary tendencies in African Marantaceae

Die Marantaceae (550 Arten) sind eine weltweit verbreitete Familie von Stauden und Lianen aus dem Unterwuchs tropischer Tieflandregenwälder. Der morphologisch-ökologische Vergleich des basal abzweigenden Sarcophrynium-Astes mit dem in abgeleiteter Position stehenden Marantochloa-Ast, soll beispielhaft evolutionäre Muster in der Familie beleuchten. So wird in der Doktorarbeit zum ersten Mal ein Überblick über die Blütenbiologie und Phylogenie von rund 30 der 40 afrikanischen Marantaceae Arten präsentiert. Die Analysen basieren auf Daten von drei mehrmonatigen Feldaufenthalten in Gabun jeweils zwischen September und Januar. Vier Blütentypen werden beschrieben, die jeweils mit einer spezifischen Bestäubergilde verbunden sind (kleine, mittlere, große Bienen bzw. Vögel). Bestäubungsexperimente belegen, dass 18 Arten selbstkompatibel, aber nur zwei Arten autogam sind, also keine Bestäubungsvermittler benötigen. Der Fruchtansatz ist generell gering (10 -30 %). Die komplexe Synorganisation der Blüte ermöglicht in den Marantaceae einen explosiven Bestäubungsmechanismus. Um dessen ökologische Funktionalität zu verstehen, werden die Blüten von 66 Arten, alle wichtigen Äste der Marantaceae abdeckend, unter einem morphologisch-funktionalen Gesichtspunkt untersucht. Es gibt große Übereinstimmungen zwischen allen untersuchten Arten im Zusammenspiel (Synorganisation) der wichtigsten Bauelemente (Griffel, Kapuzenblatt, Schwielenblatt), die eine präzise Pollenübertragung ermöglichen. Basierend auf Daten von nrDNA (ITS, 5S) und cpDNA (trnL-F) wird für ein nahezu komplettes Artenspektrum die Phylogenie der zwei afrikanischen Äste erstellt. Hierauf werden morphologische und ökologische Merkmale sowie geographischer Verbreitungsmuster nach dem Parsimonieprinzip rekonstruiert, um so deren evolutionäre Bedeutung für die Marantaceae abschätzen zu können. Die Ergebnisse weisen auf die Beteiligung einer Vielzahl verschiedener Artbildungsfaktoren hin.

A study of two Languages for Active Objects with Futures

In computer systems, specifically in multithread, parallel and distributed systems, a deadlock is both a very subtle problem - because difficult to pre- vent during the system coding - and a very dangerous one: a deadlocked system is easily completely stuck, with consequences ranging from simple annoyances to life-threatening circumstances, being also in between the not negligible scenario of economical losses. Then, how to avoid this problem? A lot of possible solutions has been studied, proposed and implemented. In this thesis we focus on detection of deadlocks with a static program analysis technique, i.e. an analysis per- formed without actually executing the program. To begin, we briefly present the static Deadlock Analysis Model devel- oped for coreABS−− in chapter 1, then we proceed by detailing the Class- based coreABS−− language in chapter 2. Then, in Chapter 3 we lay the foundation for further discussions by ana- lyzing the differences between coreABS−− and ASP, an untyped Object-based calculi, so as to show how it can be possible to extend the Deadlock Analysis to Object-based languages in general. In this regard, we explicit some hypotheses in chapter 4 first by present- ing a possible, unproven type system for ASP, modeled after the Deadlock Analysis Model developed for coreABS−−. Then, we conclude our discussion by presenting a simpler hypothesis, which may allow to circumvent the difficulties that arises from the definition of the ”ad-hoc” type system discussed in the aforegoing chapter.

Engineering Agent-Oriented Technologies and Programming Languages for Computer Programming and Software Development

Mainstream hardware is becoming parallel, heterogeneous, and distributed on every desk, every home and in every pocket. As a consequence, in the last years software is having an epochal turn toward concurrency, distribution, interaction which is pushed by the evolution of hardware architectures and the growing of network availability. This calls for introducing further abstraction layers on top of those provided by classical mainstream programming paradigms, to tackle more effectively the new complexities that developers have to face in everyday programming. A convergence it is recognizable in the mainstream toward the adoption of the actor paradigm as a mean to unite object-oriented programming and concurrency. Nevertheless, we argue that the actor paradigm can only be considered a good starting point to provide a more comprehensive response to such a fundamental and radical change in software development. Accordingly, the main objective of this thesis is to propose Agent-Oriented Programming (AOP) as a high-level general purpose programming paradigm, natural evolution of actors and objects, introducing a further level of human-inspired concepts for programming software systems, meant to simplify the design and programming of concurrent, distributed, reactive/interactive programs. To this end, in the dissertation first we construct the required background by studying the state-of-the-art of both actor-oriented and agent-oriented programming, and then we focus on the engineering of integrated programming technologies for developing agent-based systems in their classical application domains: artificial intelligence and distributed artificial intelligence. Then, we shift the perspective moving from the development of intelligent software systems, toward general purpose software development. Using the expertise maturated during the phase of background construction, we introduce a general-purpose programming language named simpAL, which founds its roots on general principles and practices of software development, and at the same time provides an agent-oriented level of abstraction for the engineering of general purpose software systems.

Comparing genetic and linguistic diversity in African populations with a focus on the Khoisan of southern Africa

The interaction between disciplines in the study of human population history is of primary importance, profiting from the biological and cultural characteristics of humankind. In fact, data from genetics, linguistics, archaeology and cultural anthropology can be combined to allow for a broader research perspective. This multidisciplinary approach is here applied to the study of the prehistory of sub-Saharan African populations: in this continent, where Homo sapiens originally started his evolution and diversification, the understanding of the patterns of human variation has a crucial relevance. For this dissertation, molecular data is interpreted and complemented with a major contribution from linguistics: linguistic data are compared to the genetic data and the research questions are contextualized within a linguistic perspective. In the four articles proposed, we analyze Y chromosome SNPs and STRs profiles and full mtDNA genomes on a representative number of samples to investigate key questions of African human variability. Some of these questions address i) the amount of genetic variation on a continental scale and the effects of the widespread migration of Bantu speakers, ii) the extent of ancient population structure, which has been lost in present day populations, iii) the colonization of the southern edge of the continent together with the degree of population contact/replacement, and iv) the prehistory of the diverse Khoisan ethnolinguistic groups, who were traditionally understudied despite representing one of the most ancient divergences of modern human phylogeny. Our results uncover a deep level of genetic structure within the continent and a multilayered pattern of contact between populations. These case studies represent a valuable contribution to the debate on our prehistory and open up further research threads.

Evolution of South African Bruniaceae: evidence from ecological and geographical investigations

The central aim of the present study was to analyse ecological and geographical mechanisms that led to the species diversity and distribution pattern of the South African (sub-) endemic Bruniaceae shown today. To answer the question if the endangerment of some species and the sometimes restricted distribution area is due to an incongruence of pollination and breeding system, pollinator observations and the breeding system were analysed. rnThe effectiveness of the plant-pollinator interactions should be reflected in the reproductive success wherefore fruit set analyses were carried out. The genetic constitution of distant and close-by populations along a spatial gradient should illuminate gene-flow or habitat isolation that could have led to the species diversity. Since niche-inhabitation could be shown in the present study, an overall biogeographical analysis illuminated the distribution pattern on family level and the geographical as well as ecological factors that led to species persistence. rnThe study illuminated that the plant-pollinator interactions and the breeding system are adaptations to the fynbos biome but can not be defined as factors that drove speciation or have tremendous influence on distribution of Bruniaceae. In fact the geography of South Africa with its fragmented landscape as well as close niche-inhabitation of co-occuring species is the reason for species diversity and the recent distribution.rn