Test Execution Framework in HOL-TestGen
Description
[HOL-TestGen](https://www.brucker.ch/projects/hol-testgen/) is a specification-based test case generation environment. While HOL-TestGen allows to generate test cases, it currently lacks a state of the art framework for executing tests as well as monitoring and analysing the test runs.
In this project, a generic test execution and reporting framework (e.g., similar to the core of [JUnit](http://junit.org) but instead of writing test cases manually, they are automatically generated by HOL-TestGen) for [HOL-TestGen](https://www.brucker.ch/projects/hol-testgen/) will be developed that supports various test scenarios (e.g., unit tests, sequence tests) as well as implementation technologies.
Usually, either a significant (non-trivial) programming task or a signifiant theoretical contribution are expected to make up a suitable project.
Skills required:
- Good programming skills
- An interest in functional programming (e.g, SML, Ocaml, Haskell)
- An interest in testing
- An interest in formal methods and/or theorem proving (e.g., Isabelle/HOL)
Initial reading and useful links:
* HOL-TestGen: <https://www.brucker.ch/projects/hol-testgen/>
- JUnit: <http://junit.org>
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
Generating Concurrent Code from Isabelle/HOL-CSP specifications
CSP