No Cover Image

E-Thesis 344 views 103 downloads

Structural usability techniques for dependable HCI. / Andy Gimblett

Swansea University Author: Andy Gimblett

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...

Full description

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!
first_indexed 2018-08-02T18:55:22Z
last_indexed 2018-08-03T10:10:54Z
id cronfa42714
recordtype RisThesis
fullrecord <?xml version="1.0"?><rfc1807><datestamp>2018-08-02T16:24:30.2114013</datestamp><bib-version>v2</bib-version><id>42714</id><entry>2018-08-02</entry><title>Structural usability techniques for dependable HCI.</title><swanseaauthors><author><sid>998895277c3cff404107143cf2fbc18e</sid><ORCID>NULL</ORCID><firstname>Andy</firstname><surname>Gimblett</surname><name>Andy Gimblett</name><active>true</active><ethesisStudent>true</ethesisStudent></author></swanseaauthors><date>2018-08-02</date><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.</abstract><type>E-Thesis</type><journal/><journalNumber></journalNumber><paginationStart/><paginationEnd/><publisher/><placeOfPublication/><isbnPrint/><issnPrint/><issnElectronic/><keywords>Computer science.</keywords><publishedDay>31</publishedDay><publishedMonth>12</publishedMonth><publishedYear>2014</publishedYear><publishedDate>2014-12-31</publishedDate><doi/><url/><notes/><college>COLLEGE NANME</college><department>Computer Science</department><CollegeCode>COLLEGE CODE</CollegeCode><institution>Swansea University</institution><degreelevel>Doctoral</degreelevel><degreename>Ph.D</degreename><apcterm/><lastEdited>2018-08-02T16:24:30.2114013</lastEdited><Created>2018-08-02T16:24:30.2114013</Created><path><level id="1">Faculty of Science and Engineering</level><level id="2">School of Mathematics and Computer Science - Computer Science</level></path><authors><author><firstname>Andy</firstname><surname>Gimblett</surname><orcid>NULL</orcid><order>1</order></author></authors><documents><document><filename>0042714-02082018162516.pdf</filename><originalFilename>10807483.pdf</originalFilename><uploaded>2018-08-02T16:25:16.1700000</uploaded><type>Output</type><contentLength>12371048</contentLength><contentType>application/pdf</contentType><version>E-Thesis</version><cronfaStatus>true</cronfaStatus><embargoDate>2018-08-02T16:25:16.1700000</embargoDate><copyrightCorrect>false</copyrightCorrect></document></documents><OutputDurs/></rfc1807>
spelling 2018-08-02T16:24:30.2114013 v2 42714 2018-08-02 Structural usability techniques for dependable HCI. 998895277c3cff404107143cf2fbc18e NULL Andy Gimblett Andy Gimblett true true 2018-08-02 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. E-Thesis Computer science. 31 12 2014 2014-12-31 COLLEGE NANME Computer Science COLLEGE CODE Swansea University Doctoral Ph.D 2018-08-02T16:24:30.2114013 2018-08-02T16:24:30.2114013 Faculty of Science and Engineering School of Mathematics and Computer Science - Computer Science Andy Gimblett NULL 1 0042714-02082018162516.pdf 10807483.pdf 2018-08-02T16:25:16.1700000 Output 12371048 application/pdf E-Thesis true 2018-08-02T16:25:16.1700000 false
title Structural usability techniques for dependable HCI.
spellingShingle Structural usability techniques for dependable HCI.
Andy Gimblett
title_short Structural usability techniques for dependable HCI.
title_full Structural usability techniques for dependable HCI.
title_fullStr Structural usability techniques for dependable HCI.
title_full_unstemmed Structural usability techniques for dependable HCI.
title_sort Structural usability techniques for dependable HCI.
author_id_str_mv 998895277c3cff404107143cf2fbc18e
author_id_fullname_str_mv 998895277c3cff404107143cf2fbc18e_***_Andy Gimblett
author Andy Gimblett
author2 Andy Gimblett
format E-Thesis
publishDate 2014
institution Swansea University
college_str Faculty of Science and Engineering
hierarchytype
hierarchy_top_id facultyofscienceandengineering
hierarchy_top_title Faculty of Science and Engineering
hierarchy_parent_id facultyofscienceandengineering
hierarchy_parent_title Faculty of Science and Engineering
department_str School of Mathematics and Computer Science - Computer Science{{{_:::_}}}Faculty of Science and Engineering{{{_:::_}}}School of Mathematics and Computer Science - Computer Science
document_store_str 1
active_str 0
description 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.
published_date 2014-12-31T03:53:30Z
_version_ 1763752658282217472
score 11.01297

Similar Items