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:

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: