Validating Properties of Component-based Graphical User Interfaces
In this paper we describe a validation process for graphical user interfaces based on existing toolkits and higher-order logic as mechanized in the HOL system. The underlying approach uses a single specification for constructing both implementations (prototypes) for experimentation and models for formal reasoning. The formal models allow the designer to verify mechanically specific requirements imposed on the user interface such as those found in safetyor security-critical applications. We illustrate our approach with an example that shows how the proof process works for behavioral properties that have been expressed in a rule-based fashion.
KeywordsUser Interface Output Port Input Port Operational Semantic Composite Component
Unable to display preview. Download preview PDF.
- 1.P.S.C. Alencar, D. Cowan, C.J.P. Lucena, and L.C.M. Nova. Formal Specification of Reusable Interface Objects. In Proceedings of Symposium on Software Reusability, Seattie, USA, April 1995.Google Scholar
- 2.C. Brink and I. Rewitzky. Modelling the algebra of weakest preconditions. South African Computer Journal, 6:11–20, July 1992.Google Scholar
- 3.P. Bumbulis. Combining Formal Techniques and Prototyping in User Interface Construction and Verification. Ph.d. thesis, Computer Science Department, University of Waterloo, 1996.Google Scholar
- 4.P. Bumbulis, P.S.C. Alencar, D.D. Cowan, and C.J.P. Lucena. Combining Formal Techniques and Prototyping in User Interface Construction and Verification. In 2nd Eurographics Workshop on Design, Specification, Verification of Interactive Systems (DSV-IS’95). Springer-Verlag Lecture Notes in Computer Science, 1995.Google Scholar
- 6.Edsger W. Dijkstra. A Discipline of Programming. Prentice-Hall, Englewood Cliffs, New Jersey, 1976.Google Scholar
- 10.M.D. Harrison and D.J. Duke. A review of formalisms for describing interactive behavior. In Richard N. Taylor and Joëlle Coutaz, editors, Software Engineering and Human-Computer Interaction; ICSE’94 Workshop on SE-HCI: Joint Research Issues, volume 896 of Lecture Notes in Computer Science, pages 49–75, Sorrento, Italy, 16–17 May 1994. Springer-Verlag.Google Scholar
- 12.Imperial College of Science, Technology and Medicine. Darwin Overview, 1994.Google Scholar
- 13.Ruurd Kuiper. An operational semantics for bounded nondeterminism equivalent to a denotational one. In J.W. de Bakker and J.C. van Vliet, editors, Algorithmic Languages, pages 373–398. IFIP, North Holland, 1981.Google Scholar
- 14.Johan J. Lukkien. An operational semantics for the guarded command language. In Mathematics of program construction: international conference, volume 669 of Lecture Notes in Computer Science, pages 233–249. Springer-Verlag, 1992.Google Scholar
- 17.G. Tredoux. Mechanizing execution sequence semantics in HOL. South African Computer Journal, 7:81–86, July 1992. Proceedings of the 7th Southern African Computer Research Symposium, Johannesburg, South Africa. Also available as part of the HOL distribution: ftp://lal.cs.byu.edu/pub/hol/holsys.tar.gz.Google Scholar