Uppaal Test Case Generator demo

The following describes the test case generation features in Uppaal by using a simple Java program toggling value up and down.

Model Annotations

Test Case Generation

Test case generator uses verification engine to find the system traces, collect the Test Code along those traces and save them as test script files.

Test Case Execution

The generated test cases are executed by running the following scripts: test.sh on Unix or test.bat on Windows. The scripts assume that all test cases are saved in their current directory by following the TestCase-*.java pattern (as specified in updown.xml), compile the app/AppC.java implementation, compile the test case and run it.

The app dirctory also contains faulty implementation and the test cases can be run against it by executing the corresponding scripts: testMutant.sh on Unix and testMutant.bat on Winduws.