Model-checking Driven Design of Interactive Systems

This paper describes a model-checking based methodology to detect systematic errors commonly made by non-expert users. The human and computer components of the systems are modelled separately. The human component consists of a general model of the user's cognitively plausible behaviour, which can be then refined into specific instances of behaviour that reflect relevant aspects of users' personalities and skills. We consider, as a case study, a formal model of an online interactive tool that enables conference attendees to share thoughts and reactions and select matching attendees to start communication with. Starting from the initial system design, a model-checking technique is used to highlight system vulnerabilities that arise from interactions with non-expert users and may lead to security violations. The results of the analysis are exploited to improve the design by introducing safeguards that reduce or even prevent security violations.