E-Thesis 427 views 124 downloads
Structural usability techniques for dependable HCI. / Andy Gimblett
Swansea University Author: Andy Gimblett
-
PDF | E-Thesis
Download (11.89MB)
Abstract
Since their invention in the middle of the twentieth century, interactive computerised systems have become more and more common to the point of ubiquity. While formal techniques have developed as tools for understanding and proving things about the behaviour of computerised systems, those that invol...
| Published: |
2014
|
|---|---|
| Institution: | Swansea University |
| Degree level: | Doctoral |
| Degree name: | Ph.D |
| URI: | https://cronfa.swan.ac.uk/Record/cronfa42714 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| Abstract: |
Since their invention in the middle of the twentieth century, interactive computerised systems have become more and more common to the point of ubiquity. While formal techniques have developed as tools for understanding and proving things about the behaviour of computerised systems, those that involve interaction with human users present some particular challenges which are less well addressed by traditional formal methods. There is an under-explored space where interaction and the high assurances provided by formal approaches meet. This thesis presents two techniques which fit into this space, and which can be used to automatically build and analyse formal models of the interaction behaviour of existing systems. Model discovery is a technique for building a state space-based formal model of the interaction behaviour of a running system. The approach systematically and exhaustively simulates the actions of a user of the system; this is a dynamic analysis technique which requires tight integration with the running system and (in practice) its codebase but which, when set up, can proceed entirely automatically. Theorem discovery is a technique for analysing a state space-based formal model of the interaction behaviour of a system, looking for strings of user actions that have equivalent effects across all states of the system. The approach systematically computes and compares the effects of ever-longer strings of actions, though insights can also arise from strings that are almost equivalent, and also from considering the meaning of sets of such equivalences. The thesis introduces and exemplifies each technique, considers how they may be used together, and demonstrates their utility and novelty, with case studies. |
|---|---|
| Keywords: |
Computer science. |
| College: |
Faculty of Science and Engineering |