Papers

The first draft of a software architecture almost never constitutes the final picture of the system to be developed. In most cases it misses some of required properties and needs to be improved or even completely rebuilt. The software architect applies architec-tural transformations in order to repair the system structure. In this paper we present our approach to software architecture and architectural transformations. We also discuss three related issues: ADLs, architectural styles and non-functional requirements. Some arguments for architectural change automation are also given.

Architectural transformations make up the core of architectural design and play a crucial role in user requirements satisfaction. Because of their impact to software structure and behavior, they directly influence the values of software quality attributes. For this reason they can become not only a way for well specified and automated software architecture development but also a mechanism for early stage software quality management. This paper introduces the notion of architectural transformations and their impact to software architecture model. It points at the relationship among transformations, non-functional requirements and architectural styles. It gives the arguments for architectural change automation. A motivating example of how transformations can be employed to custom software architect activities is also given.

Model-driven engineering reaches more and more followers and gradually grows up as an incoming solution to the software-intensive systems production. Architectural modeling (or design) seems to play a fundamental role in this kind of development not only because of its very nature but also because of its impact to final product structure and behavior as well as user requirements satisfaction. Incremental and iterative character of architectural design sets a special attention to the aspects of architecture model restructuring, where architectural transformations are the key architect00D5s instrument for introducing quality dedicated changes. Since architectural designs constantly grow in complication because of systems complexity, there is a substantial need to support architect during model architectural transformations. This paper presents our efforts in defining model-level architectural transformations. It provides definition and classification of architectural transformations and describes the semantics of three selected transformations: for component moving, for component splitting and for class splitting. An example of employing the transformations to improve the architecture of an industrial WebGIS system is also given.

We present a translation from Fickle, a small object-oriented language allowing objects to change their class at run-time, into Java. The translation is provenly correct, in the sense that we have shown it to preserve the static and dynamic semantics. Moreover, it is compatible with separate compilation, since the translation of a Fickle class does not depend on the implementation of used classes. Based on the formal system, we have developed an implementation. The translation turned out to be a more subtle problem than we expected, and the proofs helped us uncover several subtle errors. In this paper, we discuss four different possible approaches we considered for the design of the translation and justify our choice, we present formally the translation and the proof of preservation of the static and dynamic semantics, and we discuss the prototype implementation. The language Fickle has undergone, and is still undergoing several phases of development. In this paper we are discussing the translation of Fickle_II.

We define a calculus for modeling dynamic linking independently of the details of a particular programming environment. The calculus distinguishes at the language level the notions of software configuration and execution, by introducing separate syntactic notions of linkset expression and command, respectively. A reduction step can be either a simplification of a linkset expression, or the execution of a command w.r.t. a specific underlying software configuration denoted by a linkset expression; because of dynamic linking, these two kinds of reductions are interleaved. The type system of the calculus, which is proved to be sound, relies on an accurate dependency analysis for ensuring type safety without losing the advantages offered by dynamic linking.

Modern programming environments such as those of Java and C# support dynamic loading of software fragments. More in general, we can expect that in the future systems will support more and more forms of interleaving of reconfiguration steps and standard execution steps, where the software fragments composing a program are dynamically changed and/or combined on demand and in different ways. However, existing kernel calculi providing formal foundations for module systems are based on a static view of module manipulation, in the sense that open code fragments can be flexibly combined together, but all module operators must be performed once for all before starting execution of a program, that is, evaluation of a module component. The definition of clean and powerful module calculi supporting lazy module operators, that is, operators which can be performed after the selection of some module component, is still an open problem. Here, we provide an example in this direction (the first at our knowledge), defining CMS^l, an extension of the Calculus of Module Systems [?] where module operators can be performed at execution time and, in particular, are executed on demand, that is, only when needed by the executing program. In other words, execution steps, if possible, take the precedence over reconfiguration steps. The type system of the calculus, which is proved to be sound, relies on a dependency analysis which ensures that execution will never try to access module components which cannot become available by performing reconfiguration steps.

We define a formal system supporting separate compilation for a small but significant Java-like language.

This system is proved to be stronger than the standard compilation of both Java and C#, in the sense that it better supports software reuse by avoiding unnecessary recompilation steps after code modification which are usually performed by using the standard compilers.

This is achieved by introducing the notion of local type assumption allowing the user to specify weaker requirements on the source fragments which need to be compiled in isolation.

Another important property satisfied by our system is compositionality, which corresponds to the intuition that if a set of fragments can be separately compiled and such fragments are compatible, then it is possible to compile all the fragments together as a unique program and obtain the same result.

We define a formal notion, called compilation schema, suitable for specifying different possibilities for performing the overall process of Java compilation, which includes typechecking of source fragments with generation of corresponding binary code, typechecking of binary fragments, extraction of type information from fragments and definition of dependencies among them. We consider three compilation schemata of interest for Java, that is, minimal, SDK and safe, which correspond to a minimal set of checks, the checks performed by the SDK implementation, and all the checks needed to prevent run-time linkage errors, respectively. In order to demonstrate our approach, we define a kernel model for Java separate compilation and execution, consisting in a small Java subset, and a simple corresponding binary language for which we provide an operational semantics including run-time verification. We define a safe compilation schema for this language and formally prove type safety.

We define a type system modeling true separate compilation for a small but significant Java subset, in the sense that a single class declaration can be intra-checked (following the Cardelli's terminology) and compiled providing a minimal set of type requirements on missing classes. These requirements are specified by a local type environment associated with each single class, while in the existing formal definitions of the Java type system classes are typed in a global type environment containing all the type information on a closed program. We also provide formal rules for static inter-checking and relate our approach with compilation of closed programs, by proving that we get the same results.

We present a translation from FickleII (a Java-like language allowing dynamic object re-classification, that is, objects that can change their class at run-time) into FickleII^- (the subset of FickleII that does not have the reclassification operation). The translation is proved to preserve static and dynamic semantics; moreover, it is shown to be effective, in the sense that the translation of a FickleII class does not depend on the implementation of used classes, hence can be done in a separate way, that is, without having their sources, exactly as it happens for Java compilation.

The contribution of the paper is twofold. First, we provide a general notion of type system supporting separate compilation and inter-checking, and a formal definition of soundess and completeness of inter-checking w.r.t. global compilation. These properties are important in practice since they allow selective recompilation. In particular, we show that they are guaranteed when the type system has principal typings and provides sound and complete entailment relation between type environments and types. The second contribution is more specific, and is an instantiation of the notion of type system previously defined for Featherweight Java [IgarashiEtAl@OOPSLA99] with method overloading and field hiding. The aim is to show that it is possible to define type systems for Java-like languages, which, differently from those used by standard compilers, have principal typings, hence can be used as a basis for selective recompilation.

Io is an experimental programming language designed for reflective programming. Io is inspired by Oberon, Modula-2, Pascal and C. Io has been designed as a tool for understanding the essence of reflection and for teaching reflective programming and its implementation mechanisms in under-graduate courses, thus Io is a very concise language. Nevertheless, Io is not a toy language: it is located at a mid distance between toys languages and production languages - despite its simplicity, it can be used for developing complex and modular programs that can be executed with a good efficiency. Io has been kept as simple as possible by discarding all those features neither implicitly nor explicitly connected with reflective programming.

Computational reflection provides the developers with a programming mechanism devoted to favorite code extensibility, reuse and maintenance. Notwithstanding that, it has not achieved developers' unanimous acceptance and its full potential yet. In our opinion, this depends on the intrinsic complexity of most of the reflective approaches that hinders their efficient implementation. The aim of this paper consists of defining the essence of reflection, that is, to identify the minimal set of characteristics that a software system must have to be considered reflective. The consequence is the realization of a run-time environment supporting the essence of reflection without affecting the programming language and with a minimal impact on the programming system design. This achievement will improve reflective system performances reducing the impact of one of the most diffuse criticism about reflection: low performance.

We adapt the ``aliasing constraints'' approach for designing a flexible typing of evolving objects. Types are singleton types (addresses of objects, as a matter of fact) whose relevance is mainly due to the sort of ``safety property'' they guarantee. In particular we provide a type system for an imperative object based calculus with delegation and which supports method and delegate overriding, addition, and removing.

We adapt the aliasing constraints approach for designing a flexible typing of evolving objects. Types are singleton types (addresses of objects, as a matter of fact) or finite unions of these. Their relevance is mainly due to the sort of safety property they guarantee. In particular we provide a type system for an imperative object based calculus with delegation and conditional expressions and which supports method and delegate overriding, addition, and removing.

We describe a coordination-oriented way of integrating semantic-based verification environments. Our approach is distributed, thereby moving the issue to the realm of coordination. To this end, we argue that tool integration, while not new, can be given a new life by applying the emerging paradigm of web services. We argue that web services can not only serve as a technological platform for our purposes but, indeed, also as a coordination framework, addressing all the basic issues present in the situation we are dealing with. We give an account of a prototype implementation of these concepts.

The quest for the formal certification of properties of security protocols is one of the most challenging research issues in the field of formal methods. It requires the development of formal models together with effective verification techniques, methods of detecting malicious behaviour, and so on and so forth. In this paper, we describes a formal methodology for verifying cryptographic protocols based on a symbolic state space exploration technique. We also present Aspasya, a semi-automatic verification tool based on our formal framework.

Resource control has attracted increasing interest in foundational research on distributed systems. This paper focuses on space control and develops an analysis of space usage in the context of an ambient-like calculus with bounded capacities and weighed processes, where migration and activation require space. A type system complements the dynamics of the calculus by providing static guarantees that the intended capacity bounds are preserved throughout the computation.

We address the problem of formal reasoning about mobile code. We consider an Ambient Calculus, where process syntax includes constructs for sequential programming. For the sake of concreteness, and because of practical relevance, we consider objects using message exchange to implement method invocation and overriding. The contribution of the paper is a type assignment system, obtained by combination of systems for MA and for the Sigma-calculus. We exploit in the mobility framework a typical feature of the intersection type discipline for object calculi, namely late typing of self. The proposed system is then checked against standard properties of related systems, establishing type invariance a completeness theorems.

Stack inspection is a basic mechanism for implementing language based security. Stack inspection is time consuming and may prevent from code optimization. A static analysis is presented that safely approximates the access rights granted at run-rime. Stack inspection optimizations are then possible, along with program transformations.

The paper focuses on stack inspection, a mechanism for the implementation of security-aware programming languages. We introduce a static analysis which safely approximates the set of access rights granted to code at run-time. This analysis allows for fast implementations of stack inspection based on an (hyper-) eager strategy.

The paper focuses on stack inspection, the access control mechanism implemented in Java and the CLR. We introduce a static analysis which safely approximates the set of access rights granted to code at run-time. This analysis provides us with the basis to reduce the run-time overhead of stack inspection, also in combination with other program transformations.

Mixins, i.e., classes parameterized over the superclass, can be the right mechanism for dynamically assembling class hierarchies with mobile code downloaded from different sources. In this paper we present the Java package momi that implements the concepts of the language momi, which is a calculus for exchanging mobile object-oriented code structured through mixin inheritance. This package can be thought of as an ``assembly'' language that should be the target of a compiler for a mobile code object-oriented language. In order to show an usage of the package, we illustrate how it is used by the compiler of X-Klaim, a programming language for mobile code where distributed processes can exchange classes and mixins through distributed tuple spaces.

This work presents an object-oriented calculus based on higher-order mixin construction via mixin composition, where some software engineering requirements are modeled in a formal setting allowing to prove the absence of message-not-understood run-time errors. Mixin composition is shown to be a valuable language feature enabling a cleaner object-oriented design and development. In what we believe being quite a general framework, we give directions for designing a programming language equipped with higher-order mixins, although our study is not based on any already existing object-oriented language.

We design a calculus that combines class-based features with object-based ones, with the aim of fitting into a unifying setting the ``best of both worlds''. In a mixin-based approach, mixins are seen incomplete classes from which incomplete objects can be instantiated. In turn, incomplete objects can be completed in an object-based fashion. Our hybrid calculus is shown to be useful in some real world scenarios that we present as examples.

Standard class-based inheritance mechanisms, which are often used to implement distributed systems, do not seem to scale well to a distributed context with mobility. In this paper, a mixin-based approach is proposed for structuring mobile object-oriented code and it is shown to fit in the dynamic and open nature of a mobile code scenario. We introduce MoMi (Mobile Mixins), a coordination language for mobile processes that communicate and exchange object-oriented code in a distributed context. MoMi is equipped with a type system, based on polymorphism by subtyping, in order to guarantee safe code communications.

MoMi (Mobile Mixins) is a coordination language for mobile processes that communicate and exchange object-oriented code in a distributed context. MoMi's key idea is structuring mobile object-oriented code by using mixin-based inheritance. Mobile code is compiled and typed locally, and can successfully interact with code present on foreign sites only if its type is subtyping-compliant with what is expected by the receiving site. In this paper, we study a subtyping relation for MoMi that includes both subtyping-in-width and subtyping-in-depth, in order to achieve a significantly more flexible, yet still simple, communication pattern. Technical problems arising from this extension are solved by a static annotation procedure.

This paper presents O'Klaim (Object-Oriented Klaim), a linguistic extension of the higher-order calculus for mobile processes Klaim with object-oriented features. Processes interact by an asynchronous communication model: they can distribute and retrieve resources, sometimes structured as incomplete classes, i.e., mixins, to and from distributed tuple spaces. This mechanism is coordinated by providing a subtyping relation on classes and mixins, which become polymorphic items during communication. We propose a static typing system for: (i) checking locally each process in its own locality; (ii) decorating object-oriented code that is sent to remote sites with its type. This way, tuples can be dynamically retrieved only if they match by subtyping with the expected type. If this pattern matching succeeds, the so retrieved code can be composed with local code, dynamically and automatically, in a type-safe way. Thus a global safety condition is guaranteed without requiring any additional information on the local reconfiguration of local and foreign code, and, in particular, without any further type checking. Finally, we present main issues concerning the implementation of O'Klaim.

Class inheritance and dynamic binding are the key features of object-oriented programming and they permit designing and developing complex systems. However, standard class inheritance is essentially static and cannot be directly employed for modeling dynamic object behaviors. In this paper we propose a linguistic extension of Java, called Dec-Java, that is partially inspired by the decorator design pattern. This extension permits easily separating the basic features of objects (that are likely not to change during the application) from their behaviors (that, instead, can be composed dynamically at run-time). Thus, Dec-Java enables a dynamic extension and specialization of object responsibilities.

The tuple space communication model, such as the one used in Linda, provides great flexibility for modeling concurrent, distributed and mobile processes. In a distributed setting with mobile agents, particular attention is needed for protecting sites and information. We have designed and developed a Java middleware, Klava, for implementing distributed tuple spaces and operations to support agent interaction and mobility. In this paper, we extend the Klava middleware with cryptographic primitives that enable encryption and decryption of tuple fields. We describe the actual implementation of the new primitives and provide a few examples. The proposed extension is general enough to be applied to similar Java frameworks using multiple distributed tuples spaces possibly dealing with mobility.

The wide-spreading of Internet has stimulated the introduction of new programming paradigms and languages that model interactions among hosts by means of mobile agents, and that are centered around the notions of location awareness. In this paper we show how to use formal tools, specifically a modal logic, for formalizing properties for mobile agent systems. We concentrate on one of these new languages, Klaim, and we use it to specify a system that permits maintaining the software installed on several heterogeneous computers distributed over a network by taking advantage of the mobile agent paradigm.

We describe a system that permits maintaining the software installed on several heterogeneous computers distributed over a network by taking advantage of the mobile agent paradigm. The applications are installed and updated only on the central server. When a new release of an application is installed on the server, agents are scattered along the network to update the application on the clients. To build a prototype system we use X-Klaim, a programming language specifically designed to program distributed systems composed of several components interacting through multiple tuple spaces and mobile code.

Highly distributed networks have now become a common infrastructure for a new kind of wide-area distributed applications whose key design principle is network awareness, namely the ability of dealing with dynamic changes of the network environment. Network-aware computing has called for new programming languages that exploit the mobility paradigm as a basic interaction mechanism. In this paper we present the architecture of Klava, an experimental Java package for distributed applications and code mobility. We explain how Klava implements code mobility by relying on Java and show a few distributed applications that exploit mobile code and are programmed in Klava.

The structure of open nets, like the Internet, is highly dynamic, as the topology of component networks continuously evolves. In this context, node connectivity is a key aspect and a language for distributed network-aware mobile applications should provide explicit mechanisms to handle it. In this paper, we address the problem of expressing dynamic changes of node connectivity at linguistic level and, in particular, we focus on a slight extension of the language Klaim, that is targeted to this aim. The extension consists of the introduction of a new category of processes that, in addition to the standard process operations, can execute a few new coordination operations for establishing new connections, accepting connection requests and removing connections. Our extension puts forward a clean separation between the coordinator level and the user level and, hence, it is modular enough to be easily applicable also to other network-aware languages. We will also show that our approach can be used as a guide for actual distributed (i.e. without a single centralized server) implementations of mobile systems.

A general framework for network aware programming is presented that consists of a language for programming mobile applications, a logic for specifying properties of the applications and an automatic tool for verifying such properties. The framework is based on XKlaim, eXtended Klaim, an experimental programming language specifically designed to program distributed systems composed of several components interacting through multiple tuple spaces and mobile code. The proposed logic is a modal logic inspired by Hennessy-Milner logic and is interpreted over the same labelled structures used for the operational semantics of XKlaim. The automatic verification tool is based on a complete proof system that has been previously developed for the logic.

When formalizing security protocols, different specification languages support very different reasoning methodologies, whose results are not directly or easily comparable. Therefore, establishing clear relationships among different frameworks is highly desirable, as it permits various methodologies to cooperate by interpreting theoretical and practical results of one system in another. In this paper, we examine the nontrivial relationship between two general verification frameworks: multiset rewriting (MSR) and a process algebra (PA) inspired to the CCS and the pi-calculus. We present two separate mappings, one from MSR to PA and the other from PA to MSR. Although defining a simple and general bijection between MSR and PA appears difficult, we show that in the specific context of cryptographic protocols they do admit effective translations that preserve traces.

In this paper, we examine the nontrivial relationship between two general verification frameworks: multiset rewriting (MSR) and a process algebra (PA) inspired to CCS and the -calculus. Although defining a simple and general bijection between MSR and PA appears difficult, we show that the sublanguages needed to specify a large class of cryptographic protocols (immediate decryption protocols) admits an effective translation that is not only bijective and trace-preserving, but also induces a weak form of bisimulation across the two languages. In particular, the correspondence sketched in this abstract permits transferring several important trace-based properties such as secrecy and many forms of authentication.

An integrity policy defines the situations when modification of information is authorized and is enforced by the security mechanisms of the system. However, in a complex application system it is possible that an integrity policy may have been incorrectly specified and, as a result, a user may be authorized to modify information that can lead to an unexpected system compromise. In this paper we outline a scalable and quantitative technique that uses constraint solving to model and analyze the effectiveness of application system integrity policies.

An integrity policy defines the situations when modification of information is authorized and is enforced by the security mechanisms of the system. However, in a complex application system it is possible that an integrity policy may have been incorrectly specified and, as a result, a user may be authorized to modify information that can lead to an unexpected system compromise. In this paper we propose a scalable and quantitative technique that uses constraint solving to model and analyze the effectiveness of application system integrity policies.

We study long-running transactions in open component-based distributed applications, such as Web Services platforms. Long-running transactions describe time-extensive activities that involve several distributed components. Henceforth, in case of failure, it is usually not possible to restore the initial state, and firing a compensation process is preferable. Despite the interest of such transactional mechanisms, a formal modeling of them is still lacking. In this paper we address this issue by designing an extension of the asynchronous pi-calculus with long-running transactions (and sequences) the pit-calculus. We study the practice of pit-calculus, by discussing few paradigmatic examples, and its theory, by defining a semantics and providing a correct encoding of pit-calculus into asynchronous pi-calculus.

In the object-oriented realm, class-based languages dominate the world of production languages, but object-based languages have been extensively studied to provide the foundations of the object-oriented paradigm. Moreover, object-based languages are undergoing a Renaissance thanks to the growing popularity of scripting languages, which are essentially object-based. We focus on extensible object-based calculi, which feature method addition, together with classical method override and method invocation. Extensible objects can be seen as a way to bridge the gap between the class-based setting and the pure object-based setting. Our aim is to provide a brief but rigorous view on extensible objects, following a thread suggested by the concept of ``self'' (which is the reference to the executing object) and its related typing problems. This tutorial may be seen as a complementary contribution to the literature which has explored and compared extensively pure object-based and class-based foundations (for example, as in the books by Abadi and Cardelli, and Bruce, respectively), but which generally neglected extensible objects.

We present a calculus for modelling ``environment-aware'' computations, that is computations that adapt their behaviour according to the capabilities of the environment. The calculus is an imperative, object-based language with extensible objects, equipped with a labelled transition semantics. A notion of bisimulation, lifting to computations a correspondence between the capabilities of different environments, is provided. Bisimulation can be used to prove that a program is ``cross-environment'', i.e., it has the same behaviour when run in different environments.

Finding typed encodings of object-oriented into procedural or functional programming sheds light on the theoretical foundations of object-oriented languages and their specific typing constructs and techniques. This paper describes a type preserving and computationally adequate interpretation of a full-fledged object calculus that supports message passing and constructs for object update and extension. The target theory is a higher-order lambda-calculus with records and recursive folds/unfolds, polymorphic and recursive types, and subtyping. The interpretation specializes to calculi of nonextensible objects, and validates the expected subtyping relationships.

This paper is devoted to a comprehensive study of polymorphic subtypes with products. We first present a sound and complete Hilbert style axiomatization of the relation of being a subtype in presence of ->, × type constructors and the for all quantifier, and we show that such axiomatization is not encodable in the system with , only. In order to give a logical semantics to such a subtyping relation, we propose a new form of a sequent which plays a key role in a natural deduction and a Gentzen style calculi. Interestingly enough, the sequent must have the form E|- T, where E is a non-commutative, non-empty sequence of typing assumptions and T is a finite binary tree of typing judgements, each of them behaving like a pushdown store. We study basic metamathematical properties of the two logical systems, such as subject reduction and cut elimination. Some decidability/undecidability issues related to the presented subtyping relation are also explored: as expected, the subtyping over ->,×,for all is undecidable, being already undecidable for the ->,for all fragment (as proved in a previous paper by J.Tiuryn), but for the ×,for all fragment it turns out to be decidable.

We refine the notion of embedding in order to obtain a formal tool for the comparison of the relative expressive power of different languages, by taking into account also the intended architectures on which the software components described using those languages are executed. The new notion, called architectural embedding, is suitable for the comparison of different communication mechanisms, and gives rise to a natural notion of implementability. We will use this notion to present equivalence and difference results for several coordination models based on components that communicate either through an unordered broadcast, through an atomic broadcast, or through a synchronous broadcast.

Fusion calculus is commonly regarded as a generalisation of pi-calculus. Actually, we prove that there is no uniform fully abstract embedding of pi-calculus into Fusion. This fact motivates the introduction of a new calculus, D-Fusion, with two binders, lambda and nu. We show that D-Fusion is strictly more expressive than both pi-calculus and Fusion. The expressiveness gap is further clarified by the existence of a fully abstract encoding of mixed guarded choice into the choice-free fragment of D-Fusion.

We study trace and may-testing equivalences in the asynchronous versions of CCS and pi-calculus. We start from the operational definition of the may-testing preorder and provide for it finitary and fully abstract trace-based characterizations, along with a complete in-equational proof system. We also touch upon two variants of this theory, by first considering a more demanding equivalence notion (must-testing) and then a richer version of asynchronous CCS. The results throw light on the difference between synchronous and asynchronous communication and on the weaker testing power of asynchronous observations.

Observational equivalences can be used to reason about the correctness of security protocols described in the spi-calculus. Unlike in CCS or in pi-calculus, these equivalences do not enjoy a simple formulation in spi-calculus. The present paper aims at enriching the set of tools for reasoning on processes by providing a few equational laws for a sensible notion of spi-bisimilarity. We discuss the difficulties underlying compositional reasoning in spi-calculus and show that, in some cases and with some care, the proposed laws can be used to build compositional proofs. A selection of these laws forms the basis of a proof system that we show to be sound and complete for the strong version of bisimilarity.

Recently there has been much interest towards using formal methods in the analysis of security protocols. Some recent approaches take advantage of concepts and techniques from the field of process calculi. Process calculi can be given a formal yet simple semantics, which permits rigorous definitions of such concepts as `attacker', `secrecy' and `authentication'. This feature has led to the development of solid reasoning methods and verification techniques, a few of which we outline in this paper.

Designing software by coordinating components is becoming a pervasive software development methodology. This practice of building (distributed) applications is currently supported by several industrial standards competing in the marketplace. Moreover, Internet facilitates the distributions of services to be embedded into applications. In this highly dynamic scenario, we discuss a methodology to formally describe the (behavioural) features of the single components and to reason about the properties of the assembled applications.

Component adaptation is widely recognised to be one of the crucial problems in Component-Based Software Engineering. We present a formal methodology for adapting components with mismatching interaction behaviours.

Available component-oriented platforms address software interoperability only at the signature level, while they do not provide suitable mechanisms for adapting components with mismatching interaction behaviour. This paper presents a methodology for automatically developing adaptors capable of solving behaviour mismatches between heterogeneous components. These adaptors are generated from abstract specifications of the intended connection between the components, by taking into account both signature interfaces and component behaviours.

We present a formal methodology for adapting components with mismatching interaction behaviour.

Component adaptation is widely recognised to be one of the crucial problems in Component-Based Software Engineering (CBSE). We present a formal methodology for adapting components with mismatching interaction behaviour. The three main ingredients of the methodology are: (1) The inclusion of behaviour specifications in component interfaces, (2) a simple, high-level notation for expressing adaptor specifications, and (3) a fully automated procedure to derive concrete adaptors from given high-level specifications.

We study the expressiveness of the most prominent representatives of the family of shared dataspace coordination languages, namely Linda, Gamma and Concurrent Constraint Programming. The investigation is carried out by exploiting and integrating three different comparison techniques: weak and strong modular embedding and property-preserving encodings. We obtain a hierarchy of coordination languages that provides useful insights for both the design and the use of coordination languages.

The problem of adapting heterogeneous software components that present mismatching interaction behaviour is one of the crucial problems in Component-Based Software Engineering. The aim of this paper is to contribute to setting a theoretical foundation for software adaptation. A formal analysis of adaptor specifications is presented, and their usage to feature different forms of flexible adaptations is illustrated.

Component adaptation is widely recognised to be one of the crucial problems in Component-Based Software Engineering (CBSE). We present here a formal methodology for the soft adaptation of components presenting mismatching interaction behaviours. The notions of access rights (associating components with the services they are allowed to use) and subservicing (providing alternative services in place of those requested by components lacking the required access rights) are exploited to feature a secure and flexible adaptation of third-party components.

Adapting heterogeneous software components that present mismatching interaction behaviour is one of the crucial problems in Component-Based Software Engineering. The process of component adaptation can be synthesized by a transformation from an initial specification (of the requested adaptation) to a revised specification (expressing the actual adaptation that will be featured by the deployed adaptor component). An important capability in this context is hence to be able to evaluate to which extent an adaptor proposal satisfies the initially requested adaptation. The aim of this paper is precisely to develop different metrics that can be employed to this end. Such metrics can be fruitfully employed both to assess the acceptability of an adaptation proposal, and to compare different adaptation solutions proposed by different servers.

Component-Based Software Development is an emerging discipline in the field of Software Engineering. When constructing component-based systems, we must be sure that the cooperative behaviour of the components and their interaction will be successful. In this paper, we use Linda to specify the interactive behaviour of software components. To do this, we first introduce a process algebra for Linda, and then we define a compatibility relation providing conditions that ensure safe composition. This relation takes into account the state of a shared tuple space which represents the current execution. Indeed, a Linda-based computation is characterized by the store2019s evolution, so that the set of tuples included into the store governs each computation step. In this context, the success of the composition of a pair of agents in presence of a suitable store can be useful to condition the acceptance of a given component into an open running system. In order to extend our approach to complex systems, where constructing a system involves more than two components, we propose the use of distributed tuple spaces as the glue to join components. Keywords: Coordination languages, components, software architecture, compatibility, interaction, process algebras.

We discuss the principles of distributed transactions, then we define an operational model which meets the basic requirements and we give a prototyping implementation for it in join-calculus. Our model: (1) extends BizTalk with multiway transactions; (2) exploits an original algorithm, for distributed commit; (3) can deal with dynamically changing communication topology; (4) is almost language-independent. In fact, the model is based on a two-level classification of resources, which should be easily conveyed to distributed calculi and languages, providing them with a uniform transactional mechanism.

In this paper we survey and discuss a number of coordination models for agents. We define a framework general enough to be able to capture the main ideas underlying the major coordination models for agents. The framework is based on three key concepts: the coordinables, the coordination medium, and the coordination rules. We start modeling a simple dataspace-based model. Then we structure our discussion along three directions: more advanced coordination primitives exploitable by the coordinables, reshaping the coordination medium, and programming the coordination rules.

We investigate the expressive power of two alternative approaches used to express infinite behaviours in process calculi, namely, replication and recursive definitions. These two approaches are equivalent in the full pi-calculus, while there is a common agreement that this is not the case when name mobility is not allowed (as in the case of CCS), even if no formal discriminating We consider a hierarchy of calculi, previously proposed by Sangiorgi, that spans from a fragment of CCS (named ``the core of CCS'') to the pi-calculus with internal mobility. We prove the following discrimination result between replication and recursive definitions: the termination of processes is an undecidable property in the core of CCS, provided that recursive process definitions are allowed, while termination turns out to be decidable when only replication is permitted. On the other hand, this discrimination result does not hold any longer when we move to the next calculus in the hierarchy, which supports a very limited form of name mobility.

In this paper we initiate an investigation about security problems which occur when exploiting a Linda-like data driven coordination model in an open environment. In this scenario, there is no guarantee that all the agents accessing the shared tuple space are trusted. Starting from the analysis of the few proposals already available in the literature, we present a novel coordination model which provides mechanisms to manage tuple access control. The first mechanism supports logical partitions of the shared repository: in this way we can restrict the access to tuples inside a partition, simply by limiting the access to the partition itself. The second mechanism consists of adding to the tuples some extra information which exploit asymmetric cryptography in order, e.g., to authenticate the producer of a tuple or to identify its reader/consumer. Finally, we support the possibility to define access control policies based on the kind of operations an agent performs on a tuple, thus discriminating between (destructive) input and (non-destructive) read operations.

The shared dataspace metaphor is historically the most prominent representative of the family of coordination models. According to this approach, concurrent processes interact via the production, consumption, and test for presence/absence of data in a common repository. Recently, the problem of the accumulation of outdated and unwanted information in the shared repository has been addressed and it has been solved by introducing non-permanent data, obtained by associating an expiration time to data. In this paper we investigate the impact of the adoption of different notions of non-permanent data on the expressiveness of a Linda based process calculus.

Shared dataspaces, initiated by Linda since the beginning of the 80s, has been successfully adopted as a coordination model in a huge variety of systems and applications, going from parallel computing to web-based collaborative work. We point out several scalability problems which arise when trying to exploit the original Linda coordination model in peer-to-peer systems. The objective of this analysis is to produce some guidelines for the design of a data-driven coordination infrastructure suitable for the peer-to-peer scenario.

Shared dataspaces a` la Linda, and the underlying data-driven coordination model, have been successfully exploited in the development of a huge variety of applications, going from parallel computing to web-based collaborative work. In this paper we consider a novel class of applications, namely those developed for peer-to-peer networks a` la Gnutella or FreeNet. We discuss the problems which arise when trying to exploit the original Linda coordination model in this new scenario. In order to address these problems, we introduce PeerSpaces, a new coordination model particularly suited for the realm of peer-to-peer network applications, and we present a prototypical implementation of this coordination model based on the JXTA peer-to-peer technology.

The traditional Linda programming style, based on the introduction and consumption of data from a common repository, seems not adequate for highly dynamic applications in which it is important to observe modification of the environment which occur quickly. On the other hand, reactive programming seems more appropriate for this kind of applications. In this paper we consider some approaches recently presented in the literature for embedding reactive programming in shared dataspaces, we present a possible classification for these approaches, and we perform a rigorous investigation of their relative advantages and disadvantages

JavaSpaces is a coordination infrastructure inspired by the shared dataspace model: processes interact by introducing, consuming, and testing for the presence/absence of data in a common repository. Besides these traditional operations, an event based coordination mechanism is considered which allows for the notification of the introduction of new instances of data in the repository. JavaSpaces also supports transactions: multiple coordination operations can be grouped into a bundle that acts as a single atomic operation. In this paper we adopt serializability as a criterion to evaluate the correctness of the JavaSpaces transaction semantics: we prove that serializability is satisfied only if we restrict to output, input, and read operations. On the other hand, in the presence of either test for absence or event notification, serializability is not satisfied; we propose an alternative semantics and we prove that it supports serializability.

Two main architectural styles emerged in the panorama of inter-agent coordination infrastructures: the publish/subscribe model, according to which agents communicate via the raising and catch of events, and the shared-dataspace (i.e. Linda-like) approach, in which communication is achieved by introducing and consuming objects from a common repository. In this paper we perform a rigorous comparison of the two approaches with a particular emphasis on their interchangeability; we obtain the following results: (i) the shared dataspace model can be reduced to the publish/subscribe architecture, while (ii) the vice versa holds only if a global coordination operation, such as copy-collect or inp, is provided among the shared dataspace operations.

Transiently Shared Dataspaces (TSD), recently introduced in the coordination infrastructure Lime, represent an emerging technology to enable the use of dataspaces for the coordination of mobile agents: data-sharing is allowed among agents running on hosts belonging to the same federation (i.e., currently connected). In this paper we present a formalization of the TSD technology in order to provide a framework for reasoning about systems based on this infrastructure. In particular, we concentrate on alternative design choices related to data migration, host connectivity, and reactive programming.

Pure Mobile Ambients (i.e., Mobile Ambients without communication) provides three mobility primitives: in and out for ambient movement, and open to dissolve ambient boundaries. In this paper we consider the expressiveness of the primitives in and out for ambient movement; more precisely, we concentrate on the interplay between ambient movement and the ability to create new names (exploiting the restriction operator). To this aim, we consider a version of Pure Mobile Ambients (with explicit recursive definitions instead of replication) and we concentrate on the three fragments of the calculus that can be obtained removing either one or both between movement and the ability to create new names. The unique mobility primitive that we retain in all of the considered calculi is open. Te three fragments are denoted as follows: MAmv without ambient movement, MAnew without restriction, and MAmvnew without both movement and restriction. We prove that both the fragments MAmv and MAnew are Turing-complete, while this is not the case for MAmvnew. Indeed, we prove that in this latter calculus the existence of an infinite computation turns to be a decidable property.

Several coordination platforms based on the shared dataspace approach introduces, besides the typical Linda-like coordination primitives (used to produce, consume, and test for the presence/absence of data in a common repository), a transaction mechanism provided to group coordination primitives which should be executed in such a way that either all succeed or none of them is performed. In this paper we continue the investigation of the serializability of transactions in shared dataspace coordination languages. The new contribution consists of the analysis of the interplay between transactions and temporary data, ie., data with an associated expiration time.

The shared dataspace metaphor is historically the most prominent representative of the family of coordination models. According to this approach, concurrent processes interact via the production, consumption, and test for presence/absence of data in a common repository. Recently, the problem of the accumulation of outdated and unwanted information in the shared repository has been addressed. Typical garbage collection algorithms cannot be adopted in this context because there is no notion of unaccessible data. The most promising solution to this problem consists of the introduction of the notion of temporary data, intended as data with an associated expiration time. In this paper, we investigate the impact of different mechanisms for expired data collection on the expressiveness of shared dataspace coordination systems with temporary data.

This paper addresses the issue of safely combining computational effects and multi-stage programming. We propose a type system, which exploits a notion of closed type, to check statically that an imperative multi-stage program does not cause run-time errors. Our approach is demonstrated formally for a core language called MiniML_ref^meta. This core language safely combines multi-stage constructs and ML-style references, and is a conservative extension of MiniML_ref, a simple imperative subset of SML. In previous work, we introduced a closed type constructor, which was enough to ensure the safe execution of dynamically generated code in the pure fragment of MiniML_ref^meta.

This paper addresses the issue of safely combining computational effects and multi-stage programming. We propose a type system, which exploits a notion of closed type, to check statically that an imperative multi-stage program does not cause run-time errors. Our approach is demonstrated formally for a core language called MiniML_ref^meta. This core language safely combines multi-stage constructs and ML-style references, and is a conservative extension of MiniML_ref, a simple imperative subset of SML. In previous work, we introduced a closed type constructor, which was enough to ensure the safe execution of dynamically generated code in the pure fragment of MiniML_ref^meta.

Environment classifiers were recently proposed as a new approach to typing multi-stage languages. Safety was established in the simply-typed and let-polymorphic settings. While the motivation for the classifier approach was the feasibility of inference, this was in fact not established. This paper starts with the observation that inference for the full classifier-based system fails. We then identify a subset of the original system for which inference is possible. This subset, which uses implicit classifiers, retains significant expressivity (e.g. it can embed the calculi of Davies and Pfenning) and eliminates the need for classifier names in terms. Implicit classifiers were implemented in MetaOCaml, and no changes were needed to make an existing test suite acceptable by the new type checker.

The main objective of remote-method-invocation- and object-based middleware is to provide a convenient environment for the realization of distributed computations. In most cases, unfortunately, interaction policies in these middleware platforms are hardwired into the platform itself. Some platforms, e.g., CORBA?s interceptors, offer means to redefine such details but their flexibility is limited to the possibilities that the designer has foreseen.

In this way, distributed algorithms must be exclusively embedded in the application code, breaking any separation of concerns between functional and nonfunctional code. Some programming languages like Java disguise remote interactions as local calls, thus rendering their presence transparent to the programmer. However their management is not so transparent and easily maskable to the programmer.

The classical remote method invocation (RMI) mechanism adopted by several objectbased middleware is `black-box' in nature, and the RMI functionality, i.e., the RMI interaction policy and its configuration, is hard-coded into the application. This RMI nature hinders software development and reuse, forcing the programmer to focus on communication details often marginal to the application being developed. Extending the RMI behavior with extra functionality is also a very difficult job, because added code must be scattered among the entities involved in communications.

This situation could be improved by developing the system in several separate layers, confining communications and related matters to specific layers. As demonstrated by recent work on reflective middleware, reflection represents a powerful tool for realizing such a separation and therefore overcoming the problems referred to above. Such an approach improves the separation of concerns between the communicationrelated algorithms and the functional aspects of an application. However, communications and all related concerns are not managed as a single unit that is separate from the rest of the application, which makes their reuse, extension, and management difficult. As a consequence, communications concerns continue to be scattered across the meta-program, communication mechanisms continue to be black-box in nature, and there is only limited opportunity to adjust communication policies through configuration interfaces.

In this paper we examine the issues raised above, and propose a reflective approach specially designed to open up the RMI mechanism. Our proposal consists of a new reflective model, called multichannel reification, that reflects on and reifies communication channels, i.e., it renders communication channels firstclass citizens. This model is designed both for developing new communication mechanisms and for extending the behavior of communication mechanisms provided by the underlying system. Our approach is embodied in a framework called , which is described in detail in this paper.

In this paper we describe how to realize a Java RMI framework supporting multi-point method invocation. The package we have realized allows programmers to build groups of servers that could provide services in two different modes: fault tolerant and parallel. These modes differ over computations failure. Our extension is based upon the creation of entities which maintain a common state between different servers. This has been done extending the existing RMI registry. From the user's point of view the multi-point RMI acts just like the traditional RMI system, and really the same architecture has been used.

In this paper we show how to enhancing the Java RMI framework to support object groups. The package we have developed allows programmers to dynamically deal with groups of servers all implementing the same interface. Our group mechanism can be used both to improve reliability preventing system failures and to implement processor farm parallelism. Each service request dispatched to an object group returns all the values computed by the group members permitting the implementation of both kind of applications. Moreover, these approaches differ both over computations failure and over the semantic of the implemented interface. Our extension is achieved enriching the classic RMI framework and the existing RMI registry with new functionalities. From user's point of view the multicast RMI acts just like the traditional RMI system, and really the same architecture has been used.

Today, complex information systems need a simple way for changing the object behavior according with changes that occur in its running environment. We present a reflective architecture which provides the ability to change object behavior at run-time by using design-time information. By integrating reflection with design patterns we get a flexible and easily adaptable architecture. A reflective approach that describes object model, scenarios and statecharts helps to dynamically adapt the software system to environmental changes. The object model, system scenario and many other design information are reified by special meta-objects, named evolutionary meta-objects. Evolutionary meta-objects deal with two types of run-time evolution. Structural evolution is carried out by causal connection between evolutionary meta-objects and its referents through changing the structure of these referents by adding or removing objects or relations. Behavioral evolution allows the system to dynamically adapt its behavior to environment changes by itself. Evolutionary meta-objects react to environment changes for adapting the information they have reified and steering the system evolution. They provide a natural liaison between design information and the system based on such information. This paper describes how this liaison can be built and how it can be used for adapting a running system to environment changes.

In this paper we present a proposal for safely evolving a software system against run-time changes. This proposal is based on a reflective architecture which provides objects with the ability of dynamically changing their behavior by using their design information. The meta-level system of the proposed architecture supervises the evolution of the software system to be adapted that runs as the base-level system of the reflective architecture. The meta-level system is composed of cooperating components; these components carry out the evolution against sudden and unexpected environmental changes on a reification of the design information (e.g., object models, scenarios and statecharts) of the system to be adapted. The evolution takes place in two steps: first a meta-object, called evolutionary meta-object, plans a possible evolution against the detected event then another meta-object, called consistency checker meta-object validates the feasibility of the proposed plan before really evolving the system. Meta-objects use the system design information to govern the evolution of the base-level system. Moreover, we show our architecture at work on a case study.

The fragment of pattern language proposed in this paper, shows how to adapt a nonstoppable software system to reflect changes in its running environment. These framework patterns depend on well-known techniques for programs to dynamically analyze and modify their own structure, commonly called computational reflection. Our patterns go together with common reflective software architectures.

Aim of this paper is to develop a filter model for a calculus with mobility and higher-order value passing. We will define it for an extension of the Ambient Calculus in which processes can be passed as values. This model turns out to be fully abstract with respect to the notion of contextual equivalence where the observables are ambients at top level.

We present an ambient-like calculus in which the open capability is dropped, and a new form of ``lightweight process mobility is introduced. The calculus comes equipped with a type system which allows the kind of values exchanged in communications and the access and mobility properties of processes to be controlled. A type inference procedure determines the ``minimal requirements to accept a system or a component as well typed. This gives a kind of principal type. As an expressiviness test, we show that some of the most known calculi of concurrency and mobility can be encoded in our calculus in a natural way.

We introduce a rank 2 intersection type system with new typing rules for local definitions (LET-expressions and LETREC-expressions) and conditional expressions (IF-expressions and MATCH-expressions). This is a further step towards the use of intersection types in ``real'' programming languages. The technique for typing local definitions relies entirely on the principal typing property (i.e. it does not depend on particulars of rank 2 typing), so it can be applied to any system with principal typings. The technique for typing conditional expressions, which is based on the idea of introducing metrics on types to ``limit the use'' of the intersection type constructor in the types assigned to the branches of the conditionals, is instead tailored to rank 2 intersection. However, the underlying idea might be useful also for other type systems.

We present a rank 2 intersection type system for a language of modules built on a core ML-like language. The principal typing property of the rank 2 intersection type system for the core language plays a crucial role in the design of the type system for the module language. We first considers a ``plain'' notion of module, where a module is just a set of mutually recursive top-level definitions, and illustrates the notions of: module intrachecking (each module is typechecked in isolation and its interface, that is the set of typings of the defined identifiers, is inferred); interface interchecking (when linking modules, typechecking is done just by looking at the interfaces); interface specialization (interface intrachecking may require to specialize the typing listed in the interfaces); principal interfaces (the principal typing property for the type system of modules); and separate typechecking (looking at the code of the modules does not provide more type information than looking at their interfaces). Then we illustrate some limitations of the ``plain'' framework and extend the module language and the type system in order to overcome these limitations. The decidability of the system is shown by providing algorithms for the fundamental operations involved in module intrachecking and interface interchecking.

Re-classification changes at run-time the class membership of an object while retaining its identity. In our previous work on the language Fickle (and its extension FickleI and FickleII) we suggested language features for object re-classification, which could extend an imperative,typed, class-based, object-oriented language. In this paper we present the language FickleIII, which improves FicleII with a more expressive type and effect system. FickleIII allows to correctly type meaningful programs which FickleII reject. This is done by taking into account the initial and the final class of each re-classification. The syntax of FickleIII and the syntax of FickleII differ only in the effect annotations occurring in methods' signatures (every FickleII-style effect annotation can be coded into a FickleIII-style effect annotation, but not vice versa). The operational semantics (which ignores effect annotations) is unchanged.

In previous work with Dezani on the language Fickle and its extension FickleII we introduced language features for object re-classification for imperative, typed, class-based, object-oriented languages. In this paper we present the language Fickle3, which on one side refines FickleII with more expressive effect annotations, and on the other eliminates the need to declare explicitly which are the classes of the objects that may be re-classified. Therefore, Ficle3 allows to correctly type meaningful programs which FickleII rejects. Moreover, re-classification may be decided by the client of a class, allowing ``unanticipated object re-classification''. As for FickleII, also the type and effect system for Fickle3 guarantees that, even though objects may be re-classified across classes with different members, they will never attempt to access non existing members. The type and effect system of Fickle3 has some significant differences from the one of FickleII. In particular, besides the fact that intra-class type checking has to track the more refined effects, when a class is combined with other classes some additional inter-class checking is introduced.

In previous work we introduced a calculus for modelling ``environment-aware'' computations, that is computations that adapt their behavior according to the capabilities of the environment. The calculus is an imperative, object-based language (with extensible objects and primitives for discriminating the presence or absence of attributes of objects) equipped with a small-step operational semantics. In this paper we define a type and effect system for the calculus. The typing judgements specify, via constraints, the shape of environments which guarantees the correct execution of expressions and the typing rules track the effect of expression evaluation on the environment. The type and effect system is sound w.r.t. the operational semantics of the language.

In this paper we consider re-classification in the presence of multi-threading. To this aim we define a multi-threaded extension of the language Fickle, that we call Fickle_MT. We define an operational semantics and a type and effect system for the language. Each method signature carries the information on the possible effects of the method execution. The type and effect system statically checks this information. The operational semantics uses this information in order to delay the execution of some threads when this could cause ``messageNotUnderstood errors. We prove that in the execution of a well-typed expression such delays do not produce deadlock.

The explicit management of Quality of Service (QoS) of network connectivity, such as, e.g., working cost, transaction support, and security, is a key requirement for the development of the novel wide area network applications. In this paper, we introduce a foundational model for specification of QoS attributes at application level. The model handles QoS attributes as semantic constraints within a graphical calculus for mobility. In our approach QoS attributes are related to the programming abstractions and are exploited to select, configure and dynamically modify the underlying system oriented QoS mechanisms.

Klaim is an experimental programming language that supports a programming paradigm where both processes and data can be moved across different computing environments. The language relies on the use of explicit localities, and on allocation environments that associate logical localities to physical sites. This paper presents a temporal logic for specifying properties of Klaim programs. The logic is inspired by Hennessy-Milner Logic (HML) and the mu-calculus, but has novel features that permit dealing with state properties to describe the effect of actions over the different sites. The logic is equipped with a consistent and complete proof system that enables one to prove properites of mobile systems.

Many real life optimization problems contain both hard and soft constraints, as well as qualitative conditional preferences. However, there is no single formalism to specify all three kinds of information. We therefore propose a framework, based on both CP-nets and soft constraints, that handles both hard and soft constraints as well as conditional preferences efficiently and uniformly. We study the complexity of testing the consistency of preference statements, and show how soft constraints can faithfully approximate the semantics of conditional preference statements whilst improving the computational complexity.

Re-classification changes at run-time the class membership of an object while retaining its identity. We suggest language features for object re-classification, which could extend an imperative, typed, class-based, object-oriented language. We present our proposal through the language Fickle (Fickle is the successor of an earlier proposal, Fickle-99; although both Fickle and Fickle-99 address the same requirement for object re-classification, the approaches are very different). The imperative features combined with the requirement for a static and safe type system provided the main challenges. We develop a type and effect system for Fickle and prove its soundness with respect to the operational semantics. In particular, even though objects may be re-classified across classes with different members, they will never attempt to access non-existing members.

Dynamic linking supports flexible code deployment: partially linked code links further code on the fly, as needed; and thus, end-users receive updates automatically. On the down side, each program run may link different versions of the same code, possibly causing subtle errors which mystify end-users. Dynamic linking in Java and C# are similar: The same linking phases are involved, soundness is based on similar ideas, and executions which do not throw linking errors give the same result. They are, however, not identical: the linking phases are combined differently, and take place in different order. Thus, linking errors may be detected at different times in Java and C#. We develop a non-deterministic model, which includes the behaviour of Java and C#. The non-determinism allows us to describe the design space, to distill the similarities between the two languages, and to use one proof of soundness for both. We also prove that all execution strategies are equivalent in the sense that all terminating executions which do not involve a link error, give the same result.

Conditions on type preorders are provided in order to precisely characterize intersection type-induced models for the Lambda-calculus and some of its restrictions. Besides, two examples are given of filter models in which not all the continuous functions are representable.

In a recent paper we proposed a calculus for modeling dynamic linking independently of the details of a particular programming environment. Here we use a particular instantiation of this calculus to encode a toy language, called MCS, which provides an abstract view of the mechanism of dynamic class loading with multiple loaders as in Java. The aim is twofold. On one hand, we show an example of application of the calculus in modeling existing loading and linking policies, showing in particular that Java-like loading with multiple loaders can be encoded without exploiting the full expressive power of the calculus. On the other hand, we provide a simple formal model which allows a better understanding of Java-like loading mechanisms and also shows an intermediate solution between the rigid approach based only on the class path and that which allows arbitrary user-defined loaders, which can be intricate and error-prone.

This paper presents a semantic-based environment for reasoning about the behaviour of mobile systems. The verification environment, called HAL, exploits a novel automata-like model which allows finite state verification of systems specified in the pi-calculus. The HAL system is able to interface with several efficient toolkits (e.g. model checkers) to determine whether or not certain properties hold for a given specification. We report experimental results on some illustrative case studies.

Web services allow the components of applications to be highly decentralized, dynamically reconfigurable. Moreover, Web services can interoperate easily inside an heterogeneous network environment. The vast majority of current available verification environments have been built by sticking to traditional architectural styles. Hence, they are centralized and none of them deal with interoperability and dynamic reconfigurability. In this paper we present a verification toolkit whose design and implementation exploit the Web service architectural paradigm. We describe the architectural design and the discuss in detail the current implementation efforts.

This paper describes the design and the semantics of MetaKlaim, an higher order distributed process calculus equipped with staging mechanisms. MetaKlaim integrates MetaML (an extension of SML for multi-stage programming) and Klaim (a Kernel Language for Agents Interaction and Mobility), to permit interleaving of meta-programming activities (like assembly and linking of code fragments), dynamic checking of security policies at administrative boundaries and ``traditional'' computational activities on a wide area network (like remote communication and code mobility). MetaKlaim exploits a powerful type system (including polymorphic types á la system F) to deal with highly parameterized mobile components and to dynamically enforce security policies: types are metadata which are extracted from code at run-time and are used to express trustiness guarantees. The dynamic type checking ensures that the trustiness guarantees of wide are network applications are maintained whenever computations interoperate with potentially untrusted components.

This paper describes the design and the semantics of MetaKlaim, an higher order distributed process calculus equipped with staging mechanisms. MetaKlaim integrates MetaML (an extension of SML for multi-stage programming) and Klaim (a Kernel Language for Agents Interaction and Mobility), to permit interleaving of meta-programming activities (like assembly and linking of code fragments), dynamic checking of security policies at administrative boundaries and ``traditional'' computational activities on a wide area network (like remote communication and code mobility). MetaKlaim exploits a powerful type system (including polymorphic types a la system F) to deal with highly parameterized mobile components and to dynamically enforce security policies: types are metadata which are extracted from code at run-time and are used to express trustiness guarantees. The dynamic type checking ensures that the trustiness guarantees of wide are network applications are maintained whenever computations interoperate with potentially untrusted components.

This paper describes the architecture of a toolkit, called Mihda, providing facilities to minimise labelled transition systems for name passing calculi. The structure of the toolkit is derived from the co-algebraic formulation of the partition-refinement minimisation algorithm for HD-automata. HD-automata have been specifically designed to allocate and garbage collect names and they provide faithful finite state representations of the behaviours of pi-calculus processes. The direct correspondence between the coalgebraic specification and the implementation structure facilitates the proof of correctness of the implementation. We evaluate the usefulness of Mihda in practise by performing finite state verification of pi-calculus specifications of network applications.

In the Mobile Ambients of Cardelli and Gordon an ambient is a unit for mobility, which may contain processes (data) and sub-ambients. Since the seminal work of Cardelli and Gordon, several ambient-based calculi have been proposed (Seal, Box-Pi, Safe Ambients, Secure Safe Ambients, Boxed Ambients), mainly for supporting security. At the operational level these (box- and) ambient-based calculi differ only in the capabilities of processes. We propose a way of extending ambient-based calculi, which embodies two principles: an ambient is a unit for monitoring and coordination, the name of an ambient determines its (monitoring and coordination) policy. More specifically, to each ambient we attach a guardian, which monitors the activity of sub-components (i.e. processes and sub-ambients) and the interaction with the external environment. In our proposal, guardians and processes play a dual role: guardians are centralized entities monitoring and inhibiting actions, while processes are decentralized entities performing actions. We exemplify the use of guardians for enforcing security properties.

Graphical notations have been widely accepted as an expressive and intuitive working tool for system specification and design. This paper outlines a declarative approach based on (hyper-)graphs and graph synchronization to deal with the modeling of Wide Area Network applications. This paper aims at contributing to the understanding of crucial issues involved in the specification and design of Wide Area Network systems, as a first step toward the development of software engineering techniques and tools for designing and certificating internetworking systems.

In this paper, we study the relations among three aspects in the context of a multi-agent meeting scheduling system: efficiency, privacy loss, and solution quality. We do this by first implementing a multi-agent system that incorporates preferences, and then by running experiments to capture the interesting and useful trade-offs among these three aspects.

We consider multi-agent systems with preferences, which are just standard multi-agent systems, except that each agent can set some preferences over its local data. This makes these systems more flexible and realistic, since it is possible to represent possibilities, costs, probabilities, preferences, and penalties. However, it also transforms the search for a feasible solution into the search for an optimal, or good enough, solution, since the use of preferences naturally implies the adoption of an optimization criterion, both for each agent and also for the system as a whole. Thus solution quality becomes an important aspect of such systems. Moreover, each agent may want to keep its information as private as possible. Thus privacy loss is another important aspect of such systems. Finally, an obvious crucial aspect is efficiency, since we would like to find a good solution as quickly as possible. In this paper, we study the relations among these three aspects in the context of a multi-agent meeting scheduling system. We do this by first implementing a multi-agent system that incorporates preferences, and then by running experiments to capture the interesting and useful trade-offs among these three aspects.

We consider configuration problems with preferences rather than just hard constraints, and we analyze and discuss the features that such configurators should have. In particular, these configurators should provide explanations for the current state, implications of a future choice, and also information about the quality of future solutions, all with the aim of guiding the user in the process of making the right choices to obtain a good solution. We then describe our implemented system, which, by taking the soft n-queens problem as an example, shows that it is indeed possible, even in this very general context of preference-based configurators, to automatically compute all the information needed for the desired features. This is done by keeping track of the inferences that are made during the constraint propagation enforcing phases. However, the process of recording the necessary information is more complex and expensive than in the case of hard constraints, since in general a sequence of previous choices has to be recorded for each possible future choice, and not just one as in the case of hard constraints.

We present a new model for the distributed implementation of pi-like calculi, which permits strong correctness results that are simple to prove. We describe the distributed channel machine - a distributed version of a machine proposed by Cardelli. The distributed channel machine groups pi processes at their channels (or locations), in contrast with the more common approach of incorporating additional location information within pi processes. We go on to describe the fusion machine. It uses a form of concurrent constraints called fusions - equations on channel names - to distribute fragments of these processes between remote channels. This fragmentation avoids the movement of large continuations between locations, and leads to a more efficient implementation model.

A linear forwarder is a process which receives one message on a channel and sends it on a different channel. Linear forwarders constitute a basic and implementable atom of input capability, by which arbitrary input capability can be encoded. (Input capability is where a received name is used as the subject of subsequent input). In earlier work, the Join calculus eliminated all input capability with a view to making itself implemental. The significance of the current work is that this elimination was not necessary. Linear forwarders have `clean' behaviour in the presence of failure, they allow an elegant encoding of distributed choice, and they yield full abstraction with the pi calculus with respect to barbed congruence.

A tutorial introduction to the key concepts of ambient calculi and their type disciplines, illustrated through a number of systems proposed in the last few years, such as Mobile Ambients, Safe Ambients, Boxed Ambients, and other related calculi with types.

The type system for the ambient calculus M³ is presented in a new form that derives the type of a term with the minimal set of mobility assumptions, and is therefore more amenable than the original form to a translation into a type inference algorithm. From the new formulation a Prolog program is derived, which implements a type inference algorithm for M³ analogous to the one previously specified through formal rules. The implementation exploits in the standard way the peculiarities of the logic programming paradigm, and is therefore, in a sense, more abstract than the original algorithm's specification itself.

Security is a key issue for distributed systems/applications with code mobility, like, e.g., e-commerce and on-line bank transactions. In a scenario with code mobility, traditional solutions based on cryptography cannot deal with all security issues and additional mechanisms are necessary. In this paper, we present a flexible and expressive type system for security for a calculus of distributed and mobile processes. The type system has been designed to supply real systems security features, like the assignment of different privileges to users over different data/resources. Type soundness is guaranteed by using a combination of static and dynamic checks, thus enforcing specific security policies on the use of resources. The usefulness of our approach is shown by modeling the simplified behaviour of a bank account management system.

muKlaim is a process language that permits programming distributed systems made up of several mobile components interacting through multiple distributed tuple spaces. We present the language and a type system for controlling the activities, e.g. access to resources and mobility, of the processes in a net. By dealing with privileges acquisition, the type system enables dynamic variations of security policies. We exploit a combination of static and dynamic type checking, and of in-lined reference monitoring, to guarantee absence of run-time errors due to lack of privileges and state two type soundness results: one involves whole nets, the other is relative to subnets of larger nets.

We present a programming notation aiming at protecting the secrecy of both host and agent data in global computing applications. The approach exploits annotations with sets of node addresses, called regions. A datum can be annotated with a region that specifies the network nodes that are allowed to interact with it. Network nodes come equipped with two region annotations specifying the nodes that can send data and spawn processes over them. The language semantics guarantees that computation proceeds according to these region constraints. To minimize the overhead of runtime checks, a static compilation phase is exploited. The proposed approach is largely independent of a specific programming language; however, to put it in concrete form, here we focus on its integration within the process language muKlaim. We prove that in compiled muKlaim nets, data can be manipulated only by authorized users. We also give a more local formulation of this property, where only a subnet is compiled. Finally, we use our theory to model the secure behaviour of a UNIX-like multiuser system.

Security is a key issue for distributed systems/applications with code mobility, like, e.g., e-commerce and on-line bank transactions. In a scenario with code mobility, traditional solutions based on cryptography cannot deal with all security issues and additional mechanisms are necessary. In this paper, we present a flexible and expressive type system for security for a calculus of distributed and mobile processes. By using a combination of static and dynamic checks, type safety and well-typedness preservation can be guaranteed, thus enforcing specific security policies on the use of resources. The usefulness of our approach will be shown by modeling the simplified behaviour of a bank account management system.

microKLAIM is a process language that permits programming distributed systems made up of several components interacting through multiple distributed tuple spaces. We present the language and a type system for controlling the activities, e.g. access to resources and mobility, of the processes in a net. By dealing with privileges acquisition and consumption, the type system enables dynamic variations of security policies. We exploit a combination of static and dynamic type checking, and of in-lined reference monitoring, to guarantee the absence of run-time errors due to lack of privileges and show two type safety results: one involves whole nets, the other is relative to subnets of larger nets.

It is often infeasible to recompile all the sources an application consists of each time a change is made. Yet, a recompilation strategy which does not guarantee the same outcome of an entire recompilation is not useful: why wasting time in debugging a program (a set of .class files in the Java case) which might behave differently from the program obtained recompiling all the sources from scratch? We say that a compilation strategy is sound if it recompiles, besides the changed sources, all the unchanged sources whose new binary, produced by the overall recompilation, would differ from the existing one (if any) and all the sources for which the recompilation would be undefined: indeed, when the entire compilation fails, so should do the partial recompilation. We say that a compilation strategy is minimal if it never recompiles an unchanged source whose new binary would be equal to the existing one. In this paper we present a compilation strategy for a substantial subset of Java which is proved to be sound and minimal.

In a recent work we have proposed a compilation strategy (that is, a way to decide which unchanged sources have to be recompiled) for a substantial subset of Java which has been shown to be sound and minimal. That is, an unchanged source is recompiled if and only if its recompilation produces a different binary or an error. However, that model does not handle two features of Java, namely, compile-time constant fields (static final fields initialized by a compile-time constant of a primitive type or String) and unreachable code, which turn out to be troublesome for having a sound and minimal compilation strategy. To our best knowledge these two features, probably because of their low-level nature, have been omitted in all models of Java separate compilation written so far. Yet, a compilation strategy for full Java has to deal with them. Thus, in this paper we analyze the implications of handling compile-time constant fields and unreachable code, and extend our previous model in order to handle these two features as well.

Inheritance is a crucial concept in object-oriented specification, design and programming, potentially enabling code reuse. This concept has been recently integrated with concurrency, due to the development of concurrent object-oriented programming. This chapter reviews the inheritance principle initially in the sequential setting and then in the context of concurrent onbject calculi. We discuss, subsume in a unifying model, and systemize the proposals in the literature.

The current definition of the Java bytecode verifier, as well as the proposals to formalize it, does not include any check about the structured use of locks by monitorenter and monitorexit instructions. So code is run, even if critical sections are corrupted. In this paper we isolate a sublanguage of the Java Virtual Machine with thread creation and mutual exclusion. For this subset we define a semantics and a formal verifier that enforces basic properties of threads and lock and unlock operations. The verifier integrates well with previous formalizations of the Java bytecode verifier. Our analysis of structured use of locks reveals the presence of bugs in the current compilers from Sun, IBM and Microsoft.

We present a calculus of mobile processes without prefix or summation, called the solos calculus. Using two different encodings, we show that the solos calculus can express both action prefix and guarded summation. One encoding gives a strong correspondence but uses a match operator; the other yields a slightly weaker correspondence but uses no additional operators. We also show that the expressive power of the solos calculus is still retained by the sub-calculus where actions carry at most two names. On the contrary, expressiveness is lost in the solos calculus without match and with actions carrying at most one name.

Klaim (Kernel Language for Agents Interaction and Mobility) is an experimental language specifically designed to program distributed systems consisting of several mobile components that interact through multiple distributed tuple spaces. Klaim primitives allow programmers to distribute and retrieve data and processes to and from the nodes of a net. Moreover, localities are first-class citizens that can be dynamically created and communicated over the network. Components, both stationary and mobile, can explicitly refer and control the spatial structures of the network. This paper reports the experiences in the design and development of Klaim. Its main purpose is to outline the theoretical foundations of the main features of Klaim and its programming model. We also present a modal logic that permits reasoning about behavioural properties of systems and various type systems that help in controlling agents movements and actions. Extensions of the language in the direction of object oriented programming are also discussed together with the description of the implementation efforts which have lead to the current prototypes.

Building on recent work by Rutten on coinduction and formal power series, we define a denotational semantics for the csp calculus and prove it fully abstract for testing equivalence. The proposed methodology allows for abstract definition of operators in terms of behavioural differential equations and for coinductive reasoning on them, additionally dispensing with continuous order-theoretic structures.

Automatic methods developed so far for analysis of security protocols only model a limited set of cryptographic primitives (often, only encryption and concatenation) and abstract from low-level features of cryptographic algorithms. This paper is an attempt towards closing this gap. We propose a symbolic technique and a decision method for analysis of protocols based on modular exponentiation, such as Diffie-Hellman key exchange. We introduce a protocol description language along with its semantics. Then, we propose a notion of symbolic execution and, based on it, a verification method. We prove that the method is sound and complete with respect to the language semantics.

The definition of filter model is extended to a variant of Ambient Calculus: Safe Ambient Calculus, introduced for developing an algebraic theory for a bisimulation-based behavioral equivalence. The types are constructed by means of elementary and higher-order actions, that define the moves processes can do. Entailment rules for types allow to translate the parallel composition of moves into nondeterministic choice of sequences of interleaved actions, providing a normal form for types assigned to processes. In the filter model obtained via the introduced type system, any process is interpreted as the set of all its types. The type assignment system results to be sound and complete with respect to the given semantics. Moreover the partial order relation induced by the filter model is compared with observational equivalence: the model is proved adequate, but it is shown, by means of a counter-example, that completeness fails.

In this paper, we introduce an actor language following a process algebra notation. The idea is to define a formalism that enjoys a clean formal definition allowing the reuse of standard results of the theory of concurrency in a context where an high level object oriented specification style is preserved. To illustrate the expressive power of the language, we provide a specification of the Hurried Philosophers case study.

We present STA (Symbolic Trace Analyzer), a tool for the analysis of security protocols. STA relies on symbolic techniques that avoid explicit construction of the whole, possibly infinite, state-space of protocols. This results in accurate protocol modeling, increased efficiency and more direct formalization, when compared to finite-state techniques. We illustrate the use of STA by analyzing two well-known protocols, asymmetric Needham Schroeder and Kerberos. We discuss the results of this analysis, and contrast them with previous work based on finite-state model checking.

We describe a metalanguage MMML, which makes explicit the order of evaluation (in the spirit of monadic metalanguages) and the staging of computations (as in languages for multi-level binding-time analysis). The main contribution of the paper is an operational semantics which is sufficiently detailed for analyzing subtle aspects of multi-stage programming, but also intuitive to serve as a reference semantics. For instance, the separation of computational types from code types, makes immediate the distinction between a computation for generating code and the generated code, and provides a basis for multi-lingual extensions, where a variety of programming languages (aka monads) coexist. The operational semantics consists of two parts: local (semantic preserving) simplification rules, and computation steps executed in a deterministic order (because they may have side-effects). The two parts can be changed independently: the first by adding datatypes or recursive definitions, the second by adding other computational effects. We focus on the computational aspects, thus we adopt a simple type system, that can detect usual type errors, but not the unresolved link errors. Because of its explicit annotations, MMML is suitable as an intermediate language, but (in comparison to MetaML) it is too verbose as a programming language.

We describe a metalanguage MMML, which makes explicit the order of evaluation (in the spirit of monadic metalanguages) and the staging of computations (as in languages for multi-level binding-time analysis). The main contribution of the paper is an operational semantics which is sufficiently detailed for analyzing subtle aspects of multi-stage programming, but also intuitive enough to serve as a reference semantics. For instance, the separation of computational types from code types, makes clear the distinction between a computation for generating code and the generated code, and provides a basis for multi-lingual extensions, where a variety of programming languages (aka monads) coexist. The operational semantics consists of two parts: local (semantics preserving) simplification rules, and computation steps executed in a deterministic order (because they may have side-effects). We focus on the computational aspects, thus we adopt a simple type system, that can detect usual type errors, but not the unresolved link errors. Because of its explicit annotations, MMML is suitable as an intermediate language.

Launchbury and Peyton Jones came up with an ingenious idea for embedding regions of imperative programming in a pure functional language like Haskell. The key idea was based on a simple modification of Hindley-Milner's type system. Our first contribution is to propose a more natural encapsulation construct exploiting higher-order kinds, which achieves the same encapsulation effect, but avoids the adhoc type parameter of the original proposal. The second contribution is a type safety result for encapsulation of strict state using both the original encapsulation construct and the newly introduced one. We establish this result in a more expressive context than the original proposal, namely in the context of the higher-order lambda-calculus. The third contribution is a type safety result for encapsulation of lazy state in the higher-order lambda-calculus. This result resolves an outstanding open problem on which previous proof attempts failed. In all cases, we formalize the intended implementations as simple big-step operational semantics on untyped terms, which capture interesting implementation details not captured by the reduction semantics proposed previously.

This paper proposes an operational semantics for value recursion in the context of monadic metalanguages. Our technique for combining value recursion with computational effects works uniformly for all monads. The operational nature of our approach is related to the implementation of recursion in Scheme and its monadic version proposed by Friedman and Sabry, but it defines a different semantics and does not rely on assignments. When contrasted to the axiomatic approach proposed by Erkök and Launchbury, our semantics for the continuation monad invalidates one of the axioms, adding to the evidence that this axiom is problematic in the presence of continuations.

An abstract machine for a distributed implementation of an ambient calculusis presented. The abstract machine is different from, and simpler than,previous implementations of ambient-like calculi, mainly because: the underlying calculus is typed Safe Ambients rather than the untyped Ambient calculus; the logical structure of an ambient system and its physical distribution are separated. The proof of correctness and a description of a distributed implementation of the abstract machine in Java are given.

Soft constraints extend classical constraints to represent multiple consistency levels, and thus provide a way to express preferences, fuzziness, and uncertainty. While there are many soft constraint solving formalisms, even distributed ones, by now there seems to be no concurrent programming framework where soft constraints can be handled. In this paper we show how the classical concurrent constraint (cc) programming framework can work with soft constraints, and we also propose an extension of cc languages which can use soft constraints to prune and direct the search for a solution. We believe that this new programming paradigm, called soft cc (scc), can be also very useful in many web-related scenarios. In fact, the language level allows web agents to express their interaction and negotiation protocols, and also to post their requests in terms of preferences, and the underlying soft constraint solver can find an agreement among the agents even if their requests are incompatible.

Wide-Area Network (WAN) applications have become one of the most popular applications in current distributed computing. Internet and the World Wide Web are now the primary environment for designing, developing and distributing applications. This scenario imposes different programming metaphors with respect to traditional applications.

Theoretical models for formally reasoning on WAN applications must consider many crucial aspects and their mutual relationships, e.g. mobility, network awareness, security, service level agreement, etc.

This dissertation attempts to formally define declarative approaches for dealing with various facets of actual WAN programming and verification issues.

We propose a declarative approach based on hypergraphs that provide foundational framework for ``declaring'' components' behaviours of a distributed system. It is exercised with two well-known models for distributed computations as Ambient and Klaim Moreover, we extend Klaim with constructs for specifying, at application level, network connections and related Quality of Service (QoS) requirements. It is also shown how a suitable translation of our Klaim extension into hypergraphs can be exploited for detecting and reserving optimal routing path with respect to the QoS constraints imposed by applications.

We also introduce a process calculus and a logic that specifies a formal framework for declaring security protocols and properties. By means of symbolic verification technique, the framework can be exploited as a verification environment for model checking security protocols. The declarative flavour of the analysis and the ability of dealing with multi-session verification is the major advantage of the proposed approach.

Finally, we describe a verification environment based on a semantic minimization algorithm for pi-calculus specifications presented in co-algebraic setting. The final part of this dissertation introduces and discusses an implementation of the algorithm together with other verification facilities of the framework. A proofs that shows the correctness of the implementation with respect to the co-algebraic specification is given.