No Cover Image

Book Chapter 178 views

Developing GUI Applications in a Verified Setting / Stephan Adelsberger; Anton Setzer; Eric Walkingshaw

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

Swansea University Author: Setzer, Anton

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: 978-3-319-99932-6 978-3-319-99933-3
ISSN: 0302-9743 1611-3349
Published: Beijing, China Dependable Software Engineering. Theories, Tools, and Applications 4th International Symposium, SETTA 2018 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: College of Science
Start Page: 89
End Page: 107