Usable-by-Construction: a formal framework

We propose here to look at how abstract a model of a usable system can be, but still say something useful and interesting, so this paper is an exercise in abstraction and formalisation, with usability-of-design as an example target use. We take the view that when we claim to be designing a usable system we have, at the very least, to give assurances about its usability properties. This is a very abstract notion, but provides the basis for future work, and shows, even at this level that there are things to say about the (very concrete) business of designing and building usable, interactive systems. Various forms of verification and validation can provide a high level of assurance but it can be very costly, and there is clearly a lot of resistance to doing things this way. In this paper, we introduce the idea of usable-by-construction, which adopts and applies the ideas of correct-by-construction to (very abstractly) thinking about usable systems. We give a set of construction rules or tactics to develop designs of usable systems, and we also formalize them into a state suitable for, for example, a proof assistant to check claims made for the system as designed. In the future, these tactics would allow us to create systems that have the required usability properties and thus provide a basis to a usable-by-construction system. Also, we should then go on to show that the tactics preserve properties by using an example system with industrial strength requirements. And we might also consider future research directions.