Article

JPF-AWT: Model checking GUI applications

Authors:

Peter Mehlitz,

Oksana Tkachuk,

Mateusz UjmaAuthors Info & Claims

ASE '11: Proceedings of the 26th IEEE/ACM International Conference on Automated Software Engineering

Pages 584 - 587

https://doi.org/10.1109/ASE.2011.6100131

Published: 06 November 2011 Publication History

Get Access

Abstract

Verification of Graphical User Interface (GUI) applications presents many challenges. GUI applications are open systems that are driven by user events. Verification of such applications by means of model checking therefore requires a user model in order to close the state space.

References

[1]

G. Brat, K. Havelund, S. Park, and W. Visser. Java PathFinder - a second generation of a Java model-checker. In Proceedings of the Workshop on Advances in Verification, July 2000.

Google Scholar

[2]

M. B. Dwyer, Robby, O. Tkachuk, and W. Visser. Analyzing interaction orderings with model checking. In ASE'04: Proceedings of the 19th IEEE international Conference on Automated Software Engineering, pages 154-163. IEEE Computer Society, 2004.

Digital Library

Google Scholar

[3]

Java PathFinder. Website. http://babelfish.arc.nasa.gov/trac/jpf.

Google Scholar

[4]

jfcUnit. Website. http://jfcunit.sourceforge.net/.

Google Scholar

[5]

JUnit. Website. http://www.junit.org.

Google Scholar

[6]

Marathon. Website. http://sourceforge.net/projects/marathonman.

Google Scholar

[7]

A. Memon, I. Banerjee, and A. Nagarajan. Gui ripping: Reverse engineering of graphical user interfaces for testing. In WCRE '03: Proceedings of the 10th Working Conference on Reverse Engineering, page 260. IEEE Computer Society, 2003.

Digital Library

Google Scholar

[8]

A. M. Memon and Q. Xie. Studying the fault-detection effectiveness of GUI test cases for rapidly evolving software. IEEE Transactions on Software Engineering, 31(10):884-896, 2005.

Digital Library

Google Scholar

[9]

SeleniumIDE. Website. http://seleniumhq.org/projects/ide.

Google Scholar

[10]

SUN. Abstract Windowing Toolkit. http://java.sun.com/products/jdk/awt/.

Google Scholar

[11]

SUN. Swing. http://download.oracle.com/javase/6/docs/technotes/guides/swing/.

Google Scholar

[12]

UISpec4J. Website. http://www.uispec4j.org.

Google Scholar

[13]

T. Yeh, T.-H. Chang, and R. C. Miller. Sikuli: Using gui screenshots for search and automation. In Proceedings of the 22nd Annual ACM Symposium on User Interface Software and Technology, UIST '09, pages 183-192, New York, NY, USA, 2009. ACM.

Digital Library

Google Scholar

[14]

X. Yuan, M. B. Cohen, and A. M. Memon. Gui interaction testing: Incorporating event context. IEEE Transactions on Software Engineering, 37(4):559-574, 2011.

Digital Library

Google Scholar

Cited By

View all

Karna AChen YYu HZhong HZhao J(2018)The role of model checking in software engineeringFrontiers of Computer Science: Selected Publications from Chinese Universities10.1007/s11704-016-6192-012:4(642-668)Online publication date: 1-Aug-2018
https://dl.acm.org/doi/10.1007/s11704-016-6192-0
Cheng LYang ZWang CRosu GDi Penta MNguyen T(2017)Systematic reduction of GUI test sequencesProceedings of the 32nd IEEE/ACM International Conference on Automated Software Engineering10.5555/3155562.3155668(849-860)Online publication date: 30-Oct-2017
https://dl.acm.org/doi/10.5555/3155562.3155668
Cheng LChang JYang ZWang CLo DApel SKhurshid S(2016)GUICat: GUI testing as a serviceProceedings of the 31st IEEE/ACM International Conference on Automated Software Engineering10.1145/2970276.2970294(858-863)Online publication date: 25-Aug-2016
https://dl.acm.org/doi/10.1145/2970276.2970294
Show More Cited By

Recommendations

Extending JPF to verify distributed systems

This paper presents our work on model checking distributed applications. We refer to distributed applications as a collection of communicating processes, regardless of their physical locations and the communication means. Our work targets applications ...
JPF verification of habanero Java programs

Habanero Java (HJ), a mid-level concurrent language, provides several correctness advantages if it is data race free: deadlock freedom, determinism, serialization, etc. An HJ program execution can only demonstrate data race freedom for one scheduling ...
Developing and executing java AWT applications on limited devices with TCPTE
ICSE '06: Proceedings of the 28th international conference on Software engineering

The paper describes TCPTE, a framework that supports the development of thin-client applications for mobile devices. By using this framework, Java AWT applications can be executed on a server and their graphical interfaces can be displayed on a remote ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

ASE '11: Proceedings of the 26th IEEE/ACM International Conference on Automated Software Engineering

November 2011

677 pages

ISBN:9781457716386

Publisher

IEEE Computer Society

United States

Publication History

Published: 06 November 2011

Check for updates

Qualifiers

Article

Conference

ASE '11

Sponsor:

ASE '11: Automated Software Engineering

November 6 - 10, 2011

Acceptance Rates

Overall Acceptance Rate 82 of 337 submissions, 24%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

10
Total Citations
View Citations
167
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 01 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

View all

Karna AChen YYu HZhong HZhao J(2018)The role of model checking in software engineeringFrontiers of Computer Science: Selected Publications from Chinese Universities10.1007/s11704-016-6192-012:4(642-668)Online publication date: 1-Aug-2018
https://dl.acm.org/doi/10.1007/s11704-016-6192-0
Cheng LYang ZWang CRosu GDi Penta MNguyen T(2017)Systematic reduction of GUI test sequencesProceedings of the 32nd IEEE/ACM International Conference on Automated Software Engineering10.5555/3155562.3155668(849-860)Online publication date: 30-Oct-2017
https://dl.acm.org/doi/10.5555/3155562.3155668
Cheng LChang JYang ZWang CLo DApel SKhurshid S(2016)GUICat: GUI testing as a serviceProceedings of the 31st IEEE/ACM International Conference on Automated Software Engineering10.1145/2970276.2970294(858-863)Online publication date: 25-Aug-2016
https://dl.acm.org/doi/10.1145/2970276.2970294
Jeon JQiu XFetter-Degges JFoster JSolar-Lezama ADillon LVisser WWilliams L(2016)Synthesizing framework models for symbolic executionProceedings of the 38th International Conference on Software Engineering10.1145/2884781.2884856(156-167)Online publication date: 14-May-2016
https://dl.acm.org/doi/10.1145/2884781.2884856
Ceccarello MTkachuk O(2014)Automated generation of model classes for Java PathFinderACM SIGSOFT Software Engineering Notes10.1145/2557833.256057239:1(1-5)Online publication date: 11-Feb-2014
https://dl.acm.org/doi/10.1145/2557833.2560572
Shafiei Nvan Breugel FCooper KScacchi WWang A(2013)Towards model checking of computer games with Java PathFinderProceedings of the 3rd International Workshop on Games and Software Engineering: Engineering Computer Games to Enable Positive, Progressive Change10.5555/2662593.2662596(15-21)Online publication date: 18-May-2013
https://dl.acm.org/doi/10.5555/2662593.2662596
Brat GMartinie CPalanque P(2013)V&V of lexical, syntactic and semantic properties for interactive systems through model checking of formal description of dialogProceedings of the 15th international conference on Human-Computer Interaction: human-centred design approaches, methods, tools, and environments - Volume Part I10.1007/978-3-642-39232-0_33(290-299)Online publication date: 21-Jul-2013
https://dl.acm.org/doi/10.1007/978-3-642-39232-0_33
Mirzaei NMalek SPăsăreanu CEsfahani NMahmood R(2012)Testing android apps through symbolic executionACM SIGSOFT Software Engineering Notes10.1145/2382756.238279837:6(1-5)Online publication date: 27-Nov-2012
https://dl.acm.org/doi/10.1145/2382756.2382798
van der Merwe Hvan der Merwe BVisser W(2012)Verifying android applications using Java PathFinderACM SIGSOFT Software Engineering Notes10.1145/2382756.238279737:6(1-5)Online publication date: 27-Nov-2012
https://dl.acm.org/doi/10.1145/2382756.2382797
Ceccarello MShafiei N(2012)Tools to generate and check consistency of model classes for Java PathFinderACM SIGSOFT Software Engineering Notes10.1145/2382756.238279637:6(1-5)Online publication date: 27-Nov-2012
https://dl.acm.org/doi/10.1145/2382756.2382796

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Cited By

Recommendations

Extending JPF to verify distributed systems

JPF verification of habanero Java programs

Developing and executing java AWT applications on limited devices with TCPTE