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.
Keywords
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
J. Bergstra and J. Klop. Process algebra for synchronous communication. Information and Control, 60:109–137, 1984.
G. Booch, I. Jacobson, and J. Rumbaugh. The Unified Modeling Language User Guide. Addison-Wesley, 1998.
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.
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.
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.
J. Chen. On verifying distributed multithreaded Java programs. Software Quality Journal, 8:321–341, 1999.
R. Cleaveland and S. Sims. The NCSU concurrency workbench. In Computer-Aided Verification (CAV’96), LNCS 1102, pages 394–397. Springer-Verlag, 1996.
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.
E. A. Emerson. Temporal and modal logic. In Handbook of Theoretical Computer Science, volume B, chapter 16. Elsevier Science Publishers B.V., 1990.
E. A. Emerson. Automated temporal reasoning about reactive systems. In Logics for Concurrency: Structure versus Automata, LNCS 1043, pages 41–101. Springer-Verlag, 1996.
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.
K. Havelund. Java PathFinder. In The 6th International SPIN Workshop, LNCS 1680 Springer-Verlag, 1999.
C. A. R. Hoare. Communicating Sequential Processes. Prentice Hall Int., London, 1985.
G. Holzmann. The Design and Validation of Computer Protocols. Prentice Hall, 1991.
G. Holzmann. The model checker SPIN. IEEE Transactions on Software Engineering, 23(5), May 1997.
D. Kozen. Results on the propositional μ-calculus. Theoretical Computer Science, 27(2):333–354, 1983.
J. Lilius and I. Paltor. Formalizing UML state machines for model checking. In UML’99: Lecture Notes in Computer Science 1723 Springer-Verlag, 1999.
K. L. McMillan. Symbolic Model Checking. Kluwer Academic Publishers, 1993.
R. Milner. Communication and Concurrency. Prentice Hall, London, 1989.
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.
A. Pnueli. The temporal logic of programs. In Proc. of 18th IEEE Symp. on Foundations of Computer Science, pages 46–57. 1977.
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.
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.
J. M. Spivey. The Z Notation: A Reference Manual. Prentice Hall, 1992.
C. Stirling. Modal and temporal logics. In Handbook of Logic in Computer Science, Volume 2, pages 477–563. Oxford University Press, 1992.
C. Stirling. Modal and temporal logics for processes. In Logics for Concurrency: Structure versus Automata, LNCS, 1043, pages 149–237. Springer-Verlag, 1996.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights 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