No Cover Image

Conference Paper/Proceeding/Abstract 204 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!
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
College: College of Science
Start Page: 1
End Page: 15