No Cover Image

Book chapter 282 views 19 downloads

Developing GUI Applications in a Verified Setting / Anton, Setzer

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

Swansea University Author: Anton, Setzer

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: 978-3-319-99932-6 978-3-319-99933-3
ISSN: 0302-9743 1611-3349
Published: Beijing, China Dependable Software Engineering. Theories, Tools, and Applications 4th International Symposium, SETTA 2018 2018
Online Access: Check full text

URI: https://cronfa.swan.ac.uk/Record/cronfa40967
Tags: Add Tag
No Tags, Be the first to tag this record!
first_indexed 2018-07-10T15:01:44Z
last_indexed 2018-09-21T12:53:08Z
id cronfa40967
recordtype SURis
fullrecord <?xml version="1.0"?><rfc1807><datestamp>2018-09-21T12:07:35.5858506</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>SCS</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>Book chapter</type><journal>Dependable Software Engineering. Theories, Tools, and Applications</journal><volume>10998</volume><paginationStart>89</paginationStart><paginationEnd>107</paginationEnd><publisher>Dependable Software Engineering. Theories, Tools, and Applications 4th International Symposium, SETTA 2018</publisher><placeOfPublication>Beijing, China</placeOfPublication><isbnPrint>978-3-319-99932-6</isbnPrint><isbnElectronic>978-3-319-99933-3</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>http://www.cs.swan.ac.uk/~csetzer/articles/SETTA2018a/SETTA2018adelsbergerSetzerWalkingshawfinal.pdf</url><notes>Part of the Lecture Notes in Computer Science book series (LNCS, volume 10998)</notes><college>COLLEGE NANME</college><department>Computer Science</department><CollegeCode>COLLEGE CODE</CollegeCode><DepartmentCode>SCS</DepartmentCode><institution>Swansea University</institution><lastEdited>2018-09-21T12:07:35.5858506</lastEdited><Created>2018-07-10T11:32:23.8250679</Created><path><level id="1">College of Science</level><level id="2">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-10072018113732.pdf</filename><originalFilename>paper_4_Vers2.pdf</originalFilename><uploaded>2018-07-10T11:37:32.6770000</uploaded><type>Output</type><contentLength>446321</contentLength><contentType>application/pdf</contentType><version>Proof</version><cronfaStatus>true</cronfaStatus><action/><embargoDate>2019-09-10T00:00:00.0000000</embargoDate><copyrightCorrect>true</copyrightCorrect><language>eng</language></document><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><action/><embargoDate>2019-08-26T00:00:00.0000000</embargoDate><copyrightCorrect>true</copyrightCorrect><language>eng</language></document></documents></rfc1807>
spelling 2018-09-21T12:07:35.5858506 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 SCS 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. Book chapter Dependable Software Engineering. Theories, Tools, and Applications 10998 89 107 Dependable Software Engineering. Theories, Tools, and Applications 4th International Symposium, SETTA 2018 Beijing, China 978-3-319-99932-6 978-3-319-99933-3 0302-9743 1611-3349 Agda; Interactive theorem proving; GUI verification 26 8 2018 2018-08-26 10.1007/978-3-319-99933-3_6 http://www.cs.swan.ac.uk/~csetzer/articles/SETTA2018a/SETTA2018adelsbergerSetzerWalkingshawfinal.pdf Part of the Lecture Notes in Computer Science book series (LNCS, volume 10998) COLLEGE NANME Computer Science COLLEGE CODE SCS Swansea University 2018-09-21T12:07:35.5858506 2018-07-10T11:32:23.8250679 College of Science Computer Science Stephan Adelsberger 1 Anton Setzer 0000-0001-5322-6060 2 Eric Walkingshaw 3 0040967-10072018113732.pdf paper_4_Vers2.pdf 2018-07-10T11:37:32.6770000 Output 446321 application/pdf Proof true 2019-09-10T00:00:00.0000000 true eng 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
format Book chapter
container_title Dependable Software Engineering. Theories, Tools, and Applications
container_volume 10998
container_start_page 89
publishDate 2018
institution Swansea University
isbn 978-3-319-99932-6
978-3-319-99933-3
issn 0302-9743
1611-3349
doi_str_mv 10.1007/978-3-319-99933-3_6
publisher Dependable Software Engineering. Theories, Tools, and Applications 4th International Symposium, SETTA 2018
college_str College of Science
hierarchytype
hierarchy_top_id collegeofscience
hierarchy_top_title College of Science
hierarchy_parent_id collegeofscience
hierarchy_parent_title College of Science
department_str Computer Science{{{_:::_}}}College of Science{{{_:::_}}}Computer Science
url http://www.cs.swan.ac.uk/~csetzer/articles/SETTA2018a/SETTA2018adelsbergerSetzerWalkingshawfinal.pdf
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-26T04:04:54Z
_version_ 1674243572136673280
score 10.743054