Abstract Adaptive systems are designed to modify their behaviour at runtime in response to dynamically changing and open-ended environments as well as evolving requirements. Such systems may operate as individual adaptive entities or as collective adaptive systems composed of multiple collaborating components. Rigorous engineering of these systems requires appropriate methods, models, and tools that ensure reliability, correctness, and alignment with their intended purpose. This paper introduces the second part of the special section on Rigorous Engineering of Collective Adaptive Systems. It presents seven selected contributions and positions them within four major research directions: (i) Large Ensembles and Collective Dynamics, (ii) Knowledge, Consciousness and Emergence, (iii) Automated Reasoning for Better Interaction, and (iv) Analysing Collective Adaptive Systems. Together, they illustrate current progress and emerging challenges in the rigorous engineering of collective adaptive systems.

Abstract Adaptive systems are designed to modify their behaviour at runtime in response to dynamically changing and open-ended environments as well as evolving requirements. Such systems may operate as individual adaptive entities or as collective adaptive systems composed of multiple collaborating components. Rigorous engineering of these systems requires appropriate methods, models, and tools that ensure reliability, correctness, and alignment with their intended purpose. This paper introduces the first part of the special section on Rigorous Engineering of Collective Adaptive Systems. It presents six of the thirteen selected contributions and positions them within two major research directions: (i) Modelling and Engineering Collective Adaptive Systems, and (ii) Analysing Collective Adaptive Systems. Together, these contributions illustrate current progress and emerging challenges in the rigorous engineering of collective adaptive systems.

International audience

Variants of the must testing approach have been successfully applied in service oriented computing for analysing the compliance between (contracts exposed by) clients and servers or, more generally, between two peers. It has however been argued that multiparty scenarios call for more permissive notions of compliance because partners usually do not have full coordination capabilities. We propose two new testing preorders, which are obtained by restricting the set of potential observers. For the first preorder, called uncoordinated, we allow only sets of parallel observers that use different parts of the interface of a given service and have no possibility of intercommunication. For the second preorder, that we call individualistic, we instead rely on parallel observers that perceive as silent all the actions that are not in the interface of interest. We have that the uncoordinated preorder is coarser than the classical must testing preorder and finer than the individualistic one. We also provide a characterisation in terms of decorated traces for both preorders: the uncoordinated preorder is defined in terms of must-sets and Mazurkiewicz traces while the individualistic one is described in terms of classes of filtered traces that only contain designated visible actions and must-sets.

Abstract This paper advocates the use of compositional specifications based on formal languages as a means of modelling and analysing sophisticated collective behaviour in natural systems. With the use of appropriate linguistic constructs, models can be developed that are both compact and intuitive, and can be easily refined and extended in small steps. Automated workflows can be implemented on top of this methodology to provide quick feedback, enabling rapid design iterations. To support our argument, we present three examples from the natural world, focusing on flocks of birds and colonies of ants, which feature well-known examples of emergent behaviour in collective adaptive systems. We use an agent-based language to develop simple models that aim at capturing these collective phenomena, and discuss the specific language constructs that we use in the process. Then, we adapt an existing verification tool for the language to simulate our models, and show that our simulations do display emergent behaviour.

Abstract An adaptive system is able to adapt at runtime to dynamically changing environments and to new requirements. Adaptive systems can be single adaptive entities or collective ones that consist of several collaborating entities. Rigorous engineering requires appropriate methods and tools that help guaranteeing that an adaptive system lives up to its intended purpose. This paper introduces the special section on “Rigorous Engineering of Collective Adaptive Systems.” It presents the 11 contributions of the section categorizing them into five distinct research lines: correctness by design and synthesis, computing with bio-inspired communication, new system models, machine learning, and programming and analyzing ensembles.

Coordination languages for tuple spaces can offer significant advantages in the specification and implementation of distributed systems, but often do require manual programming effort to ensure consistency. We propose an experimental technique for automated replication of tuple spaces in distributed systems. The system of interest is modelled as a concurrent Go program where different threads represent the behaviour of the separate components, each owning its own local tuple repository. We automatically transform the initial program by combining program transformation and static analysis, so that tuples are replicated depending on the components' read-write access patterns. In this way, we turn the initial system into a replicated one where the replication of tuples is automatically achieved, while avoiding unnecessary replication overhead. Custom static analyses may be plugged in easily in our prototype implementation. We see this as a first step towards developing a fully-fledged framework to support designers to quickly evaluate many classes of replication-based systems under different consistency levels.

Sequential emulation is a semantics-based technique to automatically reduce property checking of distributed systems to the analysis of sequential programs. An automated procedure takes as input a formal specification of a distributed system, a property of interest, and the structural operational semantics of the specification language and generates a sequential program whose execution traces emulate the possible evolutions of the considered system. The problem as to whether the property of interest holds for the system can then be expressed either as a reachability or as a termination query on the program. This allows to immediately adapt mature verification techniques developed for general-purpose languages to domain-specific languages, and to effortlessly integrate new techniques as soon as they become available. We test our approach on a selection of concurrent systems originated from different contexts from population protocols to models of flocking behaviour. By combining a comprehensive range of program verification techniques, from traditional symbolic execution to modern inductive-based methods such as property-directed reachability, we are able to draw consistent and correct verification verdicts for the considered systems.

Summary The current cloud market is dominated by a few providers, which offer cloud services in a take‐it‐or‐leave‐it manner. However, the dynamism and uncertainty of cloud environments may require the change over time of both application requirements and service capabilities. The current service‐level agreement (SLA) management solutions cannot easily guarantee a trustworthy, distributed SLA adaptation due to the centralized authority of the cloud provider who could also misbehave to pursue individual goals. To address the above issues, we propose a novel SLA management framework, which facilitates the specification and enforcement of dynamic SLAs that enable one to describe how, and under which conditions, the offered service level can change over time. The proposed framework relies on a two‐level blockchain architecture. At the first level, the smart SLA is transformed into a smart contract that dynamically guides service provisioning. At the second level, a permissioned blockchain is built through a federation of monitoring entities to generate objective measurements for the smart SLA/contract assessment. The scalability of this permissioned blockchain is also thoroughly evaluated. The proposed framework enables creating open distributed clouds, which offer manageable and dynamic services, and facilitates cost reduction for cloud consumers, while it increases flexibility in resource management and trust in the offered cloud services.

Building open, distributed systems while guaranteeing a specific behaviour is difficult because of the dynamicity of the operating environments and the complexity of the interactions of their components. The AbC calculus provides a novel communication mechanism to select interacting partners based on their runtime capabilities, making it naturally to model complex interactions and adaptive behaviour in such systems. The formal account of this calculus has enabled constructing formally verifiable models and proving their properties. In this paper, we i) propose an implementation of AbC using the Erlang language ii) formalize the operational semantics of our implementation; iii) propose a set of rules that given an AbC specification, automatically generate Erlang executable code; and iv) prove that the proposed translation is correct by establishing a simulation relation between source and target specifications. This enables us to guarantee that any property proved for a given AbC specification is preserved by the corresponding implementation.

Collective adaptive systems are new emerging computational systems consisting of a large number of interacting components and featuring complex behaviour. These systems are usually distributed, heterogeneous, decentralised and interdependent, and are operating in dynamic and possibly unpredictable environments. Finding ways to understand and design these systems and, most of all, to model the interactions of their components, is a difficult but important endeavour. In this article we propose a language-based approach for programming the interactions of collective-adaptive systems by relying on attribute-based communication; a paradigm that permits a group of partners to communicate by considering their run-time properties and capabilities. We introduce AbC, a foundational calculus for attribute-based communication and show how its linguistic primitives can be used to program a sophisticated variant of the well-known problem of Stable Allocation in Content Delivery Networks. In our variant, content providers are assigned to clients based on collaboration and by taking into account the preferences of both parties in a fully anonymous and distributed settings. We also illustrate the expressive power of attribute-based communication by showing the natural encoding of group-based, publish/subscribe-based and channel-based communication paradigms into AbC.

Abstract An adaptive system is able to adapt at runtime to dynamically changing environments and to new requirements. Adaptive systems can be single adaptive entities or collective ones that consist of several collaborating entities. Rigorous engineering requires appropriate methods and tools that help guaranteeing that an adaptive system lives up to its intended purpose. This paper introduces the special section on “Rigorous Engineering of Collective Adaptive Systems.” It presents the seven contributions of the section and gives a short overview of the field of rigorously engineering collective adaptive systems by structuring it according to three topics: systematic development, methods and theories for modelling and analysis, and techniques for programming and operating collective adaptive systems.

Abstract Latency-sensitive and data-intensive applications, such as IoT or mobile services, are leveraged by Edge computing, which extends the cloud ecosystem with distributed computational resources in proximity to data providers and consumers. This brings significant benefits in terms of lower latency and higher bandwidth. However, by definition, edge computing has limited resources with respect to cloud counterparts; thus, there exists a trade-off between proximity to users and resource utilization. Moreover, service availability is a significant concern at the edge of the network, where extensive support systems as in cloud data centers are not usually present. To overcome these limitations, we propose a score-based edge service scheduling algorithm that evaluates network, compute, and reliability capabilities of edge nodes. The algorithm outputs the maximum scoring mapping between resources and services with regard to four critical aspects of service quality. Our simulation-based experiments on live video streaming services demonstrate significant improvements in both network delay and service time. Moreover, we compare edge computing with cloud computing and content delivery networks within the context of latency-sensitive and data-intensive applications. The results suggest that our edge-based scheduling algorithm is a viable solution for high service quality and responsiveness in deploying such applications.

Cloud services operate in a highly dynamic environment. This means that they need to be assorted with dynamic SLAs which explicate how a rich set of QoS guarantees evolves over time. Only in this way, cloud users will trust and thus migrate their processes to the cloud. Research-wise, SLAs are assumed to include single states while they are managed mainly in a centralised manner. This paper proposes a framework to manage dynamic SLAs in a distributed manner by relying on a rich and dynamic SLA formalism which is transformed into a smart contract. This contract is then handled via the blockchain which exploits an oracle-based interface to retrieve the off-chain cloud service context sensed and enforce the right SLA management/modification functions. The proposed framework can change the current shape of the cloud market by catering for the notion of an open distributed cloud which offers manageable and dynamic services to cloud customers enabling them to reduce costs and increase the flexibility in resource management.

Data availability is a key aspect of modern distributed systems. We discuss an extension of coordination languages based on tuple spaces with programming abstractions for sharing data and guaranteeing availability with different consistency guarantees. Data can be spread over the system according to user-specified replica placement strategies and user-specified consistency requirements. The framework takes care then of low-level management of the replicas, so that the programmer can just focus on the business logic of the application. We advocate that the proposed programming primitives are beneficial for data-oriented applications where different kinds of data may have different needs in terms of availability and consistency.

On social networks, the storage, usage, and sharing of users data is usually regulated by privacy policies: natural language terms, in which specific actions are authorised, obliged, or denied, under some contextual conditions. Although guaranteeing degrees of readability and clarity, policies in natural language are not machine readable, thus preventing automatic controls on how the data are actually going to be used and processed by the entities that operate on them. In this paper, we propose an ontology-based approach for automatic translation of privacy statements, from natural language to a controlled natural one, to facilitate machine-readable processing. We provide a prototype implementation of the software-based translation tool, showing its effectiveness on a set of Facebook data policies.

Summary Among the paradigms for parallel and distributed computing, the one popularized with Linda, and based on tuple spaces, is one of the least used, despite the fact of being intuitive, easy to understand, and easy to use. A tuple space is a repository, where processes can add, withdraw, or read tuples by means of atomic operations. Tuples may contain different values, and processes can inspect their content via pattern matching. The lack of a reference implementation for this paradigm has prevented its wide spreading. In this paper, first we perform an extensive analysis of a number of actual implementations of the tuple space paradigm and summarize their main features. Then, we select four such implementations and compare their performances on four different case studies that aim at stressing different aspects of computing, such as communication, data manipulation, and CPU usage. After reasoning on strengths and weaknesses of the four implementations, we conclude with some recommendations for future work towards building an effective implementation of the tuple space paradigm.

A smart contract is the formalisation of an agreement, whose terms are automatically enforced by relying on a transaction protocol, while minimising the need of intermediaries. Such contracts not only specify the service and its quality but also the possible changes at runtime of the terms of agreement. Although smart contracts provide a great deal of flexibility, analysing their compatibility and reaching agreements with this level of dynamism is considerably more challenging, due to the freedom of clients and providers in formulating needs/offers. We introduce a formal language to specify interactions between offers and requests and present a methodology for the autonomous negotiation of smart contracts, which analyses the cost and the necessary changes for reaching an agreement. Moreover, we describe a set of experiments that provides insights on the relative cost of dynamism in negotiating smart contracts and compare the request/offer matching rates of our solution with related works.

Service-oriented computing is calling for novel computational models and languages with well-disciplined primitives for client–server interaction, structured orchestration and unexpected events handling. We present CaSPiS, a process calculus where the conceptual abstractions of sessioning and pipelining play a central role for modelling service-oriented systems. CaSPiS sessions are two-sided, uniquely named and can be nested. CaSPiS pipelines permit orchestrating the flow of data produced by different sessions. The calculus is also equipped with operators for handling (unexpected) termination of the partner's side of a session. Several examples are presented to provide evidence of the flexibility of the chosen set of primitives. One key contribution is a fully abstract encoding of Misra et al.'s orchestration language Orc. Another main result shows that in CaSPiS it is possible to program a ‘graceful termination’ of nested sessions, which guarantees that no session is forced to hang forever after the loss of its partner.

Social Web Services (SWSs) constitute a novel paradigm of service-oriented computing, where Web services, just like humans, sign up in social networks that guarantee, e.g., better service discovery for users and faster replacement in case of service failures. In past work, composition of SWSs was mainly supported by specialised social networks of competitor services and cooperating ones. In this work, we continue this line of research, by proposing a novel SWSs composition procedure driven by the SWSs reputation. Making use of a well-known formal language and associated tools, we specify the composition steps and we prove that such reputation-driven approach assures better results in terms of the overall quality of service of the compositions, with respect to randomly selecting SWSs.

The autonomic computing paradigm has been proposed to cope with size, complexity, and dynamism of contemporary software-intensive systems. The challenge for language designers is to devise appropriate abstractions and linguistic primitives to deal with the large dimension of systems and with their need to adapt to the changes of the working environment and to the evolving requirements. We propose a set of programming abstractions that permit us to represent behaviors, knowledge, and aggregations according to specific policies and to support programming context-awareness, self-awareness, and adaptation. Based on these abstractions, we define SCEL (Software Component Ensemble Language), a kernel language whose solid semantic foundations lay also the basis for formal reasoning on autonomic systems behavior. To show expressiveness and effectiveness of SCEL;’s design, we present a Java implementation of the proposed abstractions and show how it can be exploited for programming a robotics scenario that is used as a running example for describing the features and potential of our approach.

We study the functorial characterisation of bisimulation-based equivalences over a categorical model of labelled trees. We show that in a setting where all labels are visible, strong bisimilarity can be characterised in terms of enriched functors by relying on the reflection of paths with their factorisations. For an enriched functor F, this notion requires that a path (an internal morphism in our framework) π going from F(A) to C corresponds to a path p going from A to K, with F(K) = C, such that every possible factorisation of π can be lifted in an appropriate factorisation of p. This last property corresponds to a Conduché property for enriched functors, and a very rigid formulation of it has been used by Lawvere to characterise the determinacy of physical systems. We also consider the setting where some labels are not visible, and provide characterisations for weak and branching bisimilarity. Both equivalences are still characterised in terms of enriched functors that reflect paths with their factorisations: for branching bisimilarity, the property is the same as the one used to characterise strong bisimilarity when all labels are visible; for weak bisimilarity, a weaker form of path factorisation lifting is needed. This fact can be seen as evidence that strong and branching bisimilarity are strictly related and that, unlike weak bisimilarity, they preserve process determinacy in the sense of Milner.

Action-labelled transition systems (LTSs) have proved to be a fundamental model for describing and proving properties of concurrent systems. In this paper we introduce Multiple-Labelled Transition Systems (MLTSs) as generalisations of LTSs that enable us to deal with system features that are becoming increasingly important when considering languages and models for network-aware programming. MLTSs enable us to describe not only the actions that systems can perform but also their usage of resources and their handling (creation, revelation . . .) of names; these are essential for modelling changing evaluation environments. We also introduce MoMo, which is a logic inspired by Hennessy–Milner Logic and the μ-calculus, that enables us to consider state properties in a distributed environment and the impact of actions and movements over the different sites. MoMo operators are interpreted over MLTSs and both MLTSs and MoMo are used to provide a semantic framework to describe two basic calculi for mobile computing, namely μKlaim and the asynchronous π-calculus.

Subtyping relations for the /spl pi/-calculus are usually defined in a syntactic way, by means of structural rules. We propose a semantic characterisation of channel types and use it to derive a subtyping relation. The type system we consider includes read-only and write-only channel types, as well as Boolean combinations of types. A set-theoretic interpretation of types is provided, in which Boolean combinations are interpreted as the corresponding set-theoretic operations. Subtyping is defined as inclusion of the interpretations. We prove the decidability of the subtyping relation and sketch the subtyping algorithm. In order to fully exploit the type system, we define a variant of the /spl pi/-calculus where communication is subjected to pattern matching that performs dynamic typecase.

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. This paper presents a temporal logic for specifying properties of Klaim programs. The logic is inspired by Hennessy-Milner Logic (HML) and the μ-calculus, but has novel features that permit dealing with state properties and impact of actions and movements over the different sites. The logic is equipped with a complete proof system that enables one to prove properties of mobile systems.

We provide a finite equational axiomatization for bisimulation equivalence of nondeterministic interpretation of regular expressions. Our axiomatization is heavily based on the one by Salomaa, that provided an implicative axiomatization for a large subset of regular expressions, namely all those that satisfy the non-empty word property (i.e. without 1 summands at the top level) in *-contexts. Our restriction is similar, it essentially amounts to recursively requiring that the non-empty word property be satisfied not just at top level but at any depth. We also discuss the impact on the axiomatization of different interpretations of the 0 term, interpreted either as a null process or as a deadlock.

Abstract Highly distributed networks have now become a common infrastructure for wide‐area distributed applications whose key design principle is network awareness, namely the ability to deal 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 describe how KLAVA permits code mobility by relying on Java and present a few distributed applications that exploit mobile code programmed in KLAVA. Copyright © 2002 John Wiley & Sons, Ltd.

Contextual equivalences for cryptographic process calculi, like the spi-calculus, can be used to reason about correctness of protocols, but their definition suffers from quantification over all possible contexts. Here, we focus on two such equivalences, namely may-testing and barbed equivalence, and investigate tractable proof methods for them. To this aim, we design an enriched labelled transition system, where transitions are constrained by the knowledge the environment has of names and keys. The new transition system is then used to define a trace equivalence and a weak bisimulation equivalence that avoid quantification over contexts. Our main results are soundness and completeness of trace and weak bisimulation equivalence with respect to may-testing and barbed equivalence, respectively. They lead to more direct proof methods for equivalence checking. The use of these methods is illustrated with a few examples concerning implementation of secure channels and verification of protocol correctness.

