Search

We present FlyFast, a recently introduced on-the-fly mean field model checker for the verification of time-dependent probabilistic properties of individual objects in the context of large populations. An example of its use is illustrated analysing a push-pull gossip protocol. Such protocols form the basis on top of which many smart collective adaptive systems are built. Typical properties are the replication of a fresh data element throughout a network, the coverage of the network, and the time to convergence. more...

We present a novel method to analyse swarm robotics sys- tems based on Bio-PEPA. Bio-PEPA is a process algebraic language originally developed to analyse biochemical systems. Its main advantage is that it allows different kinds of analyses of a swarm robotics system starting from a single description. In general, to carry out different kinds of analysis, it is necessary to develop multiple models, raising issues of mutual consistency. With Bio-PEPA, instead, it is possible to perform stochastic simulation, fluid flow analysis and statistical model checking based on the same system specification. This reduces the complexity of the analysis and ensures consistency between analysis results. Bio-PEPA is well suited for swarm robotics systems, because it lends itself well to modelling distributed scalable systems and their space-time characteris- tics. We demonstrate the validity of Bio-PEPA by modelling collective decision-making in a swarm robotics system and we evaluate the result of different analyses. more...

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 reproduce 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 Botellon" [20]. 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 in [20] 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. more...

In this paper we present an integration of PLinda, a probabilistic extension of Linda, and StoKlaim , a stochastic extension of KLAIM. In the resulting language, StoPKlaim , the execution time of coordination primitives is modeled by means of exponentially distributed random variables, as in StoKlaim , the choice of the primitive to be executed among conflicting ones is thus resolved by the race condition principle, and the choice of the tuple to be retrieved by a single input/read operation in case of multiple matching tuples is governed by the weight-based probabilistic access policy of PLinda. The language represents a natural development and integration of previous results of the SENSORIA Project in the area of probabilistic and time-stochastic extensions of Tuple Space based coordination languages. The formal operational semantics of StoPKlaim is presented and an example of modeling is provided. more...

International audience; In many modern working environments interruptions are commonplace as users must temporarily suspend a task to complete an unexpected intervening activity. As users are faced with more and more sources of information competing for their attention, it is becoming increasingly important to understand how interruptions affect their abilities to complete tasks. This paper introduces a new perspective for research in this field by employing analytical, model-based techniques that are informed by well-established cognitive theories and empirical 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 obtained results are in a form that allows validation with results obtained by empirical studies involving real users. more...

We study the variations in two dimensional (2D) pointing tasks on a traditional white board of a group of subjects by means of capturing their movement traces in an automatic way with the Mimio device. Such traces provide detailed insight in the variability of 2D pointing relevant for example for the design of computer vision based gestural interaction. This study provides experimental evidence that for medium large distances Fitts' model, and Welfords and Shannons variants, continue to show a linear relationship between movement time (MT) and the index of difficulty (ID) with a high correlation for the ranges considered. The expected increased sensitivity to changes in ID for these larger distances are confirmed. Nearly all movements show three phases: a planning phase, a ballistic phase and an adjustment phase. Finally, we show that the arrival time at the target resembles a log-normal distribution. more...

Mobile users generate a number of new problems by changing the context of interaction with the system. While context has always been relevant to interaction, the fact this can change, and the fact that tasks may be dependant on these contexts adds a new dimension to the design problem. Furthermore in some cases applications should be able to adapt to be pertinent to the current context, adding to the complexity of the applications to be constructed. With regard to “ambient” interaction, where systems are attempting to intelligently and unobtrusively help the user, understanding the user's intentions and providing relevant and adequate responses is a new problem. Furthermore, supporting the construction of such applications provides an additional challenge. more...

Stochastic model checking is a recent extension of traditional model-checking techniques for the integrated analysis of both qualitative and quantitative system properties. In this paper we show how stochastic model checking can be conveniently used to address a number of usability concerns that involve quantitative aspects of a user interface for the industrial groupware system thinkteam. thinkteam is a ready-to-use Product Data Management application developed by think3. It allows enterprises to capture, organise, automate, and share engineering product information and it is an example of an asynchronous and dispersed groupware system. Several aspects of the functional correctness, such as concurrency aspects and awareness aspects, of the groupware protocol underlying thinkteam and of its planned publish/subscribe notification service have been addressed in previous work by means of a traditional model-checking approach. In this paper we investigate the trade-off between two different design options for granting users access to files in the database: a retrial approach and a waiting-list approach and show how stochastic model checking can be used for such analyses. more...

In this paper an extension of a behavioural subset of UML Statecharts for modeling mobility issues is proposed. In this extension we relax the unique association between each Statechart – in a collection of Statecharts modeling a system – and its input-queue and we allow the use of (queue) name variables in communication actions. The resulting communication paradigm is much more flexible than the standard asymmetric one and is well suited for the modelling of mobility-oriented as well as fault tolerant systems. more...

I:Selection of Papers Presented at 5thSPIN99.- Integrated Formal Verification: Using Model Checking with Automated Abstraction, Invariant Generation, and Theorem Proving.- Runtime Efficient State Compaction in Spin.- Distributed-Memory Model Checking with SPIN.- Partial Order Reduction in Presence of Rendez-vous Communications with Unless Constructs and Weak Fairness.- Divide, Abstract, and Model-Check.- II: Papers Presented at 6thSPIN99.- Formal Methods Adoption: What's Working, What's Not!.- Model Checking for Managers.- Xspin/Project - Integrated Validation Management for Xspin.- Analyzing Mode Confusion via Model Checking.- Detecting Feature Interactions in the Terrestrial Trunked Radio (TETRA) Network Using Promela and Xspin.- Java PathFinder A Translator from Java to Promela.- VIP: A Visual Interface for Promela.- Events in Property Patterns.- Assume-Guarantee Model Checking of Software: A Comparative Case Study.- A Framework for Automatic Construction of Abstract Promela Models.- Model Checking Operator Procedures.- Applying Model Checking in Java Verification.- The Engineering of a Model Checker: the Gnu i-Protocol Case Study Revisited..- Embedding a Dialect of SDL in PROMELA.- dSPIN: A Dynamic Extension of SPIN. more...