Research in the context of the FAERUS project has investigated the feasibility of the use of stochastic process algebras for the modelling and analysis of resilience and scalability issues in ubiquitous systems. In particular a user centered model-based approach to system design has been put forward that includes modelling and automatic analysis of non-functional requirements and the evaluation of the diversity of interaction techniques with respect to their resilience to external interrupts.

The final objectives of the project, i.e. the development and analysis of the relative models and the application of the methods to a wider range of case-studies, have also been achieved. The case study on interrupts has lead to a method that shows how the cognitive theory ICS and experimental results on Human performance can be used to build integrated syndetic models of interaction. The analysis of such models by means of a stochastic model-checker that provides a stochastic temporal logic with which also measures involving rewards can be conveniently expressed, has produced very encouraging results. Also the form in which the results are produced, namely in terms of the number of drops that a user may perform on average, given a certain frequency of external interrupts, makes that the models can be validated against experimental results obtained in experiments with real human users. This is part of the future work that we are planning to perform in the context of some future project.

The case study on collaborative systems has also provided interesting results. Starting from simple process algebraic models of the basic entities of the system we have been able to analyse quantitative usability aspects of different file access policies for models with a large number of users and filemanagers which is typical for industrial case-studies. In fact the numbers used in the case-study have been obtained from log-file analysis of an industrial use of the collaborative system under study.

These positive and encouraging results have lead us to the development of a much larger case-study during the last part of the project that addresses the analysis of human flows in smart environments. In particular we have developed both qualitative and quantitative models to assess the correctness and performance aspects of the dynamic signage system GAUDI. We showed how a modular specification in PEPA of a building with rooms and interactive displays can be developed and how Fluid flow analysis can be used to study the flows of large groups  of visitors that move through the building. Finally, we have also developed preliminary prototype software that compiles automatically PEPA models from a description of the architecture of the building (e.g. number of rooms, connections between rooms, routing information, number of slots on each display, number, starting place and final destination of the groups of visitors etc.). This allows for an efficient way to evaluate different and even large configurations. A preliminary test involved several hunderds of visitors moving through 26 rooms. Fluid flow analysis of a configuration of this size took no more than 10 minutes. Of course, the time needed for the analysis may depend on several issues and requires definitely further study. This also holds for a deeper investigation of the current limitations of the use of this technique and to study more in depth whether such limitation could be relaxed in further theoretical developments of the technique.

Last update: May 19, 2009