Combining Formal Techniques and Prototyping in User Interface Construction and Verification

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


In this paper we investigate a component-based approach to combining formal techniques and prototyping for user interface construction in which a single specification is used for constructing both implementations (prototypes) for experimentation and models for formal reasoning. Using a component-based approach not only allows us to construct realistic prototypes, but also allows us to generate a variety of formal models. Rapid prototyping allows the designs to be tested with end users and modified based on their comments and performance, while formal modeling permits the designer to verify mechanically specific requirements imposed on the user interface such as those found in safety-or security-critical applications.


User Interface Symbolic Execution Primitive Component Dialogue Specification Reliable User Interface 
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.
    Heather Alexander. Formally-based techniques for dialogue design. In Proceedings of the HCI’87 Conference on People and Computers III, Systems and Interfaces, pages 201–213, 1987.Google Scholar
  2. 2.
    Apple Computer, Inc. Apple Macintosh Human Interface Guidelines, 1992.Google Scholar
  3. 3.
    Apple Computer, Inc. Human Interface Guidelines: The Apple Desktop Interface, 1992.Google Scholar
  4. 4.
    Remi Bastide and Philippe Palanque. Petri net objects for the design, validation and prototyping of user-driven interfaces. In Proceedings of IFIP INTERACT’90: Human-Computer Interaction, Detailed Design: Construction Tools, pages 625631, 1990.Google Scholar
  5. 5.
    L.M.F. Carneiro-Coffin, D.D. Cowan, C.J.P. Lucena, and D. Smith. An experience using JASMINIUM — formalization assisting with the design of user interfaces. 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 141–158, Sorrento, Italy, 16–17 May 1994. Springer-Verlag.Google Scholar
  6. 6.
    Luisa Maria Fonseca Carneiro-Coffin. Jasminum: J oining A DVS and S tate M achines i n a N otation for U ser-Interface M odeling. PhD thesis, University of Waterloo, 1994.Google Scholar
  7. 7.
    K. Mani Chandy and Jayadev Misra. Parallel programming. Addison-Wesley Pub. Co., 1988.Google Scholar
  8. 8.
    Dominique Clément and Janet Incerpi. Specifying the behavior of graphical objects using esterel. In TAPSOFT ‘89, volume 2, pages 111–125, Barcelona, Spain, March 1989.Google Scholar
  9. 9.
    Avra Cohn. The notion of proof in hardware verification. Journal of Automated Reasoning, 5 (2): 127–140, June 1989.CrossRefMATHGoogle Scholar
  10. 10.
    Bruno D’Ausbourg and Pierre Roche. Specifying formally or deriving a formal model from an informal description of user interfaces? In Christopher Rouff, editor, CHI 95 Workshop Formal Specification of User Interfaces Position Papers, Denver, Colorado, May 7–8 1995.Google Scholar
  11. 11.
    Digitalk. PARTS Workbench User’s Guide, 1992.Google Scholar
  12. 12.
    Edsger W. Dijkstra. A Discipline of Programming. Prentice-Hall, Englewood Cliffs, New Jersey, 1976.Google Scholar
  13. 13.
    D.J. Duke and M.D. Harrison. From formal models to formal methods. 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 159–173, Sorrento, Italy, 16–17 May 1994. Springer-Verlag.Google Scholar
  14. 14.
    Kevin J. Farley. Software testing for windows developers. Data Based Advisor, 11 (11), November 1993.Google Scholar
  15. 15.
    N. Frances. A case for a forward predicate transformer. Inf. Proc. Lett.,6(6):196–198, December 1977.CrossRefGoogle Scholar
  16. 16.
    Stephen J. Garland, John V. Guttag, and James J. Horning. Debugging larch shared language specifications. IEEE Transactions on Software Engineering, 16 (9): 1044–1057, September 1990.CrossRefGoogle Scholar
  17. 17.
    M. Gordon. Why higher-order logic is a good formalism for specifying and verifying hardware. In Formal Aspects of VLSI Design: Proceedings of the 1985 Edinburgh Workshop on VLSI, pages 409–417. North-Holland, 1986.Google Scholar
  18. 18.
    M. J. C. Gordon and Tom F. Melham. Introduction to HOL: a theorem proving environment for higher order logic. Cambridge University Press, New York, 1993.MATHGoogle Scholar
  19. 19.
    Nicholas Halbwachs, Paul Caspi, Pascal Raymond, and Daniel Pilaud. The synchronous data flow programming language LUSTRE. Proceedings of the IEEE, 79 (9): 1305–1320, September 1991.CrossRefGoogle Scholar
  20. 20.
    D. Harel and A. Pnueli. On the development of reactive systems. In Krzysztof R. Apt, editor, Logics and Models of Concurrent Systems, volume 13 of Series F: Computer and System Sciences, pages 477–498. Springer-Verlag, 1985.Google Scholar
  21. 21.
    Dan Heller, Paula Ferguson, and David Brennan. Motif Programming Manual, 2nd edition, February 1994.Google Scholar
  22. 22.
    Gerard J. Holzmann. Design and Validation of Computer Protocols. Prentice Hall, Englewood Cliffs, N.J., 1991.Google Scholar
  23. 23.
    IBM. VisualAge: Concepts and Features, 1994.Google Scholar
  24. 24.
    Brian W. Kernighan and Dennis M. Ritchie. The C Programming Language, 2nd Ed. Prentice Hall, 1988.Google Scholar
  25. 25.
    Ralf Kneuper. Symbolic execution: a semantic approach. Science of Computer Programming, 16: 207–249, October 1991.CrossRefMATHMathSciNetGoogle Scholar
  26. 26.
    Bogdan Korel. Automated software test data generation. IEEE Transactions on Software Engineering, 16 (8): 870–879, August 1990.CrossRefGoogle Scholar
  27. 27.
    D. C. Luckham, D. P. Heimbold, S. Meldal, D. L. Bryan, and M. A. Haberler. Task sequencing language for specifying distributed ada systems. In CRAI Workshop on Software Factories and Ada, Capri, Italy, May 26–30 1986.Google Scholar
  28. 28.
    Zohar Manna and Amir Pnueli. The temporal logic of reactive systems: Specification. Springer-Verlag, 1992.Google Scholar
  29. 29.
    Lynn S. Marshall. A formal description method for user interfaces. PhD thesis, University of Manchester, 1986.Google Scholar
  30. 30.
    K. L. McMillan. The SMV system, February 1992.Google Scholar
  31. 31.
    Microsoft Corp. Windows 3.1 Programmer’s Reference, Volume 1: Overview, 1992.Google Scholar
  32. 32.
    Microsoft Corp. Windows Interface: An Application Design Guide, 1992.Google Scholar
  33. 33.
    Microsoft Corp. The GUI Guide: International Terminology for the Windows Interface 1993.Google Scholar
  34. 34.
    Microsoft Corporation. Microsoft Visual Basic Programmer’s Guide, 1993.Google Scholar
  35. 35.
    Brad A. Myers. User interface software tools. Technical Report CMU-CS-94–182, School of Computer Science, Carnegie Mellon University, August 1994.Google Scholar
  36. 36.
    Greg Nelson. A generalization of Dijkstra’s calculus. ACM Transactions on Programming Languages and Systems, 11 (4): 517–561, October 1989.CrossRefGoogle Scholar
  37. 37.
    Oscar Nierstrasz, Simon Gibbs, and Dennis Tsichritzis. Component-oriented software development. Communications of the ACM, 35 (9): 160–165, September 1992.CrossRefGoogle Scholar
  38. 38.
    Novell, Inc. Visual AppBuilder: User’s Guide, 1994.Google Scholar
  39. 39.
    Open Software Foundation. OSF/Motif Programmer’s Reference, Revision 1.1, 1991.Google Scholar
  40. 40.
    Open Software Foundation. OSF/Motif Style Guide, Revision 1.2, 1992.Google Scholar
  41. 41.
    John K. Ousterhout. Tcl and the Tk Toolkit. Addison-Wesley, 1994.Google Scholar
  42. 42.
    Philippe A. Palanque, Rémi Bastide, and Valérie Sengès. Automatic code generation from a high-level petri net based specification of dialogue. In EWHCI94: The Fourth East-West International Conference on Human-Computer Interaction, St. Petersburg, Russia, 2–6 August 1994.Google Scholar
  43. 43.
    David L. Parnas. On the use of transition diagrams in the design of a user interface for an interactive computer system. In Proceedings of the 1969 National ACM Conference, pages 379–385, 1969.Google Scholar
  44. 44.
    F. Paternó and G. Faconti. On the use of LOTOS to describe graphical interaction. In A. Monk, D. Diaper, and M. D. Harrison, editors, Proceedings of the HCI’92 Conference on People and Computers VII, pages 155–173. Cambridge University Press, September 1992.Google Scholar
  45. 45.
    Stephen W. Plain. Novell’s visual appbuilder (sidebar to: “radical development”). PC Magazine, 13 (19), November 1994.Google Scholar
  46. 46.
    Stephen R. Quinn, John C. Ware, and John Spragens. Tireless testers: automated tools can help iron out the kinks in your custom gui applications. Info World, 15 (36), September 1993.Google Scholar
  47. 47.
    M. D. Rice and S. B. Seidman. A formal model for module interconnection languages. IEEE Transactions on Software Engineering, 20 (1): 88–101, January 1994.CrossRefGoogle Scholar
  48. 48.
    Caroline Rose and Bradley Hacker et al. Inside Macintosh. Addison-Wesley, 1985.Google Scholar
  49. 49.
    SRI International under contract to DSTO Australia, Cambridge, England. The HOL System: Reference, 1989.Google Scholar
  50. 50.
    Howard Sturgis. An effective test strategy. Technical Report CSL-85–8, Xerox Palo Alto Research Center, November 1985.Google Scholar
  51. 51.
    Kari Systä. Specifying user interfaces in DisCo. SIGCHI Bulletin,26(2):53–58, 1994. Presented at a Workshop on Formal Methods for the Design of Interactive Systems, York, UK, 23rd July 1993.Google Scholar
  52. 52.
    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
  53. 53.
    Jean Vanderdonckt. The “tools for working with guidelines” bibliography. ftp://, March 1994.Google Scholar
  54. 54.
    P. Wolper. Expressing interesting properties of programs in propositional temporal logic (extended abstract). In Proceedings, Thirteenth Annual ACM Symposium on Principles of Programming Languages, pages 184–193, St. Petersburg Beach, Fla., January 1986.Google Scholar
  55. 55.
    Michal Young and Richard N. Taylor. Rethinking the taxonomy of fault detection techniques. Technical Report TR62P, Software Engineering Research Center, Department of Computer Sciences, Purdue University, September 1991. An earlier version of this paper appeared in Proceedings of the 11th International Conference on Software Engineering, Pittsburgh, May 1989.Google Scholar

Copyright information

© Springer-Verlag/Wien 1995

Authors and Affiliations

  • Peter Bumbulis
    • 1
  • P. S. C. Alencar
    • 2
  • D. D. Cowan
    • 1
  • C. J. P. Lucena
    • 3
  1. 1.Computer Science DepartmentUniversity of WaterlooWaterlooCanada
  2. 2.Departamento de Ciência da ComputaçãoUniversidade de BrasíliaBrasíliaBrazil
  3. 3.Departamento de InformáticaPontifícia Universidade Católica do Rio de JaneiroRio de JaneiroBrazil

Personalised recommendations