No Cover Image

Conference Paper/Proceeding/Abstract 197 views 9 downloads

Declarative GUIs: Simple, Consistent, and Verified / Anton, Setzer

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

Swansea University Author: Anton, Setzer

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 2019-07-18T21:16:33Z
id cronfa40969
recordtype SURis
fullrecord <?xml version="1.0"?><rfc1807><datestamp>2019-07-18T15:04:20.1579809</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><lastEdited>2019-07-18T15:04:20.1579809</lastEdited><Created>2018-07-10T23:10:09.1595417</Created><path><level id="1">College of Science</level><level id="2">Computer Science</level></path><authors><author><firstname>Anton</firstname><surname>Setzer</surname><orcid>0000-0001-5322-6060</orcid><order>1</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><action/><embargoDate>2019-01-26T00:00:00.0000000</embargoDate><copyrightCorrect>true</copyrightCorrect><language>eng</language></document></documents></rfc1807>
spelling 2019-07-18T15:04:20.1579809 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 2019-07-18T15:04:20.1579809 2018-07-10T23:10:09.1595417 College of Science Computer Science Anton Setzer 0000-0001-5322-6060 1 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
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
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/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-03T04:02:27Z
_version_ 1650057803227725824
score 10.867005