Probabilistic formal analysis of software usage styles in the wild
Professor Muffy Calder (University of Glasgow)
Tuesday 25th October, 2016 16:00-17:00 Room 507, Boyd Orr Building.
Discrete mathematics and logics are used to analyse the intended behaviour of software systems. Statistical methods are used to analyse the logged data from instrumented systems. So what happens when we instrument software: can we bring the two techniques together to analyse how people actually use software?
But users are difficult -- they adopt different styles at different times! What characterises usage style, of a user and of populations of users, how should we characterise the different styles, how do characterisations evolve over an individual user trace, and/or over a number of sessions over days and months, and how do characteristics of usage inform evaluation for redesign and future design? Can we formalise these concepts and construct effective procedures?
Professor Calder will outline a novel mathematical/computational approach that aims to answer all these questions. The approach is based on discrete space stochastic models, statistical inference of those models, and stochastic temporal logics and model checking for investigating hypotheses about use, all applied to longitudinal sets of logged usage data. The approach is the result of a five year collaboration between software developers, statisticians, HCI, and formal methods experts. She will illustrate by way of a mobile app that is used by tens of thousands of users worldwide; a new version of the app, based on the analysis and evaluation, has just been deployed. This is formal analysis in the wild!