Conference Paper/Proceeding/Abstract 1196 views 259 downloads
Declarative GUIs: Simple, Consistent, and Verified
,
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
-
PDF | Accepted Manuscript
Download (586.12KB)
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...
| 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!
|
| 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. |
|---|---|
| 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 |
| Start Page: |
1 |
| End Page: |
15 |