Is my configuration any good: checking usability in an interactive sensor-based activity monitor

We investigate formal analysis of two aspects of usability in a deployed interactive, configurable and context-aware system: an event-driven, sensor-based homecare activity monitor system. The system was not designed from formal requirements or specification: we model the system as it is in the context of an agile development process. Our aim was to determine if formal modelling and analysis can contribute to improving usability, and if so, which style of modelling is most suitable. The purpose of the analysis is to inform configurers about how to interact with the system, so the system is more usable for participants, and to guide future developments. We consider redundancies in configuration rules defined by carers and participants and the interaction modality of the output messages.Two approaches to modelling are considered: a deep embedding in which devices, sensors and rules are represented explicitly by data structures in the modelling language and non-determinism is employed to model all possible device and sensor states, and a shallow embedding in which the rules and device and sensor states are represented directly in propositional logic. The former requires a conventional machine and a model-checker for analysis, whereas the latter is implemented using a SAT solver directly on the activity monitor hardware. We draw conclusions about the role of formal models and reasoning in deployed systems and the need for clear semantics and ontologies for interaction modalities.