Skip to main content
SpringerLink
Log in

Developing GUI Applications in a Verified Setting

  • Conference paper
  • First Online:
Dependable Software Engineering. Theories, Tools, and Applications (SETTA 2018)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 10998))

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.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Notes

  1. 1.

    The library contains a more interesting example [4] where clicking button \(b_i\) extends the GUI with i additional buttons.

References

  1. Abel, A., Adelsberger, S., Setzer, A.: Interactive programming in Agda - objects and graphical user interfaces. J. Funct. Program. 27, 38 (2017). https://doi.org/10.1017/S0956796816000319

    Article  MathSciNet  MATH  Google Scholar 

  2. Abel, A., Pientka, B.: Well-founded recursion with copatterns and sized types. JFP 26, e2 (2016). iCFP 2013 special issue

    MathSciNet  MATH  Google Scholar 

  3. Abel, A., Pientka, B., Thibodeau, D., Setzer, A.: Copatterns: programming infinite structures by observations. In: POPL 2013, pp. 27–38. ACM, New York (2013)

    Google Scholar 

  4. Adelsberger, S., Setzer, A., Walkingshaw, E.: Deveoping GUI applications in a verified setting (2017). https://github.com/stephanpaper/SETTA18, git respository

  5. Adelsberger, S., Setzer, A., Walkingshaw, E.: Declarative GUIs: simple, consistent, and verified. In: International Conference on Principles and Practice of Declarative Programming (PPDP). ACM (2018)

    Google Scholar 

  6. Agda Community: Agda Wiki (2017). http://wiki.portal.chalmers.se/agda

  7. Bauer, A., Pretnar, M.: Programming with algebraic effects and handlers (2012). http://arxiv.org/abs/1203.1539, arXiv

  8. Bauereiß, T., Gritti, A.P., Popescu, A., Raimondi, F.: CoSMeDis: a distributed social media platform with formally verified confidentiality guarantees. In: 2017 Symposium on Security and Privacy, pp. 729–748. IEEE (2017)

    Google Scholar 

  9. Brady, E.: Resource-dependent algebraic effects. In: Hage, J., McCarthy, J. (eds.) TFP 2014. LNCS, vol. 8843, pp. 18–33. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-14675-1_2

    Chapter  Google Scholar 

  10. Brady, E.: Type-Driven Development with Idris, 1st edn. Manning Publications, Greenwich (2017)

    Google Scholar 

  11. Chiao, C.M., Künzle, V., Reichert, M.: Towards object-aware process support in healthcare information systems. In: eTELEMED 2012. IARIA, Delaware (2012)

    Google Scholar 

  12. Cooper, E., Lindley, S., Wadler, P., Yallop, J.: The essence of form abstraction. In: Ramalingam, G. (ed.) APLAS 2008. LNCS, vol. 5356, pp. 205–220. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-89330-1_15

    Chapter  Google Scholar 

  13. Debois, S., Hildebrandt, T., Slaats, T.: Concurrency and asynchrony in declarative workflows. In: Motahari-Nezhad, H.R., Recker, J., Weidlich, M. (eds.) BPM 2015. LNCS, vol. 9253, pp. 72–89. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-23063-4_5

    Chapter  Google Scholar 

  14. Hancock, P., Setzer, A.: Interactive programs in dependent type theory. In: Clote, P.G., Schwichtenberg, H. (eds.) CSL 2000. LNCS, vol. 1862, pp. 317–331. Springer, Heidelberg (2000). https://doi.org/10.1007/3-540-44622-2_21

    Chapter  Google Scholar 

  15. Harrison, M.D., Masci, P., Campos, J.C., Curzon, P.: Verification of user interface software: the example of use-related safety requirements and programmable medical devices. IEEE Trans. Hum.-Mach. Syst. 47(6), 834–846 (2017)

    Article  Google Scholar 

  16. Hughes, J., Pareto, L., Sabry, A.: Proving the correctness of reactive systems using sized types. In: POPL 1996, pp. 410–423. ACM, New York (1996)

    Google Scholar 

  17. Igried, B., Setzer, A.: Defining trace semantics for CSP-Agda, 30 January 2018. http://www.cs.swan.ac.uk/~csetzer/articles/types2016PostProceedings/igriedSetzerTypes2016Postproceedings.pdf. Accepted for Publication in Postproceedings TYPES 2016, 23 p.

  18. Jeffrey, A.: LTL types FRP: linear-time temporal logic propositions as types, proofs as functional reactive programs. In: PLPV 2012. ACM, New York (2012)

    Google Scholar 

  19. Kanav, S., Lammich, P., Popescu, A.: A conference management system with verified document confidentiality. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 167–183. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-08867-9_11

    Chapter  Google Scholar 

  20. Krasner, G.E., Pope, S.T.: A cookbook for using the model-view-controller user interface paradigm in Smalltalk-80. JOOP 1(3), 26–49 (1988)

    Google Scholar 

  21. Memon, A.M.: GUI testing: pitfalls and process. Computer 35(8), 87–88 (2002)

    Article  Google Scholar 

  22. Memon, A.M.: An event-flow model of GUI-based applications for testing. Softw. Test. Verif. Reliab. 17(3), 137–157 (2007)

    Article  MathSciNet  Google Scholar 

  23. Memon, A.M., Xie, Q.: Studying the fault-detection effectiveness of GUI test cases for rapidly evolving software. IEEE Trans. Softw. Eng. 31(10), 884–896 (2005)

    Article  Google Scholar 

  24. Mertens, S., Gailly, F., Poels, G.: Enhancing declarative process models with DMN decision logic. In: Gaaloul, K., Schmidt, R., Nurcan, S., Guerreiro, S., Ma, Q. (eds.) CAISE 2015. LNBIP, vol. 214, pp. 151–165. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-19237-6_10

    Chapter  Google Scholar 

  25. Moggi, E.: Notions of computation and monads. Inf. Comput. 93(1), 55–92 (1991)

    Article  MathSciNet  Google Scholar 

  26. Montali, M., Chesani, F., Mello, P., Maggi, F.M.: Towards data-aware constraints in Declare. In: SAC 2013, pp. 1391–1396. ACM (2013)

    Google Scholar 

  27. Montali, M., Pesic, M., van der Aalst, W.M.P., Chesani, F., Mello, P., Storari, S.: Declarative specification and verification of service choreographies. ACM Trans. Web 4(1), 3:1–3:62 (2010)

    Article  Google Scholar 

  28. Petersson, K., Synek, D.: A set constructor for inductive sets in Martin-Löf’s type theory. In: Pitt, D.H., Rydeheard, D.E., Dybjer, P., Pitts, A.M., Poigné, A. (eds.) Category Theory and Computer Science. LNCS, vol. 389, pp. 128–140. Springer, Heidelberg (1989). https://doi.org/10.1007/BFb0018349

    Chapter  Google Scholar 

  29. Pinson, K.: GUI programming in Idris? (2015). https://groups.google.com/forum/#!topic/idris-lang/R_7oixHofUo, google groups posting

  30. Ruiz, A., Price, Y.W.: Test-driven GUI development with TestNG and Abbot. IEEE Softw. 24(3), 51–57 (2007)

    Article  Google Scholar 

  31. Sculthorpe, N., Nilsson, H.: Safe functional reactive programming through dependent types. In: ICFP 2009, pp. 23–34. ACM (2009)

    Google Scholar 

  32. Sinnig, D., Khendek, F., Chalin, P.: Partial order semantics for use case and task models. Formal Asp. Comput. 23(3), 307–332 (2011)

    Article  Google Scholar 

  33. Tan, L., Liu, C., Li, Z., Wang, X., Zhou, Y., Zhai, C.: Bug characteristics in open source software. Empir. Softw. Eng. 19(6), 1665–1705 (2014)

    Article  Google Scholar 

  34. Valaer, L.A., Babb, R.G.: Choosing a user interface development tool. IEEE Softw. 14(4), 29–39 (1997)

    Article  Google Scholar 

  35. Wan, Z., Hudak, P.: Functional reactive programming from first principles. In: PLDI 2000, pp. 242–252. ACM, New York (2000)

    Google Scholar 

  36. Whittle, J., Hutchinson, J., Rouncefield, M.: The state of practice in model-driven engineering. IEEE Softw. 31(3), 79–85 (2014)

    Article  Google Scholar 

  37. wiki: WxHaskell. https://wiki.haskell.org/WxHaskell. Accessed 9 Feb 2017

Download references

Acknowledgments

The first and second author were supported by the project CA COST Action CA15123 European research network on types for programming and verification (EUTYPES). The second author was additionally supported by CORCON (Correctness by Construction, FP7 Marie Curie International Research Project, PIRSES-GA-2013-612638), COMPUTAL (Computable Analysis, FP7 Marie Curie International Research Project, PIRSES-GA-2011-294962), CID (Computing with Infinite Data, Marie Curie RISE project, H2020-MSCA-RISE-2016-731143). The third author was supported by AFRL Contract FA8750-16-C-0044 under the DARPA BRASS program.

Author information

Authors and Affiliations

  1. Department of Information Systems, Vienna University of Economics, Vienna, Austria

    Stephan Adelsberger

  2. Department of Computer Science, Swansea University, Swansea, UK

    Anton Setzer

  3. School of EECS, Oregon State University, Corvallis, USA

    Eric Walkingshaw

Authors
  1. Stephan Adelsberger
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Anton Setzer
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Eric Walkingshaw
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Stephan Adelsberger .

Editor information

Editors and Affiliations

  1. Nanjing University, Nanjing, China

    Xinyu Feng

  2. Westfälische Wilhelms-Universität Münster, Münster, Germany

    Markus Müller-Olm

  3. Western Michigan University, Kalamazoo, Michigan, USA

    Zijiang Yang

Rights and permissions

Reprints and permissions

Copyright information

© 2018 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Adelsberger, S., Setzer, A., Walkingshaw, E. (2018). Developing GUI Applications in a Verified Setting. In: Feng, X., Müller-Olm, M., Yang, Z. (eds) Dependable Software Engineering. Theories, Tools, and Applications. SETTA 2018. Lecture Notes in Computer Science(), vol 10998. Springer, Cham. https://doi.org/10.1007/978-3-319-99933-3_6

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-99933-3_6

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-99932-6

  • Online ISBN: 978-3-319-99933-3

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation