可用性即构造：一个形式化框架
Usable-by-Construction: a formal framework
AI总结：
本文提出“可用性即构造”形式化框架，将正确性即构造理念应用于可用系统设计，给出构造规则并形式化以支持证明助手验证，旨在确保系统可用性属性。
摘要：
我们在此提出探讨一个可用系统的模型可以抽象到何种程度，同时仍能说出有用且有趣的内容，因此本文是一次抽象与形式化的练习，以设计可用性作为示例目标应用。我们认为，当我们声称在设计一个可用系统时，至少必须对其可用性属性提供保证。这是一个非常抽象的概念，但为未来工作提供了基础，并表明即使在这个层面上，关于设计和构建可用、交互式系统这一（非常具体的）事务，也有可说的内容。各种形式的验证与确认可以提供高水平的保证，但可能代价高昂，而且显然对此方式存在大量抵触。在本文中，我们引入了“可用性即构造”的思想，它将“正确性即构造”的理念采纳并应用于（非常抽象地）思考可用系统。我们给出了一组构造规则或策略，用于开发可用系统的设计，并将它们形式化为适合例如证明助手检查系统设计声明状态的形式。未来，这些策略将使我们能够创建具有所需可用性属性的系统，从而为“可用性即构造”系统提供基础。此外，我们还应通过使用一个具有工业级需求的示例系统来证明这些策略保持属性。我们也可以考虑未来的研究方向。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
