Cited By
View all- Adelsberger SSetzer AWalkingshaw E(2018)Developing GUI Applications in a Verified SettingDependable Software Engineering. Theories, Tools, and Applications10.1007/978-3-319-99933-3_6(89-107)Online publication date: 26-Aug-2018
Declarative GUIs: Simple, Consistent, and Verified
Article No.: 4, Pages 1 - 15
Abstract
Graphical user interfaces (GUIs) are ubiquitous in real-world software and a notorious source of bugs that are difficult to catch through software testing. Model checking has been used to prove the absence of certain kinds of bugs, but model checking works on an abstract model of the GUI application, which might be inconsistent with its implementation. We present a library for developing directly verified, state-dependent GUI applications in the dependently typed programming language Agda. In the library, the type of a GUI's controller depends on a specification of the GUI itself, statically enforcing consistency between them. Arbitrary properties can be defined and proved in terms of user interactions and state transitions. Our library connects to a custom-built Haskell back-end for declarative vector-based GUI elements. Compared to an earlier version of our library built on an existing imperative GUI framework, the more declarative back-end supports simpler definitions and proofs.
As a practical application of our library to 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.
References
[1]
Andreas Abel, Stephan Adelsberger, and Anton Setzer. 2017. Interactive programming in Agda -- Objects and graphical user interfaces. Journal of Functional Programming 27, Article 38 (Jan 2017), 54 pages.
[2]
Andreas Abel and Brigitte Pientka. 2016. Well-founded recursion with copatterns and sized types. JFP 26, Article e2 (2016), 61 pages. ICFP 2013 special issue.
[3]
Andreas Abel, Brigitte Pientka, David Thibodeau, and Anton Setzer. 2013. Copatterns: Programming infinite structures by observations. In Proceedings of the 40th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages (POPL '13), Roberto Giacobazzi and Radhia Cousot (Eds.). ACM, New York, NY, USA, 27--38.
[4]
Samina Raza Abidi, Jafna Cox, Ashraf Abusharekh, Nima Hashemian, and Syed Sibte Raza Abidi. 2016. A Digital Health System to Assist Family Physicians to Safely Prescribe NOAC Medications. Studies in health technology and informatics 228 (2016), 519--523. http://europepmc.org/abstract/MED/27577437
[5]
Stephan Adelsberger, Bashar Igried, Markus Moser, Vadim Savenkov, and Anton Setzer. 2018. Formal Verification for Feature-based Composition of Workflows. http://www.cs.swan.ac.uk/~csetzer/articles/SERENE/SERENE18/SERENE18AdelsbergerIgriedMoserSavenkoSetzer.pdf To appear in proceedings of http://www.cs.swan.ac.uk/~csetzer/articles/SERENE/SERENE18/SERENE18AdelsbergerIgriedMoserSavenkoSetzer.pdf.
[6]
Stephan Adelsberger, Anton Setzer, and Eric Walkingshaw. 2017. Declarative GUIs: Simple, Consistent, and Verified. (2017). https://github.com/stephanadelsb/PPDP18 Git respository.
[7]
Stephan Adelsberger, Anton Setzer, and Eric Walkingshaw. 2018. Developing GUI Applications in a Verified Setting. In Symp. on Dependable Software Engineering: Theories, Tools and Applications. ACM.
[8]
Agda Community. 2017. The Agda Wiki. (2017). http://wiki.portal.chalmers.se/agda
[9]
Dan Amelang, Bert Freudenberg, Ted Kaehler, Alan Kay, Stephen Murrell, Yoshiki Ohshima, Ian Piumarta, Kim Rose, Scott Wallace, Alessandro Warth, and Takashi Yamamiya. 2011. STEPS Toward Expressive Programming Systems, 2011 Progress Report. Technical Report. Viewpoints Research Institute.
[10]
Sven Apel, Don Batory, Christian Kästner, and Gunter Saake. 2013. Feature-Oriented Software Product Lines: Concepts and Implementation. Springer-Verlag, Berlin/Heidelberg.
[11]
Heinrich Apfelmus. 2017. Threepenny-gui. https://wiki.haskell.org/Threepenny-gui
[12]
Andrew W. Appel, Lennart Beringer, Adam Chlipala, Benjamin C. Pierce, Zhong Shao, Stephanie Weirich, and Steve Zdancewic. 2017. Position paper: the science of deep specification. Philosophical Transactions of the Royal Society of London A: Mathematical, Physical and Engineering Sciences 375, 2104 (2017), 1 -- 24.
[13]
Manuel Bärenz and Sebastian Seufert. 2017. Verifying Functional Reactive Programs with Side Effects. (2017). {41}, pp. 47 -- 48.
[14]
Andrej Bauer and Matija Pretnar. 2015. Programming with algebraic effects and handlers. Journal of Logical and Algebraic Methods in Programming 84, 1 (2015), 108 -- 123.
[15]
Thomas Bauereiß, Armando Pesenti Gritti, Andrei Popescu, and Franco Raimondi. 2017. CoSMeDis: A Distributed Social Media Platform with Formally Verified Confidentiality Guarantees. In 2017 IEEE Symposium on Security and Privacy (SP). IEEE, IEEE, Piscataway, New Jersey, US, 729--748.
[16]
Bernhard Beckert and Daniel Bruns. 2013. Dynamic Logic with Trace Semantics. In Automated Deduction -- CADE-24, Maria Paola Bonacina (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg, 315--329.
[17]
Edwin Brady. 2015. Resource-Dependent Algebraic Effects. In Trends in Functional Programming: 15th International Symposium, TFP 2014, Soesterberg, The Netherlands, May 26-28, 2014. Revised Selected Papers, Jurriaan Hage and Jay McCarthy (Eds.). Springer International Publishing, Cham, 18--33.
[18]
Edwin Brady. 2017. Type-driven Development with Idris (1 ed.). Manning Publications, Greenwich, Connecticut.
[19]
Carolina Ming Chiao, Vera Künzle, and Manfred Reichert. 2012. Towards Object-aware Process Support in Healthcare Information Systems. In 4th International Conference on eHealth, Telemedicine, and Social Medicine (eTELEMED 2012). IARIA, Wilmington, Delaware, US, 227--236. http://dbis.eprints.uni-ulm.de/775/
[20]
Ezra Cooper, Sam Lindley, Philip Wadler, and Jeremy Yallop. 2008. The essence of form abstraction. In Programming Languages and Systems: 6th Asian Symposium, APLAS 2008, Bangalore, India, December 9-11, 2008. Proceedings, G. Ramalingam (Ed.). Springer, Berlin, Heidelberg, 205--220.
[21]
Dan Amelang. 2018. Gezira Library. https://github.com/damelang/gezira https://github.com/damelang/gezira.
[22]
R. Davies. 1996. A temporal-logic approach to binding-time analysis. In Proceedings 11th Annual IEEE Symposium on Logic in Computer Science. IEEE, Piscataway, New Jersey, US, 184--195.
[23]
Søren Debois, Thomas Hildebrandt, and Tijs Slaats. 2015. Concurrency and Asynchrony in Declarative Workflows. In Business Process Management: 13th International Conference, BPM 2015, Innsbruck, Austria, August 31 -- September 3, 2015, Proceedings, Hamid Reza Motahari-Nezhad, Jan Recker, and Matthias Weidlich (Eds.). Springer International Publishing, Cham, 72--89.
[24]
Peter Dybjer. 2000. A general formulation of simultaneous inductive-recursive definitions in type theory. Journal of Symbolic Logic 65, 2 (June 2000), 525 -- 549.
[25]
Peter Dybjer and Anton Setzer. 2003. Induction-Recursion and Initial Algebras. Annals of Pure and Applied Logic 124 (2003), 1 -- 47.
[26]
Dov Gabbay, Amir Pnueli, Saharon Shelah, and Jonathan Stavi. 1980. On the Temporal Analysis of Fairness. In Proceedings of the 7th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL '80). ACM, New York, NY, USA, 163--173.
[27]
Mark L Graber, Dana Siegal, Heather Riah, Doug Johnston, and Kathy Kenyon. 2015. Electronic health record-related events in medical malpractice claims. Journal of patient safety 00, 00 (2015), 1-- 9.
[28]
Mark Grechanik, Qing Xie, and Chen Fu. 2009. Maintaining and Evolving GUI-directed Test Scripts. In Proceedings of the 31st International Conference on Software Engineering (ICSE '09). IEEE Computer Society, Washington, DC, USA, 408--418.
[29]
Peter Hancock and Anton Setzer. 2000. Interactive Programs in Dependent Type Theory. In CSL'00 (Lect. Notes in Comput. Sci.), Peter Clote and Helmut Schwichtenberg (Eds.), Vol. 1862. Springer, Berlin / Heidelberg, 317--331.
[30]
Peter Hancock and Anton Setzer. 2000. Specifying interactions with dependent types. http://www-sop.inria.fr/oasis/DTP00/Proceedings/proceedings.html Workshop on subtyping and dependent types in programming, Portugal, 7 July 2000.
[31]
Peter Hancock and Anton Setzer. 2005. Interactive programs and weakly final coalgebras in dependent type theory. In From Sets and Types to Topology and Analysis. Towards Practicable Foundations for Constructive Mathematics (Oxford Logic Guides). Clarendon Press, Oxford, UK, 115 -- 136.
[32]
haskell.org. 2018. SDL. Haskell Library. https://wiki.haskell.org/SDL https://wiki.haskell.org/SDL.
[33]
John Hughes, Lars Pareto, and Amr Sabry. 1996. Proving the Correctness of Reactive Systems Using Sized Types. In Proceedings of the 23rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL '96). ACM, New York, NY, USA, 410--423.
[34]
Idris Development Team. 2017. Idris. A language with dependent types. https://www.idris-lang.org/
[35]
K Ioannidis, I Scarlatinis, A Papachristos, and X Madia. 2018. 4CPS-017 Misuse of novel oral anticoagulants in hospital settings.
[36]
Alan Jeffrey. 2012. LTL Types FRP: Linear-time Temporal Logic Propositions As Types, Proofs As Functional Reactive Programs. In Proceedings of the Sixth Workshop on Programming Languages Meets Program Verification (PLPV '12). ACM, New York, NY, USA, 49--60.
[37]
Sudeep Kanav, Peter Lammich, and Andrei Popescu. 2014. A conference management system with verified document confidentiality. In Computer Aided Verification: 26th International Conference, CAV 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 18-22, 2014. Proceedings, Armin Biere and Roderick Bloem (Eds.). Springer International Publishing, Cham, 167--183.
[38]
Karim Kanso. 2012. Agda as a Platform for the Development of Verified Railway Interlocking Systems. Ph.D. Dissertation. Dept. of Computer Science, Swansea University, Swansea, UK. http://www.swan.ac.uk/csetzer/articlesFromOthers/index.html
[39]
Karim Kanso. 2017. Agda. https://github.com/kazkansouh/agda Github repository, fork of Agda installation, containing code from PhD thesis Kanso.
[40]
Karim Kanso and Anton Setzer. 2014. A lightweight integration of automated and interactive theorem proving. Mathematical Structures in Computer Science FirstView (12 November 2014), 1--25.
[41]
Ambrus Kaposi (Ed.). 2017. 23rd International Conference on Types for Proofs and Programs TYPES 2017, Budapest, Hungary, 29 May - 1 June 2017, Abstracts. (May 2017). http://types2017.elte.hu/proc.pdf
[42]
Kensuke Kojima and Atsushi Igarashi. 2011. Constructive linear-time temporal logic: Proof systems and Kripke semantics. Information and Computation 209, 12 (2011), 1491 -- 1503. Intuitionistic Modal Logic and Applications (IMLA 2008).
[43]
Glenn E. Krasner and Stephen T. Pope. 1988. A Cookbook for Using the Model-View-Controller User Interface Paradigm in Smalltalk-80. Journal of Object Oriented Programming 1, 3 (1988), 26--49.
[44]
Neelakantan R. Krishnaswami and Nick Benton. 2011. A Semantic Model for Graphical User Interfaces. In Proceedings of ICFP '11. ACM, New York, NY, USA, 45--57.
[45]
S Lawes and M Grissinger. 2017. Medication errors attributed to health information technology. PA-PSRS Patient Saf Advis 14, 1 (2017), 1--8.
[46]
Fabrizio Maria Maggi, Marlon Dumas, Luciano García-Bañuelos, and Marco Montali. 2013. Discovering Data-Aware Declarative Process Models from Event Logs. In Business Process Management, Florian Daniel, Jianmin Wang, and Barbara Weber (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 81--96.
[47]
Farah Magrabi, Mei-sing Ong, and Enrico Coiera. 2016. An Overview of HIT-Related Errors. In Safety of Health IT: Clinical Case Studies, Abha Agrawal (Ed.). Springer, Cham, 11--23.
[48]
Patrick Maier. 2004. Intuitionistic LTL and a New Characterization of Safety and Liveness. In Computer Science Logic: 18th International Workshop, CSL 2004, 13th Annual Conference of the EACSL, Karpacz, Poland, September 20-24, 2004. Proceedings, Jerzy Marcinkowski and Andrzej Tarlecki (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 295--309.
[49]
Martin A Makary and Michael Daniel. 2016. Medical error-the third leading cause of death in the US. BMJ: British Medical Journal (Online) 353 (May 03 2016), 1--5.
[50]
Atif M. Memon. 2002. GUI Testing: Pitfalls and Process. Computer 35, 8 (2002), 87--88.
[51]
Atif M. Memon. 2007. An Event-FlowModel of GUI-Based Applications for Testing. Software Testing, Verification and Reliability 17, 3 (2007), 137--157.
[52]
Atif M. Memon, Mary Lou Soffa, and Martha E. Pollack. 2001. Coverage Criteria for GUI Testing. ACM SIGSOFT Software Engineering Notes 26, 5 (2001), 256--267.
[53]
Atif M. Memon and Qing Xie. 2005. Studying the Fault-Detection Effectiveness of GUI Test Cases for Rapidly Evolving Software. IEEE Transactions on Software Engineering (TSE) 31, 10 (2005), 884--896.
[54]
Steven Mertens, Frederik Gailly, and Geert Poels. 2015. Enhancing declarative process models with DMN decision logic. In International Conference on Enterprise, Business-Process and Information Systems Modeling. Springer, Cham, 151--165.
[55]
Eugenio Moggi. 1991. Notions of computation and monads. Information and Computation 93, 1 (1991), 55 -- 92.
[56]
Marco Montali, Federico Chesani, Paola Mello, and Fabrizio M. Maggi. 2013. Towards Data-aware Constraints in Declare. In Proceedings of the 28th Annual ACM Symposium on Applied Computing (SAC '13). ACM, New York, NY, USA, 1391--1396.
[57]
Marco Montali, Maja Pesic, Wil M. P. van der Aalst, Federico Chesani, Paola Mello, and Sergio Storari. 2010. Declarative Specification and Verification of Service Choreographies. ACM Trans. Web 4, 1, Article 3 (Jan. 2010), 62 pages.
[58]
Risa B Myers, Stephen L Jones, and Dean F Sittig. 2011. Review of reported clinical information system adverse events in US Food and Drug Administration databases. Applied clinical informatics 2, 1 (2011), 63.
[59]
Keiko Nakata and Tarmo Uustalu. 2009. Trace-based coinductive operational semantics for while. In Theorem Proving in Higher Order Logics, Stefan Berghofer, Tobias Nipkow, Christian Urban, and Makarius Wenzel (Eds.). Springer, Springer Berlin Heidelberg, Berlin, Heidelberg, 375--390.
[60]
Kent Petersson and Dan Synek. 1989. A Set Constructor for Inductive Sets in Martin-Löf's Type Theory. In CTCS'89 (Lect. Notes in Comput. Sci.), Vol. 389. Springer-Verlag, London, UK, 128--140.
[61]
Simon L. Peyton Jones and Philip Wadler. 1993. Imperative Functional Programming. In Proceedings of the 20th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL '93). ACM, New York, NY, USA, 71--84.
[62]
Keith Pinson. 2015. GUI programming in Idris? https://groups.google.com/forum/#!topic/idris-lang/R_7oixHofUo Google groups posting.
[63]
David C Radley, Melanie R Wasserman, Lauren EW Olsho, Sarah J Shoemaker, Mark D Spranca, and Bethany Bradshaw. 2013. Reduction in medication errors in hospitals due to adoption of computerized provider order entry systems. Journal of the American Medical Informatics Association 20, 3 (2013), 470--476.
[64]
Rasterific. 2018. Github repository. https://github.com/Twinside/Rasterific https://github.com/Twinside/Rasterific.
[65]
William B Runciman, Elizabeth E Roughead, Susan J Semple, and Robert J Adams. 2003. Adverse drug events and medication errors in Australia. International Journal for Quality in Health Care 15, suppl_1 (2003), i49-i59.
[66]
Eva A Saedder, Birgitte Brock, Lars Peter Nielsen, Dorthe K Bonnerup, and Marianne Lisby. 2014. Identifying high-risk medication: a systematic literature review. European journal of clinical pharmacology 70, 6 (2014), 637--645.
[67]
Neil Sculthorpe and Henrik Nilsson. 2009. Safe Functional Reactive Programming Through Dependent Types. In Proceedings of the 14th ACM SIGPLAN International Conference on Functional Programming (ICFP '09). ACM, New York, NY, USA, 23--34.
[68]
SDL. 2018. Single Directmedia Layer. Library. http://www.libsdl.org/http://www.libsdl.org/.
[69]
Anton Setzer. 2006. Object-oriented programming in dependent type theory. In Conference Proceedings of TFP 2006. Intellect Books, Bristol, 1--16. http://www.cs.nott.ac.uk/~psznhn/TFP2006/Papers/26-AntonSetzer-OOPInDependentTypeTheory.pdf
[70]
Anton Setzer and Peter Hancock. 2004. Interactive Programs and Weakly Final Coalgebras in Dependent Type Theory (Extended Version). In Dependently Typed Programming 2004 (Dagstuhl Seminar Proc.s), Thorsten Altenkirch, Martin Hofmann, and John Hughes (Eds.), Vol. 04381. Internationales Begegnungs- und Forschungszentrum (IBFI), Schloss Dagstuhl, Germany, Dagstuhl, Germany, 1--30. http://drops.dagstuhl.de/opus/volltexte/2005/176/
[71]
Lin Tan, Chen Liu, Zhenmin Li, Xuanhui Wang, Yuanyuan Zhou, and Chengxiang Zhai. 2014. Bug Characteristics in Open Source Software. Empirical Software Engineering 19, 6 (2014), 1665--1705.
[72]
Laura A. Valaer and Robert G. Babb. 1997. Choosing a User Interface Development Tool. IEEE Software 14, 4 (1997), 29--39.
[73]
Wil MP van Der Aalst, Maja Pesic, and Helen Schonenberg. 2009. Declarative workflows: Balancing between flexibility and support. Computer Science-Research and Development 23, 2 (2009), 99--113.
[74]
Philip Wadler. 1990. Comprehending Monads. In Proceedings of the 1990 ACM Conference on LISP and Functional Programming (LFP '90). ACM, New York, NY, USA, 61--78.
[75]
Philip Wadler. 1995. Monads for functional programming. In Advanced Functional Programming: First International Spring School on Advanced Functional Programming Techniques Båstad, Sweden, May 24-30, 1995 Tutorial Text, Johan Jeuring and Erik Meijer (Eds.). Springer, Berlin, Heidelberg, 24--52.
[76]
Philip Wadler. 1997. How to Declare an Imperative. ACM Comput. Surv. 29, 3 (September 1997), 240--263.
[77]
Philip Wadler. 1998. The Marriage of Effects and Monads. In Proceedings of the Third ACM SIGPLAN International Conference on Functional Programming (ICFP 98). ACM, New York, NY, USA, 63--74.
[78]
Zhanyong Wan and Paul Hudak. 2000. Functional Reactive Programming from First Principles. In ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI). ACM, New York, NY, USA, 242--252.
[79]
J. Whittle, J. Hutchinson, and M. Rouncefield. 2014. The State of Practice in Model-Driven Engineering. IEEE Software 31, 3 (2014), 79--85.
[80]
wiki.haskell. 2017. WxHaskell. (Retrieved 9 February 2017). https://wiki.haskell.org/WxHaskell
[81]
Xiaoxi Yao, Nilay D Shah, Lindsey R Sangaralingham, Bernard J Gersh, and Peter A Noseworthy. 2017. Non-vitamin K antagonist oral anticoagulant dosing in patients with atrial fibrillation and renal dysfunction. Journal of the American College of Cardiology 69, 23 (2017), 2779--2790.
Index Terms
- Declarative GUIs: Simple, Consistent, and Verified
Recommendations
FranTk - a declarative GUI language for Haskell
ICFP '00: Proceedings of the fifth ACM SIGPLAN international conference on Functional programmingFranTk is a new high level library for programming Graphical User Interfaces (GUIs) in Haskell. It is based on Fran (Functional Reactive Animation), and uses the notions of Behaviors and Events to structure code. Behaviors are time-varying, reactive ...
Declarative GUI Programming in Microsoft Windows
A domain-specific language for building user interfaces offers a transparent way for programmers to specify interface elements. Microsoft's Extensible Application Markup Language is an XML dialect for this purpose. However, XAML isn't the only choice ...
Asynchronous functional reactive programming for GUIs
PLDI '13Graphical user interfaces (GUIs) mediate many of our interactions with computers. Functional Reactive Programming (FRP) is a promising approach to GUI design, providing high-level, declarative, compositional abstractions to describe user interactions ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
September 2018
306 pages
Copyright © 2018 ACM.
Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]
In-Cooperation
- SIGPLAN: ACM Special Interest Group on Programming Languages
- Goethe University: Goethe University Frankfurt
Publisher
Association for Computing Machinery
New York, NY, United States
Publication History
Published: 03 September 2018
Check for updates
Author Tags
Qualifiers
- Research-article
- Research
- Refereed limited
Conference
PPDP '18
PPDP '18: The 20th International Symposium on Principles and Practice of Declarative Programming
September 3 - 5, 2018
Frankfurt am Main, Germany
Acceptance Rates
PPDP '18 Paper Acceptance Rate 22 of 39 submissions, 56%;
Overall Acceptance Rate 230 of 486 submissions, 47%
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- View Citations1Total Citations
- 139Total Downloads
- Downloads (Last 12 months)13
- Downloads (Last 6 weeks)7
Reflects downloads up to 16 Nov 2024
Other Metrics
Citations
Cited By
View all- Adelsberger SSetzer AWalkingshaw E(2018)Developing GUI Applications in a Verified SettingDependable Software Engineering. Theories, Tools, and Applications10.1007/978-3-319-99933-3_6(89-107)Online publication date: 26-Aug-2018
View Options
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in