Usable-by-Construction: a formal framework

Fuente: arXiv
Saved in:
Bibliographic Details
Main Author: Reeves, Steve
Format: Preprint
Published: 2024
Subjects:
Online Access:
Tags: Add Tag
No Tags, Be the first to tag this record!
_version_ 1866907829867118592
author Reeves, Steve
author_facet Reeves, Steve
contents 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.
format Preprint
id arxiv_https___arxiv_org_abs_2402_00218
institution arXiv
publishDate 2024
record_format arxiv
spellingShingle Usable-by-Construction: a formal framework
Reeves, Steve
Human-Computer Interaction
Logic in Computer Science
Software Engineering
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.
title Usable-by-Construction: a formal framework
topic Human-Computer Interaction
Logic in Computer Science
Software Engineering
url https://arxiv.org/abs/2402.00218