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.

翻译：我们在此探讨可用系统模型的抽象程度，以及其仍能提供有用且有趣见解的可能性。因此，本文是一项关于抽象化与形式化的实践，并以设计可用性作为示例目标。我们认为，当声称正在设计一个可用系统时，至少需要对其可用性属性提供保证。这是一个非常抽象的概念，但为未来工作奠定了基础，并且表明了即使在此层次上，我们也有关于（非常具体的）设计与构建可用交互系统工作的问题需要阐述。各种形式的验证与确认虽能提供高水平的保证，但成本极高，且显然存在诸多对此方式的抵触。本文引入了“可用性构建”的概念，将“正确性构建”的思想采纳并应用于（非常抽象地）思考可用系统。我们给出了一套用于开发可用系统设计的构建规则或策略，并将其形式化为适用于（例如）证明助手验证系统设计声明的状态。未来，这些策略将使我们能够创建具有所需可用性属性的系统，从而为“可用性构建”系统奠定基础。此外，我们还需通过一个具有工业级需求的示例系统，证明这些策略能够保持属性。同时，我们也会探讨未来的研究方向。