Search

Predicate-based communication allows components of a system to send messages and requests to ensembles of components that are determined at execution time through the evaluation of a predicate, in a multicast fashion. Predicate-based communication can greatly simplify the programming of autonomous and adaptive systems. We present a stochastically timed extension of the Software Component Ensemble Language (SCEL) that was introduced in previous work. Such an extension allows for quantitative modelling and analysis of system behaviour (e.g. performance) but rises a number of non-trivial design and formal semantics issues with different options as possible solutions at different levels of abstraction.

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.

We study the variations in two dimensional (2D) pointing behaviour of a group of subjects by means of capturing their movement traces in an automatic way with the Mimio device. Such traces can 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 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.

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.

An abstract is not available.