A populations approach to ubicomp systems design

Formal Analysis

We are working on new techniques for formal modelling and analysis of representations real-life usage patterns of software systems (mobile applications in particular). The representations are based on a stochastic abstraction of the populations of software in use and user behaviours. We have hypothesised that temporal logic reasoning over probabilistic models inferred from user traces can aid software developers, evaluators, and users by:

• providing insights into usage behaviours, including differences and similarities between different usage styles,
• predicting user behaviours, and
• recommending future application development and redesign/redevelopment.

We propose that formal, probabilistic analysis of inferred patterns of logged app usage is key, and we refer to these patterns as activity patterns. Our concept of population is therefore based on inferred temporal behaviours, i.e. activity patterns, rather than on static or slowly changing user attributes such as gender and age. The novelty of our approach is realising the concept of population through a combination of three powerful ingredients:

• inference of Markov models of activity patterns from automatically logged data on user sessions,
• characterisation of the activity patterns by probabilistic temporal logic properties using model checking, and
• longitudinal analysis of usage data drawn from different time cuts (e.g. logged sessions over the first day, first month, second month, etc.).

---