Skip to main content
SpringerLink
Log in

Combining Formal Techniques and Prototyping in User Interface Construction and Verification

  • Conference paper
Design, Specification and Verification of Interactive Systems ’95

Part of the book series: Eurographics ((EUROGRAPH))

Abstract

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.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  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. Apple Computer, Inc. Apple Macintosh Human Interface Guidelines, 1992.

    Google Scholar 

  3. Apple Computer, Inc. Human Interface Guidelines: The Apple Desktop Interface, 1992.

    Google Scholar 

  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. 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. 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. K. Mani Chandy and Jayadev Misra. Parallel programming. Addison-Wesley Pub. Co., 1988.

    Google Scholar 

  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. Avra Cohn. The notion of proof in hardware verification. Journal of Automated Reasoning, 5 (2): 127–140, June 1989.

    Article  MATH  Google Scholar 

  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. Digitalk. PARTS Workbench User’s Guide, 1992.

    Google Scholar 

  12. Edsger W. Dijkstra. A Discipline of Programming. Prentice-Hall, Englewood Cliffs, New Jersey, 1976.

    Google Scholar 

  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. Kevin J. Farley. Software testing for windows developers. Data Based Advisor, 11 (11), November 1993.

    Google Scholar 

  15. N. Frances. A case for a forward predicate transformer. Inf. Proc. Lett.,6(6):196–198, December 1977.

    Article  Google Scholar 

  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.

    Article  Google Scholar 

  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. 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.

    MATH  Google Scholar 

  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.

    Article  Google Scholar 

  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. Dan Heller, Paula Ferguson, and David Brennan. Motif Programming Manual, 2nd edition, February 1994.

    Google Scholar 

  22. Gerard J. Holzmann. Design and Validation of Computer Protocols. Prentice Hall, Englewood Cliffs, N.J., 1991.

    Google Scholar 

  23. IBM. VisualAge: Concepts and Features, 1994.

    Google Scholar 

  24. Brian W. Kernighan and Dennis M. Ritchie. The C Programming Language, 2nd Ed. Prentice Hall, 1988.

    Google Scholar 

  25. Ralf Kneuper. Symbolic execution: a semantic approach. Science of Computer Programming, 16: 207–249, October 1991.

    Article  MATH  MathSciNet  Google Scholar 

  26. Bogdan Korel. Automated software test data generation. IEEE Transactions on Software Engineering, 16 (8): 870–879, August 1990.

    Article  Google Scholar 

  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. Zohar Manna and Amir Pnueli. The temporal logic of reactive systems: Specification. Springer-Verlag, 1992.

    Google Scholar 

  29. Lynn S. Marshall. A formal description method for user interfaces. PhD thesis, University of Manchester, 1986.

    Google Scholar 

  30. K. L. McMillan. The SMV system, February 1992.

    Google Scholar 

  31. Microsoft Corp. Windows 3.1 Programmer’s Reference, Volume 1: Overview, 1992.

    Google Scholar 

  32. Microsoft Corp. Windows Interface: An Application Design Guide, 1992.

    Google Scholar 

  33. Microsoft Corp. The GUI Guide: International Terminology for the Windows Interface 1993.

    Google Scholar 

  34. Microsoft Corporation. Microsoft Visual Basic Programmer’s Guide, 1993.

    Google Scholar 

  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. Greg Nelson. A generalization of Dijkstra’s calculus. ACM Transactions on Programming Languages and Systems, 11 (4): 517–561, October 1989.

    Article  Google Scholar 

  37. Oscar Nierstrasz, Simon Gibbs, and Dennis Tsichritzis. Component-oriented software development. Communications of the ACM, 35 (9): 160–165, September 1992.

    Article  Google Scholar 

  38. Novell, Inc. Visual AppBuilder: User’s Guide, 1994.

    Google Scholar 

  39. Open Software Foundation. OSF/Motif Programmer’s Reference, Revision 1.1, 1991.

    Google Scholar 

  40. Open Software Foundation. OSF/Motif Style Guide, Revision 1.2, 1992.

    Google Scholar 

  41. John K. Ousterhout. Tcl and the Tk Toolkit. Addison-Wesley, 1994.

    Google Scholar 

  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. 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. 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. Stephen W. Plain. Novell’s visual appbuilder (sidebar to: “radical development”). PC Magazine, 13 (19), November 1994.

    Google Scholar 

  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. 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.

    Article  Google Scholar 

  48. Caroline Rose and Bradley Hacker et al. Inside Macintosh. Addison-Wesley, 1985.

    Google Scholar 

  49. SRI International under contract to DSTO Australia, Cambridge, England. The HOL System: Reference, 1989.

    Google Scholar 

  50. Howard Sturgis. An effective test strategy. Technical Report CSL-85–8, Xerox Palo Alto Research Center, November 1985.

    Google Scholar 

  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. 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://Ial.cs.byu.edu/pub/hol/holsys.tar.gz.

    Google Scholar 

  53. Jean Vanderdonckt. The “tools for working with guidelines” bibliography. ftp:// arzach.fundp.ac.be/pub/papers/jvdd/Tools_fww_guidelines.txt, March 1994.

    Google Scholar 

  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. 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 

Download references

Author information

Authors and Affiliations

  1. Computer Science Department, University of Waterloo, Waterloo, Ontario, Canada

    Peter Bumbulis & D. D. Cowan

  2. Departamento de Ciência da Computação, Universidade de Brasília, Brasília, Brazil

    P. S. C. Alencar

  3. Departamento de Informática, Pontifícia Universidade Católica do Rio de Janeiro, Rio de Janeiro, Brazil

    C. J. P. Lucena

Authors
  1. Peter Bumbulis
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. P. S. C. Alencar
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. D. D. Cowan
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. C. J. P. Lucena
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. LIS/Université Toulouse I, Toulouse Cedex, France

    Philippe Palanque  & Rémi Bastide  & 

Rights and permissions

Reprints and permissions

Copyright information

© 1995 Springer-Verlag/Wien

About this paper

Cite this paper

Bumbulis, P., Alencar, P.S.C., Cowan, D.D., Lucena, C.J.P. (1995). Combining Formal Techniques and Prototyping in User Interface Construction and Verification. In: Palanque, P., Bastide, R. (eds) Design, Specification and Verification of Interactive Systems ’95. Eurographics. Springer, Vienna. https://doi.org/10.1007/978-3-7091-9437-9_11

Download citation

  • DOI: https://doi.org/10.1007/978-3-7091-9437-9_11

  • Publisher Name: Springer, Vienna

  • Print ISBN: 978-3-211-82739-0

  • Online ISBN: 978-3-7091-9437-9

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation