No Cover Image

Conference Paper/Proceeding/Abstract 1011 views 126 downloads

Developing GUI Applications in a Verified Setting

Stephan Adelsberger, Anton Setzer Orcid Logo, Eric Walkingshaw

Dependable Software Engineering. Theories, Tools, and Applications, Volume: 10998, Pages: 89 - 107

Swansea University Author: Anton Setzer Orcid Logo

Check full text

DOI (Published version): 10.1007/978-3-319-99933-3_6

Abstract

Although there have been major achievements in verified software, work on verifying graphical user interfaces (GUI) applications is underdeveloped relative to their ubiquity and societal importance.In this paper, we present a library for the development of verified, state-dependent GUI applications...

Full description

Published in: Dependable Software Engineering. Theories, Tools, and Applications
ISBN: 9783319999326 9783319999333
ISSN: 0302-9743 1611-3349
Published: Cham Springer International Publishing 2018
Online Access: Check full text

URI: https://cronfa.swan.ac.uk/Record/cronfa40967
first_indexed 2018-07-10T15:01:44Z
last_indexed 2022-06-17T02:57:31Z
id cronfa40967
recordtype SURis
fullrecord <?xml version="1.0"?><rfc1807><datestamp>2022-06-16T16:07:58.8486468</datestamp><bib-version>v2</bib-version><id>40967</id><entry>2018-07-10</entry><title>Developing GUI Applications in a Verified Setting</title><swanseaauthors><author><sid>5f7695285397f46d121207120247c2ae</sid><ORCID>0000-0001-5322-6060</ORCID><firstname>Anton</firstname><surname>Setzer</surname><name>Anton Setzer</name><active>true</active><ethesisStudent>false</ethesisStudent></author></swanseaauthors><date>2018-07-10</date><deptcode>MACS</deptcode><abstract>Although there have been major achievements in verified software, work on verifying graphical user interfaces (GUI) applications is underdeveloped relative to their ubiquity and societal importance.In this paper, we present a library for the development of verified, state-dependent GUI applications in the dependently typed programming language Agda. The library uses Agda's expressive type system to ensure that the GUI, its controller, and the underlying model are all consistent, significantly reducing the scope for GUI-related bugs.We provide a way to specify and prove correctness properties of GUI applications in terms of user interactions and state transitions. Critically, GUI applications and correctness properties are not restricted to finite state machines and may involve the execution of arbitrary interactive programs. Additionally, the library connects to a standard, imperative GUI framework, enabling the development of native GUI applications with expected features, such as concurrency.We present applications of our library to building GUI applications to manage healthcare processes. The correctness properties we consider are the following: (1) That a state can only be reached by passing through a particular intermediate state, for example, that a particular treatment can only be reached after having conducted an X-Ray. (2) That one eventually reaches a particular state, for example, that one eventually decides on a treatment. The specification of such properties is defined in terms of a GUI application simulator, which simulates all possible sequences of interactions carried out by the user.</abstract><type>Conference Paper/Proceeding/Abstract</type><journal>Dependable Software Engineering. Theories, Tools, and Applications</journal><volume>10998</volume><journalNumber/><paginationStart>89</paginationStart><paginationEnd>107</paginationEnd><publisher>Springer International Publishing</publisher><placeOfPublication>Cham</placeOfPublication><isbnPrint>9783319999326</isbnPrint><isbnElectronic>9783319999333</isbnElectronic><issnPrint>0302-9743</issnPrint><issnElectronic>1611-3349</issnElectronic><keywords>Agda; Interactive theorem proving; GUI verification</keywords><publishedDay>26</publishedDay><publishedMonth>8</publishedMonth><publishedYear>2018</publishedYear><publishedDate>2018-08-26</publishedDate><doi>10.1007/978-3-319-99933-3_6</doi><url/><notes>Part of the Lecture Notes in Computer Science book series (LNCS, volume 10998)</notes><college>COLLEGE NANME</college><department>Mathematics and Computer Science School</department><CollegeCode>COLLEGE CODE</CollegeCode><DepartmentCode>MACS</DepartmentCode><institution>Swansea University</institution><apcterm/><lastEdited>2022-06-16T16:07:58.8486468</lastEdited><Created>2018-07-10T11:32:23.8250679</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>Stephan</firstname><surname>Adelsberger</surname><order>1</order></author><author><firstname>Anton</firstname><surname>Setzer</surname><orcid>0000-0001-5322-6060</orcid><order>2</order></author><author><firstname>Eric</firstname><surname>Walkingshaw</surname><order>3</order></author></authors><documents><document><filename>0040967-26072018015932.pdf</filename><originalFilename>SETTA18adelsbergerSetzerWalkingshawfinal.pdf</originalFilename><uploaded>2018-07-26T01:59:32.5800000</uploaded><type>Output</type><contentLength>446321</contentLength><contentType>application/pdf</contentType><version>Accepted Manuscript</version><cronfaStatus>true</cronfaStatus><embargoDate>2019-08-26T00:00:00.0000000</embargoDate><copyrightCorrect>true</copyrightCorrect><language>eng</language></document></documents><OutputDurs/></rfc1807>
spelling 2022-06-16T16:07:58.8486468 v2 40967 2018-07-10 Developing GUI Applications in a Verified Setting 5f7695285397f46d121207120247c2ae 0000-0001-5322-6060 Anton Setzer Anton Setzer true false 2018-07-10 MACS Although there have been major achievements in verified software, work on verifying graphical user interfaces (GUI) applications is underdeveloped relative to their ubiquity and societal importance.In this paper, we present a library for the development of verified, state-dependent GUI applications in the dependently typed programming language Agda. The library uses Agda's expressive type system to ensure that the GUI, its controller, and the underlying model are all consistent, significantly reducing the scope for GUI-related bugs.We provide a way to specify and prove correctness properties of GUI applications in terms of user interactions and state transitions. Critically, GUI applications and correctness properties are not restricted to finite state machines and may involve the execution of arbitrary interactive programs. Additionally, the library connects to a standard, imperative GUI framework, enabling the development of native GUI applications with expected features, such as concurrency.We present applications of our library to building GUI applications to manage healthcare processes. The correctness properties we consider are the following: (1) That a state can only be reached by passing through a particular intermediate state, for example, that a particular treatment can only be reached after having conducted an X-Ray. (2) That one eventually reaches a particular state, for example, that one eventually decides on a treatment. The specification of such properties is defined in terms of a GUI application simulator, which simulates all possible sequences of interactions carried out by the user. Conference Paper/Proceeding/Abstract Dependable Software Engineering. Theories, Tools, and Applications 10998 89 107 Springer International Publishing Cham 9783319999326 9783319999333 0302-9743 1611-3349 Agda; Interactive theorem proving; GUI verification 26 8 2018 2018-08-26 10.1007/978-3-319-99933-3_6 Part of the Lecture Notes in Computer Science book series (LNCS, volume 10998) COLLEGE NANME Mathematics and Computer Science School COLLEGE CODE MACS Swansea University 2022-06-16T16:07:58.8486468 2018-07-10T11:32:23.8250679 Faculty of Science and Engineering School of Mathematics and Computer Science - Computer Science Stephan Adelsberger 1 Anton Setzer 0000-0001-5322-6060 2 Eric Walkingshaw 3 0040967-26072018015932.pdf SETTA18adelsbergerSetzerWalkingshawfinal.pdf 2018-07-26T01:59:32.5800000 Output 446321 application/pdf Accepted Manuscript true 2019-08-26T00:00:00.0000000 true eng
title Developing GUI Applications in a Verified Setting
spellingShingle Developing GUI Applications in a Verified Setting
Anton Setzer
title_short Developing GUI Applications in a Verified Setting
title_full Developing GUI Applications in a Verified Setting
title_fullStr Developing GUI Applications in a Verified Setting
title_full_unstemmed Developing GUI Applications in a Verified Setting
title_sort Developing GUI Applications in a Verified Setting
author_id_str_mv 5f7695285397f46d121207120247c2ae
author_id_fullname_str_mv 5f7695285397f46d121207120247c2ae_***_Anton Setzer
author Anton Setzer
author2 Stephan Adelsberger
Anton Setzer
Eric Walkingshaw
format Conference Paper/Proceeding/Abstract
container_title Dependable Software Engineering. Theories, Tools, and Applications
container_volume 10998
container_start_page 89
publishDate 2018
institution Swansea University
isbn 9783319999326
9783319999333
issn 0302-9743
1611-3349
doi_str_mv 10.1007/978-3-319-99933-3_6
publisher Springer International Publishing
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 Although there have been major achievements in verified software, work on verifying graphical user interfaces (GUI) applications is underdeveloped relative to their ubiquity and societal importance.In this paper, we present a library for the development of verified, state-dependent GUI applications in the dependently typed programming language Agda. The library uses Agda's expressive type system to ensure that the GUI, its controller, and the underlying model are all consistent, significantly reducing the scope for GUI-related bugs.We provide a way to specify and prove correctness properties of GUI applications in terms of user interactions and state transitions. Critically, GUI applications and correctness properties are not restricted to finite state machines and may involve the execution of arbitrary interactive programs. Additionally, the library connects to a standard, imperative GUI framework, enabling the development of native GUI applications with expected features, such as concurrency.We present applications of our library to building GUI applications to manage healthcare processes. The correctness properties we consider are the following: (1) That a state can only be reached by passing through a particular intermediate state, for example, that a particular treatment can only be reached after having conducted an X-Ray. (2) That one eventually reaches a particular state, for example, that one eventually decides on a treatment. The specification of such properties is defined in terms of a GUI application simulator, which simulates all possible sequences of interactions carried out by the user.
published_date 2018-08-26T13:33:36Z
_version_ 1821412600763645952
score 11.247077

Similar Items