Testing SWING-based user-interfaces: a Case Study for HOL-TestGen

[HOL-TestGen](https://www.brucker.ch/projects/hol-testgen/) is a specification-based test case generation environment. HOL-TestGen can be used to automatically generate test-sequences, or even interactive testers. The purpose of this project is:

• to develop a formal model of a GUI programming interface (such as SWING)
• to develop a method to generate and execute low-level GUI-Testsequences
• to develop a method to specify high-level Goals of Interaction or abstract Requirements to possible interactions

Approaches:

• Capture+Replay:
  • typical tools: Abbot+Costello, Marathon, Jacareto, TestGen4Web, Selenium, WebTst,
• Script-language controlled approaches:
  • typical tools: Apodora, Concordion, FitNesse, …
• QF - Test

Links:

• https://en.wikipedia.org/wiki/Graphical_user_interface_testing
• https://en.wikipedia.org/wiki/Comparison_of_GUI_testing_tools
• https://www.infoq.com/articles/gui-automation-patterns
• https://www.youtube.com/watch?v=c91XBjfODks

Required Skills:

• Good functional programming skills
• Very basic Knowledge on Isabelle/HOL and HOL-TestGen