Formal Analysis of Evolving Resilient Usable Systems



International Mini-project in the context of the

EU Network of Excellence ReSIST, 2008
Contract Number: 026764
Pisa, IT
Thursday May 19, 2009.

  • Project Coordinator
  •   M.Massink AT isti.cnr.it

Research in the context of the FAERUS Mini-project has focused on two main issues. The first concerned a formal model-based analysis to compare the resilience of two different interaction techniques, `Drag and Drop’ and `Speak and Drop’, for removing icons from a screen to the presence of external interrupts. The models in this work have been specified in the process algebra PEPA (Performance Evaluation Process Algebra) and analysed with the stochastic model checker PRISM. The latter also provides automatic verification of measures, expressed as logical formulae, that concern rewards associated with actions. This allows for the analysis of the resilience of the interaction techniques to external interrupts by studying how the number of drop-actions changes when the interupt rate increases. For the models, knowledge from different domains has been brought together. The model of the user has been based on cognitive theory and human factors analysis. The model of the system used timing aspects obtained from literature such as time needed for speech processing. The models predict that the interaction technique ‘Speak and Drop’ is more resilient to external interrupts (a pop-up window in this case) than the traditional `Drag and Drop’. This is as expected and can be explained by the fact that with `Drag and Drop’ the time during which the activity can be interrupted (which requires the user to start from the beginning for that icon) is longer in comparison with `Speak and Drop’. This effect is even stronger if a real-time speech recogniser is considered.

The second issue addressed the problem of to what extent recently developed scalable formal modelling techniques can be applied to analyse the behaviour of a large number of users in (possibly smart) environments and the effect that their behaviour may have on the performance of such environments. The first case study focused on the performance aspects of different file access policies in the context of an industrial collaborative design application thinkteam. Two such policies have been compared : one based on a retry policy and one in which users could subscribe to a file and wait for it in a queue. Stochastic models have been analysed in which 90 users compete for 30 files in which different usage patterns have been addressed such as different mean time to edit a file and different mean time between file access. For the modelling PEPA has been used and for the analysis the scalable Fluid Flow technique which is based on solving sets of Ordinary Differential Equations that have been derived in an automatic way from the PEPA specification with help of the PEPA workbench developed at the University of Edinburgh. Given the size of the state space of the PEPA model for the given number of visitors and files it contains, the model would not be amenable to stochastic model checking. It has been shown that for what concerns the transient aspects of the system the Fluid Flow approach provides a time-efficient alternative leading to results that show good correspondence to those obtained with the much more time-consuming stochastic simulation approach.

A more extended case study has applied the same scalable technique to the analysis of the behaviour of large groups of visitors that are visiting a smart environment that is provided with a dynamic signage system. Alternative models of interaction within the smart environment have been explored. The first focused on the individual within the environment and the second provided a quantitative analysis of the impact of the designed environment on collective behaviour. A scenario has been modelled in which groups of visitors move through a building from room to room towards a final destination. Each room is provided with a display with a limited number of slots to provide routing information to the visitors, and with a number of places to sit. Fluid Flow analysis has shown to be a useful technique to provide in a timely way transient information on the model such as resource usage and arrival time of visitors. The case-study served as a feasibility study of the application of the Fluid Flow analysis to more complicated environments such as airports and stadions. Also scalability with respect to the number of rooms has been analysed : a model of a building with 26 rooms and a few hundred visitors has been successfully analysed in a few minutes on a normal desktop PC.

Last update: May 19, 2009