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.
Keywords
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
The library contains a more interesting example [4] where clicking button \(b_i\) extends the GUI with i additional buttons.
References
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
Abel, A., Pientka, B.: Well-founded recursion with copatterns and sized types. JFP 26, e2 (2016). iCFP 2013 special issue
Abel, A., Pientka, B., Thibodeau, D., Setzer, A.: Copatterns: programming infinite structures by observations. In: POPL 2013, pp. 27–38. ACM, New York (2013)
Adelsberger, S., Setzer, A., Walkingshaw, E.: Deveoping GUI applications in a verified setting (2017). https://github.com/stephanpaper/SETTA18, git respository
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)
Agda Community: Agda Wiki (2017). http://wiki.portal.chalmers.se/agda
Bauer, A., Pretnar, M.: Programming with algebraic effects and handlers (2012). http://arxiv.org/abs/1203.1539, arXiv
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)
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
Brady, E.: Type-Driven Development with Idris, 1st edn. Manning Publications, Greenwich (2017)
Chiao, C.M., Künzle, V., Reichert, M.: Towards object-aware process support in healthcare information systems. In: eTELEMED 2012. IARIA, Delaware (2012)
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
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
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
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)
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)
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.
Jeffrey, A.: LTL types FRP: linear-time temporal logic propositions as types, proofs as functional reactive programs. In: PLPV 2012. ACM, New York (2012)
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
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)
Memon, A.M.: GUI testing: pitfalls and process. Computer 35(8), 87–88 (2002)
Memon, A.M.: An event-flow model of GUI-based applications for testing. Softw. Test. Verif. Reliab. 17(3), 137–157 (2007)
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)
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
Moggi, E.: Notions of computation and monads. Inf. Comput. 93(1), 55–92 (1991)
Montali, M., Chesani, F., Mello, P., Maggi, F.M.: Towards data-aware constraints in Declare. In: SAC 2013, pp. 1391–1396. ACM (2013)
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)
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
Pinson, K.: GUI programming in Idris? (2015). https://groups.google.com/forum/#!topic/idris-lang/R_7oixHofUo, google groups posting
Ruiz, A., Price, Y.W.: Test-driven GUI development with TestNG and Abbot. IEEE Softw. 24(3), 51–57 (2007)
Sculthorpe, N., Nilsson, H.: Safe functional reactive programming through dependent types. In: ICFP 2009, pp. 23–34. ACM (2009)
Sinnig, D., Khendek, F., Chalin, P.: Partial order semantics for use case and task models. Formal Asp. Comput. 23(3), 307–332 (2011)
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)
Valaer, L.A., Babb, R.G.: Choosing a user interface development tool. IEEE Softw. 14(4), 29–39 (1997)
Wan, Z., Hudak, P.: Functional reactive programming from first principles. In: PLDI 2000, pp. 242–252. ACM, New York (2000)
Whittle, J., Hutchinson, J., Rouncefield, M.: The state of practice in model-driven engineering. IEEE Softw. 31(3), 79–85 (2014)
wiki: WxHaskell. https://wiki.haskell.org/WxHaskell. Accessed 9 Feb 2017
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
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2018 Springer Nature Switzerland AG
About this paper
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)