Contextual equivalences for cryptographic process calculi can be used to reason about correctness of protocols, but their definition suffers from quantification over all possible contexts. Here, we focus on two such equivalences, may-testing and barbed equivalence, and investigate tractable proof methods for them. To this aim, we develop an 'environment-sensitive' labelled transition system, where transitions are constrained by the knowledge the environment has of names and keys. On top of the new transition system, a trace equivalence and a co-inductive weak bisimulation equivalence are defined, both of which avoid quantification over contexts. Our main results are soundness of trace semantics and of weak bisimulation with respect to may-testing and barbed equivalence, respectively. This leads to more direct proof methods for equivalence checking. The use of such methods is illustrated via a few examples concerning implementation of secure channels by means of encrypted public channels. We also consider a variant of the labelled transition system that gives completeness, but is less handy to use.

We investigate the issue of designing a kernel programming language for mobile computing and describe KLAIM, a language that supports a programming paradigm where processes, like data, can be moved from one computing environment to another. The language consists of a core Linda with multiple tuple spaces and of a set of operators for building processes. KLAIM naturally supports programming with explicit localities. Localities are first-class data (they can be manipulated like any other data), but the language provides coordination mechanisms to control the interaction protocols among located processes. The formal operational semantics is useful for discussing the design of the language and provides guidelines for implementations. KLAIM is equipped with a type system that statically checks access right violations of mobile agents. Types are used to describe the intentions (read, write, execute, etc.) of processes in relation to the various localities. The type system is used to determine the operations that processes want to perform at each locality, and to check whether they comply with the declared intentions and whether they have the necessary rights to perform the intended operations at the specific localities. Via a series of examples, we show that many mobile code programming paradigms can be naturally implemented in our kernel language. We also present a prototype implementation of KLAIM in Java.

Three of the rewriting systems used by Degano, De Nicola and Montanari to provide Milner's CCS with a causality based semantics are compared by using also a fourth intermediate one. These rewriting systems have been used to associate Petri nets, Labelled Event Structures and structured sets of partial orderings to CCS terms. It is proved that the four rewriting systems yield computations from which the same causality relations among the executed actions can be extracted, thus it is established that the four partial ordering transitional semantics do coincide.

Three temporal logics are introduced that induce on labeled transition systems the same identifications as branching bisimulation, a behavioral equivalence that aims at ignoring invisible transitions while preserving the branching structure of systems. The first logic is an extension of Hennessy-Milner Logic with an “until” operator. The second one is another extension of Hennessy-Milner Logic, which exploits the power of backward modalities. The third logic is CTL* without the next-time operator. A relevant side-effect of the last characterization is that it sets a bridge between the state- and action-based approaches to the semantics of concurrent systems.

Three temporal logics are introduced which induce on labeled transition systems the same identifications as branching bisimulation. The first is an extension of Hennessy-Milner logic with a kind of unit operator. The second is another extension of Hennessy-Milner logic which exploits the power of backward modalities. The third is CTL* with the next-time operator interpreted over all paths, not just over maximal ones. A relevant side effect of the last characterization is that it sets a bridge between the state- and event-based approaches to the semantics of concurrent systems.>

The problem of the relationship between truly concurrent operational and denotational semantics is tackled by mapping syntactic terms on similar semantic domains in both approaches. Occurrence nets are associated to terms through structural operational semantics based on a set of rewriting rules; event structures are defined as denotations for terms, without resorting to categorical constructions. The proof of the equivalence of the two semantics relies on the direct correspondence between occurrence nets and event structures. R. Milner's (1980) calculus of communicating systems is used as a test case; truly concurrent denotional and operational semantics are given for it and proved consistent. This equivalence is established for the first time in true concurrency approach. It is proved that G. Winskel's (1982) categorical denotational semantics is equivalent to that given here.>