Skip to main content
SpringerLink
Log in

Formal Modelling of Java GUI Event Handling

  • Conference paper
  • First Online:
Formal Methods and Software Engineering (ICFEM 2002)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 2495))

Included in the following conference series:

Abstract

Programming in Java Swing and AWT can be quite error-prone due to the implicit nondeterminism caused by the complex event handling realized via multithreading. In this work, we provide a framework on formal modelling of Java GUI event handling in terms of labelled transition systems. The significance of the work is twofold: on one hand, it provides a formal basis for a better understanding and correct use of Java GUI event handling mechanism; on the other hand, it lays the ground work for formally reasoning about the correctness of a GUI-based Java application against certain properties that, due to the nondeterminism involved, may be hard to detect.

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 84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 109.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. J. Bergstra and J. Klop. Process algebra for synchronous communication. Information and Control, 60:109–137, 1984.

    Article  MATH  MathSciNet  Google Scholar 

  2. G. Booch, I. Jacobson, and J. Rumbaugh. The Unified Modeling Language User Guide. Addison-Wesley, 1998.

    Google Scholar 

  3. G. Boudol, R. de Simone, V. Roy, and D. Vergamini. Process calculi, from theory to practice: Verification tools. In Proc. of Workshop on Automatic Verification Methods for Finite State Systems, LNCS 407. Springer-Verlag, 1990.

    Google Scholar 

  4. T. Cattel. Modeling and verification of sC++ applications. In Proc. of the Tools and Algorithms for the Construction and Analysis of Systems, LNCS 1384, pages 232–248. Springer-Verlag, 1998.

    Chapter  Google Scholar 

  5. P. Cenciarelli, A. Knapp, B. Reus, and M. Wirsing. An event-based structural operational semantics of multi-threaded java. In Formal Syntax and Semantics of Java, LNCS 1523, pages 157–200. Springer-Verlag, 1999.

    Chapter  Google Scholar 

  6. J. Chen. On verifying distributed multithreaded Java programs. Software Quality Journal, 8:321–341, 1999.

    Article  Google Scholar 

  7. R. Cleaveland and S. Sims. The NCSU concurrency workbench. In Computer-Aided Verification (CAV’96), LNCS 1102, pages 394–397. Springer-Verlag, 1996.

    Google Scholar 

  8. E. Coscia and G. Reggio. A proposal for a semantics of a subset of multi-threaded “good” Java programs. In Proc. of the OOPSLA’ 98 Workshop on Formal Underpinnings of the Java Paradigm. Vancouver, Canada, October 1998.

    Google Scholar 

  9. E. A. Emerson. Temporal and modal logic. In Handbook of Theoretical Computer Science, volume B, chapter 16. Elsevier Science Publishers B.V., 1990.

    Google Scholar 

  10. E. A. Emerson. Automated temporal reasoning about reactive systems. In Logics for Concurrency: Structure versus Automata, LNCS 1043, pages 41–101. Springer-Verlag, 1996.

    Google Scholar 

  11. R. B. France, J. M. Bruel, M. M. Larrondo-Petrie, and M. Shroff. Exploring the semantics of UML type structures with Z. In IFIP Proc. of Formal Methods in Open Object-based Distributed Systems, pages 247–257. Chapman & Hall, 1997.

    Google Scholar 

  12. K. Havelund. Java PathFinder. In The 6th International SPIN Workshop, LNCS 1680 Springer-Verlag, 1999.

    Google Scholar 

  13. C. A. R. Hoare. Communicating Sequential Processes. Prentice Hall Int., London, 1985.

    MATH  Google Scholar 

  14. G. Holzmann. The Design and Validation of Computer Protocols. Prentice Hall, 1991.

    Google Scholar 

  15. G. Holzmann. The model checker SPIN. IEEE Transactions on Software Engineering, 23(5), May 1997.

    Google Scholar 

  16. D. Kozen. Results on the propositional μ-calculus. Theoretical Computer Science, 27(2):333–354, 1983.

    Article  MATH  MathSciNet  Google Scholar 

  17. J. Lilius and I. Paltor. Formalizing UML state machines for model checking. In UML’99: Lecture Notes in Computer Science 1723 Springer-Verlag, 1999.

    Google Scholar 

  18. K. L. McMillan. Symbolic Model Checking. Kluwer Academic Publishers, 1993.

    Google Scholar 

  19. R. Milner. Communication and Concurrency. Prentice Hall, London, 1989.

    MATH  Google Scholar 

  20. R. D. Nicola, A. Fantechi, S. Gnesi, and G. Ristori. An action based framework for verifying logical and behavioural properties of concurrent systems. Computer Networks and ISDN Systems, 25(7):761–778, Feb. 1993.

    Google Scholar 

  21. A. Pnueli. The temporal logic of programs. In Proc. of 18th IEEE Symp. on Foundations of Computer Science, pages 46–57. 1977.

    Google Scholar 

  22. G. Reggio, M. Cerioli, and E. Astesiano. Towards a rigorous semantics of UML supporting its multiview approach. In Proceedings of FASE 2001, LNCS 2029. Springer-Verlag, 2001.

    Google Scholar 

  23. S. Shatz, K. Mai, C. Black, and S. Tu. Design and implementation of a Petri Net based toolkit for Ada tasking analysis. IEEE Transactions on Parallel and Distributed Systems, 1(4), October 1990.

    Google Scholar 

  24. J. M. Spivey. The Z Notation: A Reference Manual. Prentice Hall, 1992.

    Google Scholar 

  25. C. Stirling. Modal and temporal logics. In Handbook of Logic in Computer Science, Volume 2, pages 477–563. Oxford University Press, 1992.

    MathSciNet  Google Scholar 

  26. C. Stirling. Modal and temporal logics for processes. In Logics for Concurrency: Structure versus Automata, LNCS, 1043, pages 149–237. Springer-Verlag, 1996.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. School of Computer Science, University of Windsor, Windsor, Ont., Canada, N9B 3P4

    Jessica Chen

Authors
  1. Jessica Chen
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. International Institute for Software Technology, United Nations University, Casa Silva Mendes, Est. do Engenheiro Trigo No. 4, P.O. Box 3058, Macao

    Chris George

  2. School of Computer Engineering and Science, Shanghai University, 149 Yanchang Road, Shanghai, 200072, P.R. China

    Huaikou Miao

Rights and permissions

Reprints and permissions

Copyright information

© 2002 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Chen, J. (2002). Formal Modelling of Java GUI Event Handling. In: George, C., Miao, H. (eds) Formal Methods and Software Engineering. ICFEM 2002. Lecture Notes in Computer Science, vol 2495. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-36103-0_37

Download citation

  • DOI: https://doi.org/10.1007/3-540-36103-0_37

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-00029-7

  • Online ISBN: 978-3-540-36103-9

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation