Search

This volume contains the proceedings of the Tenth Workshop on Quantitative Aspects of Programming Languages and Systems (QAPL 2012), held in Tallinn, Estonia, on 31 March and 1 April, 2012. QAPL 2012 was a satellite event of the European Joint Conferences on Theory and Practice of Software (ETAPS 2012).

Emergent phenomena occur due to the pattern of non-linear and distributed local interactions between the elements of a system over time. 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" (Rowe and Gomez 2003). Surprisingly, crowd models in which the movement of each individual follows a very limited set of simple rules often re-produce quite closely the emergent behaviour of crowds that can be observed in reality. In this paper we take a stochastic process algebraic approach to agent based modelling. In this setting, a single stochastic process algebraic model can be used for several forms of analyses among which simulation, stochastic model-checking and fluid flow analysis. Here we revisit the case of self-organisation of crowds in a city. 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 in Rowe and Gomez 2003 where simulation was used instead. Scalability features of this approach may make it particularly useful when studying models of more complex city topologies with very large populations.

Pervasive environments offer an increasing number of services to a large number of people moving within these environments including timely information about where to go and when. People using these services interact with the system but they are also meeting other people and performing other activities as relevant opportunities arise. The design of such systems and the analysis of collective dynamic behaviour of people within them is a challenging problem. In previous work we have successfully explored a scalable analysis of stochastic process algebraic models of smart signage systems. In this paper we focus on the validation of a representative example of this class of models in the context of emergency egress. This context has the advantage that there is detailed data available from studies with alternative analysis methods. A second aim is to show how realistic human behaviour, often observed in emergency egress, can be embedded in the model and how the effect of this behaviour on building evacuation can be analysed in an efficient and scalable way.

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 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.

Product Data Management (PDM) systems support the document management of design processes like those used in the manufacturing industry. They allow enterprises to capture, organise, automate and share engineering information efficiently. Essential aspects of such systems are handling queries on product information and down- and uploading assemblies of related files for modification by designers. The efficiency of such a system as perceived by its users depends on its correct functioning, but also for a significant part on its performance aspects. We apply stochastic model checking in an industrial setting to evaluate a service-oriented extension of the PDM system thinkteam with multiple replicated vaults. We investigate the effect of different quality of service assumptions on the system's usability from a user's perspective, and briefly report on our industrial experience with stochastic model checking.

This chapter is concerned with the modeling and analysis of distributed systems using formal methods.

This paper reports on the fruitful combination of academic experience with formal modelling techniques and industrial experience with requirements exploration. We study the addition of a publish/subscribe notification service to thinkteam, a ready-to-use Product Data Management application developed by think3. thinkteam allows enterprises to capture, organise, automate, and share engineering product information and it is an example of an asynchronous and dispersed groupware system. We define an abstract specification (model) of the groupware protocol underlying thinkteam and augment it with a publish/subscribe notification service. Consequently, we show a number of important correctness properties of the thinkteam model, some of which are also relevant to groupware protocols in general. In particular, we show that by adding a publish/subscribe notification service to thinkteam, the user's awareness of the status of the development of the engineering product and the activities of the design team increases.

A characteristic that many emerging technologies and interaction techniques have in common is a shift towards tighter coupling between human and computer. In addition to traditional discrete interaction, more continuous interaction techniques, such as gesture recognition, haptic feedback and animation, play an increasingly important role. Additionally, many supervisory control systems (such as flight deck systems) already have a strong continuous element. The complexity of these systems and the need for rigorous analysis of the human factors involved in their operation leads us to examine formal and possibly automated support for their analysis. The fact that these systems have important temporal aspects and potentially involve continuous variables, besides discrete events, motivates the application of hybrid systems modelling, which has the expressive power to encompass these issues. Essentially, we are concerned with human-factors related questions whose answers are dependent on interactions between the user and a complex, dynamic system. In this paper we explore the use of hybrid automata, a formalism for hybrid systems, for the specification and analysis of interactive systems. To illustrate the approach we apply it to the analysis of an existing flight deck instrument for monitoring and controlling the hydraulics subsystem.

This paper presents a formal operational semantics for a behavioral subset of UML Statechar Diagrams including a formal proof of its correctness with respect to the UML semantic requirements

Modern information technology is becoming both increasingly ubiquitous and increasingly varied in the possible ways it can interact with the user. With many emerging technologies, interaction with the user is no longer based exclusively on discrete interactions, which are the underlying model for many traditional approaches in HCI (for example, Norman's seven stage model (Norman, 1998). Rather, modem interaction techniques develop towards interfaces where the user is in constant interaction with the computing system, communicating with it by means of gestures, speech and animation as well as discrete communication such as selection by pressing buttons or typing via a keyboard. This development requires new interface design approaches that allow for the analysis of the discrete as well as the continuous aspects of the interface, and that support reasoning about real-time issues. We examine how classical manual control theory can be applied in this area. Conversely, in the area of human control, a shift has occurred away from pure manual control scenarios to more supervisory and mixed control tasks. We believe these two trends have established much common ground between the areas of interactive· systems and human control, and examine some on-going research in this area.