Antonio Cerone and Norzima Elbegbayan

Model-checking Driven Design of Interactive Systems

Keywords:

formal verification, human behaviour, usability, user error, social computing, process calculi, model-checking.

Abstract:

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's 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.

Download:

Preliminary Version:

• PDF - Access Restricted UNU-IIST Academics and Authorised Users
• PDF - Internal Access from UNU-IIST LAN: ~antonio/unuiist/share/papers/2006-fmis-ce.pdf