Computer Science and Applications Research Seminars

Control Lyapunov functions provide a fundamental tool to support control design when robustness, constraints fulfillment and optimality have to be simultaneous addressed in system stabilization. However, such general control problem is very challenging and almost impossible to be solved using a single control Lyapunov function. The recent framework of R-functions allow the design of innovative control Lyapunov functions having smooth and non-homothetic level sets. In particular, given a control Lyapunov function with a "large" domain of attraction and a second one guaranteeing local optimality, our merging procedure yields the controlled domain of attraction of the former and the local performance of the latter.

The coordination modeling language Paradigm distinguishes fine-grained behaviour of transitions between states and coarse-grained behaviour of transfers between phases in component-based systems. The semantics guarantees vertical consistency of states and phases within a component. Protocols maintain horizontal consistency for collaborations of components. By adapting the protocols at run-time, system evolution can be arranged on-the-fly. We discuss for examples of a critical-section problem and a production line how dynamic system adaptation using the symbolic model checker mCRL2 can be verified

Session types and contracts are two formalisms used to study client-server interactions. In this talk we show the relationship between them. In particular, we will show a natural interpretation of session types into a subset of contracts. This interpretation can be used to define a fully abstract model for the relation of sub-typing on session types.

Operational semantics describes the behaviour of programs in a language in terms of their execution on an abstract machine, which is often represented as a, possibly infinite, state machine. Structural Operational Semantics is a rule-based and syntax-driven approach to giving operational semantics to programming and specification languages. Determinism is a semantic property of (a fragment of) a language that specifies that a program cannot evolve operationally in several different ways. Idempotence is a property of binary language constructs requiring that the composition of two identical specifications or programs will result in a piece of specification or program that is equivalent to the original components. In this talk, I will discuss two (related) meta-theorems for guaranteeing determinism and idempotence of binary operators. These meta-theorems are formulated in terms of syntactic templates for operational semantics, called rule formats. I will argue for the applicability of the proposed formats by applying them to various operational semantics from the literature. The talk is based on joint work with Arnar Birgisson (Chalmers), Anna Ingolfsdottir (Reykjavik University), MohammadReza Mousavi (TU Eindhoven) and Michel A. Reniers (TU Eindhoven). A journal paper based on this work will appear in Science of Computer Programming (http://dx.doi.org/10.1016/j.scico.2010.04.002).

FastFlow is a programming framework specifically targeting multi- and many-cores architetcures. It is implemented as a stack of C++ template libraries built on top of lock-free (and memory fence free) synchronization mechanisms. Its philosophy is to combine programmability with performance. In particular, FastFlow promotes (lock-free) pattern-based programming by providing programmers with extendible high-level parallel constructs, which are implemented as parametric streaming networks. They are realized by decoupling synchronizations of parallel activities, which are implemented in a message-passing style, and data exchange, which can be realized in both message-passing and shared-memory style (by way of pointer passing). This makes it possible: 1) to implement the whole run-time support in a lock-free and memory fence-free fashion, which ensures the efficient orchestration of fine-grained parallel activities on cache-coherent architectures (down to ~10 ns core-to-core synchronization latency); and 2) to employ different programming models to enhance locality or fast data movement according to the patterns’ high-level semantics. FastFlow’s expressivity will be illustrated by way of existing applications, which span different areas and include extensions to the programming model itself. Throughout the talk, the technological and methodological advances we advocate will be discussed in the perspective of challenges in formal methods to support performance and productivity in programming models we believe will characterize the multi-core era. More information at http://di.unito.it/fastflow

Model checking is one of the most successful formal techniques for the verification of software and hardware systems. Developed in the beginning of the eighties, nowadays it is used by major companies, like Microsoft, to improve the quality of their products. In my talk I focus on improvements of model checking algorithms by exploiting the recent developments in the processor technology. In particular, the emphasis is on parallel algorithms for shared memory architectures, like multi-core systems and general purpose graphic processing units (GPGPUs). These research directions are quite new - the first papers on multi-core and GPU model checking were published in the last four years. Therefore, there are still many untrodden avenues for cooperation of experts from different computer science communities. For example, one of the main open problems is how to design an efficient (shared memory) parallel algorithm for finding cycles in the state space graph. In the recent years we have been using successfully GPUs for accelerating probabilistic model checking. The implementations in the probabilistic model checker PRISM achieve speedups of more than one order of magnitude compared to their sequential counterparts. Our approach crucially hinges on efficient parallel algorithms for sparse matrix vector multiplication. The above mentioned issues, like cycle detection and multiplication algorithms, are in principle independent on their applications in model checking and as such can be interesting for other computer science areas.

Important progresses in medicine and healthcare has been made during the last century. The duration of the life of human beings is dramatically increased. Population of the developed countries is aging, causing serious problems in the health sector. In Europe it is expected that the number of citizens aged over 65 will rise up to 123 millions in 2030. This fact will have a huge impact on social, economic, and health aspects. On the other hand, access to healthcare treatment is not always granted in developing countries where healthcare and communications infrastructures are missing. Electronic health (e-Health) can help to overcome these problems. The aim is to make it possible for patients to maintain a mobile and independent lifestyle. The e-Health has the possibility to bring electronic healthcare treatments to citizens and regions, which otherwise would not have access to it, and improves their quality of life. Initiatives like Integrating the Healthcare Enterprise (IHE) have been developed for the definition of standard methodologies for secure and interoperable EHR exchanges among clinics and hospitals. Using the requisites specified by these initiatives, many large-scale projects have been set up to enable healthcare professionals to handle patients' EHRs. Applications deployed in these settings are often considered safety-critical, thus ensuring such security properties as confidentiality, authentication, and authorization is crucial for their success. This seminar will introduce de-facto security standards for e-Health software interoperability (OASIS, Hl7, IHE) in Service Oriented Architectures. Common problems and security flaws found in real project specifications will be covered.

In rhopi every step can always be undone, and each process freely moves back and forward. To make rhopi usable to program recoverable systems, the ability to go back has to be controlled. Many possibilities in this direction exist. We analyze one such possibility, namely the introduction in rhopi of an explicit rollback primitive. The definition of a proper semantics for such a primitive is a surprisingly delicate matter because of the potential interferences between concurrent rollbacks. We define a high-level operational semantics allowing to capture concurrent rollbacks. We also define a lower-level distributed semantics, which is closer to an actual implementation of the rollback primitive. The two semantics are equivalent with respect to weak barbed congruence.

The notion of reversible computation is attracting increasing interest because of its applications in diverse fields, in particular the study of programming abstractions for reliable systems. In this paper, we continue the study undertaken by Danos and Krivine on reversible CCS by defining a reversible higher-order pi-calculus (HOpi). We prove that reversibility in our calculus is causally consistent and that one can encode faithfully reversible HOpi into a variant of HOpi.

In this talk, I propose a functional framework to understand the emergence of intelligence in agents exposed to examples and knowledge granules. The theory is based on the abstract notion of constraint, which provides a representation of knowledge granules gained from the interaction with the environment. I give a picture of the “agent body” in terms of representation theorems by extending the classic framework of kernel machines in such a way to incorporate logic formalisms, like first-order logic. This is made possible by the unification of continuous and discrete computational mechanisms in the same functional framework, so as any stimulus, like supervised examples and logic predicates, is translated into a constraint. The learning, which is based on constrained variational calculus, is either guided by a parsimonious match of the constraints or by unsupervised mechanisms expressed in terms of the minimization of the entropy. I show some experiments with different kinds of symbolic and sub-symbolic constraints, and then I give insights on the adoption of the proposed framework in computer vision. It is shown that in most interesting tasks the learning from constraints naturally leads to “deep architectures”, that emerge when following the developmental principle of focusing attention on “easy constraints”, at each stage. Interestingly, this suggests that stage-based learning, as discussed in developmental psychology, might not be primarily the outcome of biology, but it could be instead the consequence of optimization principles and complexity issues that hold regardless of the “body.”

In distributed systems, the traditional way of enforcing security is by means of access control security policies. We propose a framework and some analyses that can be done over it. The framework allows attaching security policies in the various locations of the system, following a realistic and practical fashion. As the runtime system involves interaction of locations, groups of policies may be relevant thereby needing a logic and consistent way of combining them. This leads to a complex system of networks and security policies that are only sometimes relevant. The resulting global system cannot then be trivially certified by static means. We propose a model checking that does not explore the entire state space but is inspired in static analysis techniques instead. Our aim is to have a formal framework with which it is possible to design distributed systems with adaptable and certifiable security.

The experience of art in urban space represents a very special case in the area of the studies of reception. In museums or galleries, reception of art often tries visitors' membership of the "worlds of art" (H. S. Becker, 1988). But the whole "apparatus" of museums and galleries (as a "system of relations" between material and non material, human and non human elements - Foucault, 1973) generally can help them in going beyond this "trial". In urban space, this apparatus is lacking, most of the time... In such a context, the meeting with a work of art is like this "astounding complex" (or "negative experience") Goffman described in his Frame analysis (1986). After an overlook on theories of reception, and its process that involves memories and affects, we particularly will point out the role that plays the apparatus in giving its "form" to the experience of art, including in urban space. On this "system of relations" basically depend the true nature of things (what is a work of art ?... Or another kind of symbolic objects) and our subjective "response" (Freedberg, 1986) : cognitive and emotional as well.

We introduce the problem of Model Repair for Probabilistic Systems as follows. Given a probabilistic system M and a probabilistic temporal logic formula φ such that M fails to satisfy φ, the Model Repair problem is to find an M that satisfies φ and differs from M only in the transition flows of those states in M that are deemed controllable. Moreover, the cost associated with modifying M’s transition flows to obtain M should be minimized. Using a new version of parametric probabilistic model checking, we show how the Model Repair problem can be reduced to a nonlinear optimization problem with a minimal-cost objective function, thereby yielding a solution technique. We demonstrate the practical utility of our approach by applying it to a number of significant case studies, including a DTMC reward model of the Zeroconf protocol for assigning IP addresses, and a CTMC model of the highly publicized Kaminsky DNS cache-poisoning attack.

A language is "higher-order" if program code can be passed around, that is, terms of the language can be values. Developing a theory of behavioural equivalence in higher-order languages can be hard. Particularly challenging can be: (1) the proof of congruence, (2) obtaining definitions and results that scale to languages with different features. In the talk, I will discuss the problems that higher-order languages present, and some approaches to tackle these problems. I will start from the lambda-calculus --the best known higher-order language-- and then move to the higher-order pi-calculus.

Service-based applications are considered a promising technology since they are able to offer complex and flexible functionalities in widely distributed environments by composing different types of services. These applications have to be adaptable to unforeseen changes in the functionality offered by component services and to their unavailability or decreasing performances. Furthermore, when applications are made available to a high number of potential users, they should also be able to dynamically adapt to the current context of use as well as to specific requirements and needs of the specific users. In order to address these issues, mechanisms that enable adaptation should be introduced in the life-cycle of applications, both in the design and in the runtime phases. The seminar is organized in three parts. In the first part the speaker will present design principles and guidelines that are suitable to enable adaptation, discussing their effectiveness of the proposed methodology by means of real-world scenarios over various types of service-based applications. In the second Bucchiarone will present a formal framework designed and implemented with the goal to adapt the execution of service-based business processes at runtime in case of context changes. He will conclude with a demo to show all concepts behind adaptation of service-based applications.

A Markovian bisimulation equivalence has been defined for sequential processes, which is weak in the sense that it reduces certain sequences of exponentially timed internal actions to single exponentially timed internal actions having the same average duration and execution probability as the corresponding sequences. This weak Markovian bisimulation equivalence is a congruence for sequential processes with abstraction and turns out to induce an exact CTMC-level aggregation at steady state for all the processes. Unfortunately, it is not a congruence with respect to parallel composition. In this talk, we show how to extend it to concurrent processes in a way that a reasonable tradeoff among abstraction, compositionality, and exactness is achieved. In particular, by enhancing the abstraction capability when dealing with concurrent computations, it is possible to retrieve the congruence property with respect to parallel composition, with the resulting CTMC-level aggregation being exact at steady state for a certain class of concurrent processes.

In this seminar we focus on material culture, specifically how the physical properties of objects convey or inhibit our understanding of their social meaning

In this seminar we explore the links between social structure and culture by looking at the interplay among the social world, creators, audiences, and culture

The Markovian behavioral equivalences defined so far treat exponentially timed internal actions like any other action. Since an exponentially timed internal action has a nonzero duration, it can be observed whenever it is executed between a pair of exponentially timed noninternal actions. However, no difference may be noted between a sequence of exponentially timed internal actions and a single exponentially timed internal action as long as their average durations coincide. We show that Milner's construction to derive a weak bisimulation congruence for nondeterministic processes can be extended to sequential Markovian processes in a way that captures the above situation. We then prove that the resulting weak Markovian bisimulation congruence admits a sound and complete axiomatization, induces an exact CTMC-level aggregation at steady state, and is decidable in polynomial time for finite-state processes having no cycles of exponentially timed internal actions.

The main objective of this seminar is to outline a roadmap for the definition of the vision of the Culture, Communication and Computing unit and discuss it with the students of the Management and Development of Cultural Heritage phd program. The C3 unit, Culture, Communication & Computing at the IMT Lucca aims at conducting innovative research and designing technologies and applications to explore new paradigms related to cultural heritage, to rethink how innovative technologies can improve users’ activities & experiences, and generate new concepts to enrich the user experience in the context of cultural heritage. During the seminar, a critical review of several case studies related to the intersection between interactive technologies and cultural heritage will be provided. The main assets of the C3 vision will be identified as well as long-term research objectives. Furthermore, the Locast Tourism - Lucca project will be introduced as the first concrete step of the unit.

This talk gives an overview of recent research concerning the use of stochastic process algebras for the quantitative evaluation of computer systems. The talk consists of three parts. The first part will introduce some basic notions on the usual discrete-state semantics in terms of continuous-time Markov chains. The second part will focus on the stochastic process algebra PEPA and discuss its fluid interpretation, a deterministic approximation with ordinary differential equations for the analysis of large-scale models. Finally, the third part will discuss how to compute typical measures of performance such as utilisation, throughput, and average response times from fluid models. Backed by theoretical results of asymptotic convergence, extensive numerical assays will show good accuracy of this approach for all practical purposes.

Over the past few years, renewable energy (from sun, wind, or water power) has rapidly advanced as a economical and ecological factor, within the European Union and even world-wide. The production facilities (e.g. solar panels, wind or water power turbines) are typically widely distributed and are in the low-to-medium power range. While the traditional power distribution structure is organized in a top-down manner this is inadequate and more than inefficient for renewable energy. In the seminar the DEZENT will be presented where power management, distribution, and “market” negotiations are handled through bottom-up control. In order to cope with the high amount of unpredictability of the regenerative sources we manage to do the whole business of negotiating, power distribution, grid stability checking and/or redistributing power flows within intervals (periods) of 0,5 sec, independent of the number of customers involved. (Keeping this rather tight deadline allows to assume that the negotiation situation, i.e. for demand and supply, is constant in the meantime.) The customer agents frequently adapt their strategies through distributed collaborative learning procedures (tailored Reinforcement Learning). Reserve energy needed for peak demand situations can be kept to a minimum because smart meters – as part of smart consumer facilities - would be utilized to dynamically make use of “conditional” consumers whereas in peak supply situations excessive power would be fed into large stationary batteries or grid-connected e-vehicles. The emphasis of the talk will be on the technical context. Also steps into the future will be indicated.

The service oriented computing (SOC) paradigm enables software application developers and service providers to dynamically grow application portfolios by seamlessly integrating services, information, and processes over the networks. One of the most relevant capabilities that this paradigm should provide is the ability of applications and services to adapt themselves and to evolve in reaction to unexpected changes of, e.g., technology, regulations, requirements, usage contexts, market opportunities. In the seminar, we will present a framework that we are developing in Trento, which supports the adaptation and evolution of service oriented applications developed according to the SOC paradigm. In particular, we will introduce the formal definition of adaptation and evolution adopted by the framework; then we will discuss the capabilities offered by the framework and the open problems in this context.

A lot of work has been done so far in the field of planning for web or software services. In this work, major tasks can be described in a planning framework: modeling of software services leads to a planning domain, their automated composition can be done by plan generation, their monitoring becomes monitoring of plan executions, and adaptation can done by re-planning. Things change radically when we move to the framework envisioned by Future Internet. One of the major promises of the vision of Future Internet is the so called "Internet of Services", where applications "live" in the network and are available to end users as "real services" are available today to consumers in everyday life. According to this vision, software services are just software components that provide electronic access to "real services" (e.g., a software service for travel booking allows us to access the actual service behind it, namely "the possibility of traveling"). "Real services" are however very different from the corresponding software services, since they differ in their main characteristics, such as their duration, their accessibility, their constraints and conflicts, and their connection with the real world, which makes them highly dynamic. This new vision requires a shift in the research approach, as well as in the corresponding planning framework: Modeling should describe how the use of real services affects their consumers; Composition does not consist anymore in the generation of a new composed service, it becomes a task that finds relations among services based on emergent needs, constraints, opportunities of the consumers; Monitoring should not check software executions but rather focus on properties of the physical environment where the real services operate; Adaptation should move from reaction to changes in software services to reaction to changes in real services, in the physical environment where they operate, and to users' behaviors. In this talk, I will first describe an approach to planning for software services, and I will then discuss some new research challenges for the future internet of services and how they are related to planning.

In the development of reactive systems with nondeterministic densely-valued temporal parameters, qualitative verification and quantitative evaluation play complementary roles, supporting the identification of feasible behaviors and their association with a measure of probability. Though inherently coupled in the application perspective, the two aspects yield contrasting needs that resulted in separate formalisms and techniques developed upon different theoretical grounds. We report the results of our research towards a unified approach of the two aspects based on the method of stochastic state classes, which extends state space analysis based on Difference Bounds Matrix zones (DBM) with the symbolic calculus of a density-function providing a measure for the probability of individual states. To this end, we extend Time Petri Nets by associating a general probability distribution to the static firing interval of each nondeterministic transition, and we explain how this stochastic information induces a probability distribution for the states contained within a DBM class and how this probability evolves in the enumeration of the reachability relation among classes. In particular, we show that the state-density function accepts a continuous piecewise representation over a partition in DBM-shaped subdomains, we develop a closed-form symbolic calculus of state-density functions under the assumption that transitions in the sTPN model have expolynomial distributions over possibly bounded intervals, and we provide an efficient approximation approach based on Bernstein Polynomials. % This enables the construction of a stochastic transition system that supports correctness verification based on the theory of TPNs, provides a measure of probability for each feasible run, enables steady-state analysis based on Markov Renewal Theory.

Christel Baier, Technische Universitaet Dresden Automata-based model checking relies on a representation of the system and the properties to be verified by finite-state automata. In the classical setting, nondeterministic automata are used for both the system and the properties, and verification amounts analyzing the product of these two nondeterministic automata by means of graph algorithms. In this talk, we address the automata-based approach for verifying randomized systems modeled by some kind of probabilistic automata. Technical problems in the definition of the product arise when dealing with nondeterministic automata for the property to be verified. One solution is to switch to deterministic automata for the requirements, but this can cause a double exponential blow-up for the construction of an automata for a given logical formula (e.g., LTL) formalizing the requirements. An alternative obvious idea is the use of a probabilistic automata representing the properties. This, however, leads to the undecidability of the verification problem. Nevertheless there are some special instances of the verification problem that can be solved algorithmically in an elegant way using probabilistic automata for both the system and the property.

Weighted automata are used to describe quantitative properties in various areas such as probabilistic systems, image compression and speech-to-text processing. The abstract behaviour of these automata is usually expressed in terms of weighted languages (also called formal power series), i.e., functions assigning to each word (in some alphabet) a weight (in some semiring). Another abstract behaviour can be expressed in terms of weighted bisimilarity that, differently from the weighted-language semantics, takes into account the full branching structure. In this talk, we show that (weighted) language semantics naturally arises from "linear coalgebras" on "vector spaces", while bisimilarity arises from "coalgebras" on "sets". These observations are also crucial for defining some algorithms for computing these semantics.

The convergence between computer science and biology occurred in successive waves, involving deeper and deeper concepts of computing. The current situation makes computer science a suitable candidate for becoming a philosophical foundation for systems biology with the same importance as mathematics, chemistry and physics. However, this significant opportunity is not a free lunch. New developments and a strong integration of different fields of computing are needed to face the challenges of systems biology. One of these developments is that of a complex and expanding applicative domain that can open entirely new avenues of research in computing and eventually help it become a natural, quantitative science. The main characteristic of highly parallelism and interaction-driven dynamics of biological systems make the conceptual and software framework developed for biological systems amenable to model, simulate and analyse any complex system whose evolution is determined by the interaction of its sub-components. Therefore, economics, ecology, sociology and computing systems themselves are suitable applicative domains. More info in "Algorithmic Systems Biology", Communications of the ACM, 52(5):80-88, May 2009.

The linkage between research, innovation and education (the so called knowledge dimensions) is gaining momentum in the European social and economic landscape. Most of European challenges and related opportunities are heavily affected by our capability to consolidate new models where the three dimensions of knowledge can fertilise each other in the framework of a sustainable economy. The talk is offering some reflection on these subjects by elaborating on the preliminary actions carried out by the European Institute of Innovation and Technology

Sessions are a common and widespread mechanism of interaction in distributed architectures. The processes willing to interact establish a connection on a shared public channel. In this connection they agree on some private channel on which to have a conversation, dubbed session. The conversation follows a given protocol which describes the kind and order of the messages exchanged on the private channel. The messages exchanged during a session may be synchronisation signals, basic values (e.g., integers, booleans, strings), names of public channels (those used to start sessions), or even names of private channels of already started sessions. In the last case one speaks of delegation since by sending to some other process the private channel of a session, the process delegates the receiver to continue that session. Session types describe the sequences of messages exchanged on a private session channel and their possible branching based on labels: they prevent communication mismatches and session deadlocks. The aim of this talk is to give an overview of sessions/session types and some hints on new proposals for incorporating secure information flow requirements within session types.

Wireless Vehicular Ad Hoc Networks (VANETs) have received an explosive attention under a research viewpoint in recent years, and a number of research groups worldwide are making efforts to explore the potential of vehicular communication as the enabling factor for a novel set of pervasive services and applications. This is also testified by the high number of recent and ongoing EU and US research projects in this field. This survey illustrates a quick tour on the most challenging issues that have been considered in recent researches, and on some open problems that would need additional efforts and research solutions. Specifically, this survey will focus on the MAC and Network protocol layers, by introducing the specific assumptions, limitations and potential of the VANET scenarios, and by exploring the most significant milestones so far achieved under a protocol design and optimization viewpoint. These guidelines are based on the overall evaluation of recent research results, projects, standards and directions for exploitation of the VANET potential under a service level viewpoint.

In service oriented computing, different instances of the same service may be available at a particular moment. Usually, a particular client is aimed at interacting with just one specific instance at a time. Consequently, clients need to be able to identify service instances. Correlation sets are a programming primitive that allows instance identification in orchestration languages. A correlation set is a set of properties (i.e., values carried on by messages) that are used to associate each received message with ``a unique'' process instance: every time a service receives a message, it inspects its content and determines a unique service instance that should handle the received message. If this is not possible (no instance or several instances are candidate), then the service raises an exception. In this talk we will present a formal model for correlation sets that accounts also for correlation exceptions. We also characterise a class of correlation exceptions, called avoidable, that can be prevented during service design. We also propose a type system that guarantees that orchestrators are free from avoidable exceptions.

In this talk we discuss the energy savings that can be obtained with the energy-aware cooperative management of the cellular access networks of the operators that offer service over the same area. We show that a huge amount of energy can be saved by using all networks in high traffic conditions, but progressively switching off networks during the periods when traffic decreases, and eventually becomes so low that the desired quality of service can be obtained with just one network. When a network is switched off, its customers are allowed to roam over those that remain powered on. Several alternatives are studied, as regards the traffic profile, the switch-off pattern, the energy cost model, and the roaming policy.

A variant of Rate Transition Systems (RTS) is introduced and used as the basic model for defining stochastic behaviour of processes and for associating Continuous Time Markov Chains to process terms. The transition relation used in our variant associates to each process, for each action, the set of possible futures paired with a measure indicating their rates.We show how RTS can be used for providing the operational semantics of stochastic extensions of classical formalisms, namely CSP and CCS. We also show that our semantics for stochastic CCS guarantees associativity of parallel composition. Similarly, in contrast with the original definition by Priami, we argue that a similar approach for defining the semantics of stochastic pi-calculus guarantees associativity of parallel composition.

The success of Web related technologies is leading to the implementation of large networked systems that support heterogeneous, possibly critical, services. Dynamic capacity management of these services would increase efficiency and business productivity, but similar processes are difficult to be implemented in contexts characterized by extreme variability of workloads and resource states to the extent that it is difficult to identify stationary periods. We propose an innovative multi-phase methodology that is based on stochastic representations of the resource measures and on accurate models for positioning the present and future state of the system resources with respect to their capacities. These models represent the basis of several runtime decision algorithms that are oriented to load balancing, access control, anomaly detection, energy saving. This research area is characterized by various open issues that will be outlined at the end of the talk.

Abstract Reliability is a critical issue in multi-organizational, distributed applications. Design by Contract traditionally addresses reliability by elaborating type signatures for sequential programs centring on asymmetric procedural invocations. This talk will present a generalisation of the Design by Contract paradigm to multiparty distributed applications each using one or more complex, and possibly long-running, application-level protocols. The main contribution is an assertion method for distributed multiparty interactions centring on the notion of global assertion, which specifies constraints on a whole interaction scenario by elaborating multiparty session types.