Search

This deliverable reports on the WP2 activities that have been conducted during months 25-36. In Task 2.1 we further pursued the investigation on the theoretical foundations of the distributed implementation of connectors, including expressiveness issues for classes of dynamic BIP connectors and further investigating the issue of parallel executions for BIP systems with time constraints. We fur- ther continued the study of coalgebraic models for our resource-aware calculus we also discussed last year, and chosen peer-to-peer overlay as a case study. Finally, we freshly tackled nominal automata, investigating the issue of regular expressions for such automata. In Task 2.2 we focussed mostly on the soft constraints paradigm. A more theoretical investigation concerned the laws for behavioral equivalence in SCCP, the best-known language based on constraints. A more applicative outlook lead to the development of a technique based on the orchestration of declarative and procedural knowledge for solving locally optimization problems that are global. In Task 2.3 we kept on investigating about issues related to game semantics for agents, focusing on energy trading scenarios, and looking at the self-organizational aspects of an agent-based system managing the interactions among prosumers introduced early in the project. Furthermore, we pursued the study of coalgebraic semantics for the stochastic calculus introduced early in the project, whose work was previously reported in the sections of Deliverables D2.1 and D2.2 devoted to Task 2.1. The deliverable is organized around the above structure of themes. Each subsection includes a short description of the novelty and offer pointers towards future work. A concluding section offers some general remarks on the overall satisfaction of the objectives, on the influences from and towards other work packages, and some comments on the foreseen developments for the forthcoming year.

Emergent phenomena occur due to the pattern of non-linear and distributed local interactions between the elements of a system over time. Surprisingly, agent based crowd models in which the movement of each individual follows a limited set of simple rules often re-produce quite closely the emergent behaviour of crowds that can be observed in reality. An example of such phenomena is the spontaneous self-organisation of drinking parties in the squares of cities in Spain, also known as ``El Botell'on" (by Rowe and Gomez 2003). We revisit this case study providing an elegant stochastic process algebraic model in Bio-PEPA amenable to several forms of analyses among which simulation and fluid flow analysis. We show that a fluid flow approximation, i.e. a deterministic reading of the average behaviour of the system, can provide an alternative and efficient way to study the same emergent behaviour as that explored by Rowe and Gomez in 2003 where simulation was used instead. Besides empirical evidence also an analytical justification is provided for the good correspondence found between simulation results and the fluid flow approximation. Scalability features of the fluid flow approach may make it particularly useful when studying models of more complex city topologies with very large populations.

While the cost of deploying a smart environment is likely to be high, the benefits of such systems are hard to quantify and predict. The potential for expensive failure is therefore considerable. This paper is concerned with how formal models of smart environments might be used to explore the consequences of the technology on users of the environment before deployment. Alternative models of interaction within smart environments are explored. The first focuses on the individual within the environment and the second provides an exploration of the impact of the designed environment on collective behaviour. It applies a recent approach that provides a quantitative analysis of systems with a very large number of entities with similar behaviour. The paper argues that there are particular properties relating to implicit interaction in immersive systems and to issues of crowd system interaction and discusses how these properties should be analysed. The relationship between these models is discussed and an agenda is established for tool supported methodology. This paper is concerned with an engineering approach to the analysis of human aspects of smart environments.

In this paper we present how Rate Transition Systems (RTS) can be used as a unifying framework for the definition of the semantics of stochastic process algebras. RTS facilitate the compositional definition of such semantics exploiting operators on the next state functions which are the functional counterpart of classical process algebra operators. We apply this framework to representative fragments of major stochastic process calculi including TIPP, PEPA and IML, and show how they solve the issue of transition multiplicity in a simple and elegant way. We, moreover, show how RTS help describing different languages, their differences and their similarities. For each calculus, we also show the formal correspondence between the RTS semantics and the standard SOS one.

In this paper we present how Rate Transition Systems (RTS) can be used as a unifying framework for the definition of the semantics of stochastic process algebras. RTS facilitate the compositional definition of such semantics exploiting operators on the next state functions which are the functional counterpart of classical process algebra operators. We apply this framework to representative fragments of major stochastic process calculi including TIPP, EMPA, PEPA and IML, and show how they solve the issue of transition multiplicity in a simple and elegant way. We, moreover, show how RTS help describing different languages, their differences and their similarities. For each calculus, we also show the formal correspondence between the RTS semantics and the standard SOS one.

In many modern working environments interruptions are commonplace as users must temporarily suspend their current task in order to complete an unexpected intervening activity. As users are faced with more and more sources of information competing for users' attention at any time, it is becoming increasingly important to understand how interruptions affect our abilities to complete tasks. The present work introduces a new perspective for the research in the field by employing analytical, model-based, techniques that are informed by well-established cognitive theories and experimental data available in the literature. We propose stochastic modelling and model checking to predict measures of the disruptive effects of interruptions to two well-known interaction techniques: Drag 'n Drop and Speak 'n Drop. The approach also provides a way to compare the resilience of different interaction techniques to the presence of external interruptions that users need to handle. The results obtained are in a form that allows validation with results obtained by empirical studies involving real users.

Global (or network-aware) computing entails large-scale networks of computers performing tasks in a cooperative and coordinated manner. Programming and modeling languages such as KLAIM focus on key functional aspects of global computing such as distribution awareness, (code and agent) mobility, and privacy aspects. This paper instead concentrates on their performance and dependability aspects. It proposes STOKLAIM, an extension of KLAIM which permits the description of random phenomena such as spontaneous computer crashes and spurious network hick ups. The operational semantics of STOKLAIM is based on continuous-time Markov chains. The approach is illustrated by modeling the spreading of a virus through a network.