Validating Properties of Component-based Graphical User Interfaces

  • Peter Bumbulis
  • P. S. C. Alencar
  • D. D. Cowan
  • C. J. P. Lucena
Part of the Eurographics book series (EUROGRAPH)


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.


User Interface Output Port Input Port Operational Semantic Composite Component 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 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. 2.
    C. Brink and I. Rewitzky. Modelling the algebra of weakest preconditions. South African Computer Journal, 6:11–20, July 1992.Google Scholar
  3. 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. 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
  5. 5.
    Avra Cohn. The notion of proof in hardware verification. Journal of Automated Reasoning, 5(2):127–140, June 1989.CrossRefMATHGoogle Scholar
  6. 6.
    Edsger W. Dijkstra. A Discipline of Programming. Prentice-Hall, Englewood Cliffs, New Jersey, 1976.Google Scholar
  7. 7.
    Edsger W. Dijkstra and Carel S. Scholten. Predicate Calculus and Program Semantics. Springer-Verlag, New York, 1990.MATHGoogle Scholar
  8. 8.
    N. Francez. A case for a forward predicate transformer. Inf. Proc. Lett., 6(6):196–198, December 1977.CrossRefMATHMathSciNetGoogle Scholar
  9. 9.
    Stephen J. Garland, John V. Guttag, and James J. Homing. Debugging larch shared language specifications. IEEE Transactions on Software Engineering, 16(9):1044–1057, September 1990.CrossRefGoogle Scholar
  10. 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
  11. 11.
    C.A.R. Hoare. Some properties of predicate transformers. Journal of the ACM, 25(3):461–480, July 1978.CrossRefMathSciNetGoogle Scholar
  12. 12.
    Imperial College of Science, Technology and Medicine. Darwin Overview, 1994.Google Scholar
  13. 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. 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
  15. 11.
    Greg Nelson. A generalization of Dijkstra’s calculus. ACM Transactions on Programming Languages and Systems, 11(4): 517–561, October 1989.CrossRefGoogle Scholar
  16. 16.
    Oscar Nierstrasz, Simon Gibbs, and Dennis Tsichritzis. Component-oriented software development. Communications of the ACM, 35(9):160–165, September 1992.CrossRefGoogle Scholar
  17. 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: Scholar

Copyright information

© Springer-Verlag/Wien 1996

Authors and Affiliations

  • Peter Bumbulis
    • 1
  • P. S. C. Alencar
    • 1
  • D. D. Cowan
    • 1
  • C. J. P. Lucena
    • 2
  1. 1.Computer Science DepartmentUniversity of WaterlooWaterlooCanada
  2. 2.Departamento de InformáticaPontifícia Universidade Católica do Rio de JaneiroRio de JaneiroBrazil

Personalised recommendations