No Cover Image

Conference Paper/Proceeding/Abstract 1094 views 234 downloads

Declarative GUIs: Simple, Consistent, and Verified

Stephan Adelsberger, Anton Setzer Orcid Logo, Eric Walkingshaw

PPDP '18 Proceedings of the 20th International Symposium on Principles and Practice of Declarative Programming, Pages: 1 - 15

Swansea University Author: Anton Setzer Orcid Logo

DOI (Published version): 10.1145/3236950.3236962

Abstract

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

Full description

Published in: PPDP '18 Proceedings of the 20th International Symposium on Principles and Practice of Declarative Programming
ISBN: 978-1-4503-6441-6
Published: Frankfurt/Main, Germany Proceedings of PPDP 2018 2018
Online Access: http://www.cs.swan.ac.uk/~csetzer/articles/SETTA2018/SETTA2018adelsbergerSetzerWalkingshaw.pdf
URI: https://cronfa.swan.ac.uk/Record/cronfa40969
Tags: Add Tag
No Tags, Be the first to tag this record!
first_indexed 2018-07-11T04:41:39Z
last_indexed 2020-08-06T03:04:54Z
id cronfa40969
recordtype SURis
fullrecord <?xml version="1.0"?><rfc1807><datestamp>2020-08-05T13:38:54.3720035</datestamp><bib-version>v2</bib-version><id>40969</id><entry>2018-07-10</entry><title>Declarative GUIs: Simple, Consistent, and Verified</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>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 means 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; they may involve both infinitely many states and the execution of arbitrary interactive programs.To demonstrate the practical application of our library to develop verified GUI applications in a safety-critical domain, we present a case study developed in cooperation with the Medical University of Vienna. The case study implements a healthcare process for prescribing anticoagulants, which is highly error-prone when followed manually.Our implementation generates GUIs from an abstract description of a data-aware business process, making our approach easy to reuse and adapt to other safety-critical processes. We prove medically relevant safety properties about the executable GUI application, such as that given certain inputs, certain states must or must not be reached. The specification of such properties is defined in terms of a GUI application simulator, which conceptually simulates all possible sequences of interactions performed by the user.</abstract><type>Conference Paper/Proceeding/Abstract</type><journal>PPDP '18 Proceedings of the 20th International Symposium on Principles and Practice of Declarative Programming</journal><paginationStart>1</paginationStart><paginationEnd>15</paginationEnd><publisher>Proceedings of PPDP 2018</publisher><placeOfPublication>Frankfurt/Main, Germany</placeOfPublication><isbnElectronic>978-1-4503-6441-6</isbnElectronic><keywords>Agda, interactive theorem proving, dependently typed programming, graphical user interfaces, GUI verification, state-dependent GUIs, reachability, dependable software, data-aware business processes, verification of business processes</keywords><publishedDay>3</publishedDay><publishedMonth>9</publishedMonth><publishedYear>2018</publishedYear><publishedDate>2018-09-03</publishedDate><doi>10.1145/3236950.3236962</doi><url>http://www.cs.swan.ac.uk/~csetzer/articles/SETTA2018/SETTA2018adelsbergerSetzerWalkingshaw.pdf</url><notes/><college>COLLEGE NANME</college><department>Computer Science</department><CollegeCode>COLLEGE CODE</CollegeCode><DepartmentCode>SCS</DepartmentCode><institution>Swansea University</institution><apcterm/><lastEdited>2020-08-05T13:38:54.3720035</lastEdited><Created>2018-07-10T23:10:09.1595417</Created><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>0040969-26072018020615.pdf</filename><originalFilename>PPDP18adelsbergerSetzerWalkingshawFinal.pdf</originalFilename><uploaded>2018-07-26T02:06:15.1270000</uploaded><type>Output</type><contentLength>577163</contentLength><contentType>application/pdf</contentType><version>Accepted Manuscript</version><cronfaStatus>true</cronfaStatus><embargoDate>2019-01-26T00:00:00.0000000</embargoDate><copyrightCorrect>true</copyrightCorrect><language>eng</language></document></documents><OutputDurs/></rfc1807>
spelling 2020-08-05T13:38:54.3720035 v2 40969 2018-07-10 Declarative GUIs: Simple, Consistent, and Verified 5f7695285397f46d121207120247c2ae 0000-0001-5322-6060 Anton Setzer Anton Setzer true false 2018-07-10 SCS 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 means 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; they may involve both infinitely many states and the execution of arbitrary interactive programs.To demonstrate the practical application of our library to develop verified GUI applications in a safety-critical domain, we present a case study developed in cooperation with the Medical University of Vienna. The case study implements a healthcare process for prescribing anticoagulants, which is highly error-prone when followed manually.Our implementation generates GUIs from an abstract description of a data-aware business process, making our approach easy to reuse and adapt to other safety-critical processes. We prove medically relevant safety properties about the executable GUI application, such as that given certain inputs, certain states must or must not be reached. The specification of such properties is defined in terms of a GUI application simulator, which conceptually simulates all possible sequences of interactions performed by the user. Conference Paper/Proceeding/Abstract PPDP '18 Proceedings of the 20th International Symposium on Principles and Practice of Declarative Programming 1 15 Proceedings of PPDP 2018 Frankfurt/Main, Germany 978-1-4503-6441-6 Agda, interactive theorem proving, dependently typed programming, graphical user interfaces, GUI verification, state-dependent GUIs, reachability, dependable software, data-aware business processes, verification of business processes 3 9 2018 2018-09-03 10.1145/3236950.3236962 http://www.cs.swan.ac.uk/~csetzer/articles/SETTA2018/SETTA2018adelsbergerSetzerWalkingshaw.pdf COLLEGE NANME Computer Science COLLEGE CODE SCS Swansea University 2020-08-05T13:38:54.3720035 2018-07-10T23:10:09.1595417 Stephan Adelsberger 1 Anton Setzer 0000-0001-5322-6060 2 Eric Walkingshaw 3 0040969-26072018020615.pdf PPDP18adelsbergerSetzerWalkingshawFinal.pdf 2018-07-26T02:06:15.1270000 Output 577163 application/pdf Accepted Manuscript true 2019-01-26T00:00:00.0000000 true eng
title Declarative GUIs: Simple, Consistent, and Verified
spellingShingle Declarative GUIs: Simple, Consistent, and Verified
Anton Setzer
title_short Declarative GUIs: Simple, Consistent, and Verified
title_full Declarative GUIs: Simple, Consistent, and Verified
title_fullStr Declarative GUIs: Simple, Consistent, and Verified
title_full_unstemmed Declarative GUIs: Simple, Consistent, and Verified
title_sort Declarative GUIs: Simple, Consistent, and Verified
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 PPDP '18 Proceedings of the 20th International Symposium on Principles and Practice of Declarative Programming
container_start_page 1
publishDate 2018
institution Swansea University
isbn 978-1-4503-6441-6
doi_str_mv 10.1145/3236950.3236962
publisher Proceedings of PPDP 2018
url http://www.cs.swan.ac.uk/~csetzer/articles/SETTA2018/SETTA2018adelsbergerSetzerWalkingshaw.pdf
document_store_str 1
active_str 0
description 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 means 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; they may involve both infinitely many states and the execution of arbitrary interactive programs.To demonstrate the practical application of our library to develop verified GUI applications in a safety-critical domain, we present a case study developed in cooperation with the Medical University of Vienna. The case study implements a healthcare process for prescribing anticoagulants, which is highly error-prone when followed manually.Our implementation generates GUIs from an abstract description of a data-aware business process, making our approach easy to reuse and adapt to other safety-critical processes. We prove medically relevant safety properties about the executable GUI application, such as that given certain inputs, certain states must or must not be reached. The specification of such properties is defined in terms of a GUI application simulator, which conceptually simulates all possible sequences of interactions performed by the user.
published_date 2018-09-03T03:52:12Z
_version_ 1763752576011993088
score 11.017797

Similar Items