No Cover Image

Conference Paper/Proceeding/Abstract 1011 views 126 downloads

Developing GUI Applications in a Verified Setting

Stephan Adelsberger, Anton Setzer Orcid Logo, Eric Walkingshaw

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

Swansea University Author: Anton Setzer Orcid Logo

Check full text

DOI (Published version): 10.1007/978-3-319-99933-3_6

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: 9783319999326 9783319999333
ISSN: 0302-9743 1611-3349
Published: Cham Springer International Publishing 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!
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.
Item Description: Part of the Lecture Notes in Computer Science book series (LNCS, volume 10998)
Keywords: Agda; Interactive theorem proving; GUI verification
College: Faculty of Science and Engineering
Start Page: 89
End Page: 107

Similar Items