Welcome to TAUC

TAUC is a toolset to generate test cases addressing software timeliness. The toolset has been developed by Chunhui Wang, at the SVV lab of the University of Luxembourg.

Why TAUC?

Experiments proved that TAUC can generate effective test suite addressing software timing requirements (up to 31% additional fault coverage than manually written test cases). TAUC spares software engineers from the burden of creating very detail test model in order to generate full executable timeliness test cases, when the design artefacts are available to use.

Requirements

• Mac OS X / Linux / Windows
• Java 1.7+
• UPPAAL 4.1.19

Structure of TAUC distribution

.
+-- Aritifacts
|   +-- DomainModel       //Domain model for distributed example.
|   +-- ModelTestGeneration //Timeliness test model for test generation.
|   +-- ModelVerification  //Timeliness test model for verification.
+-- TAUC
|   +-- bin-Linux   //UPPAAL model checking server binary for Linux.
|   +-- bin-MacOS   //UPPAAL model checking server binary for MacOS.
|   +-- bin-Win32   //UPPAAL model checking server binary for Windows.
|   +-- lib         //Library dependencies for executable jars.
|   +-- taucGen.jar
|   +-- muta.jar
|   +-- vmodel.jar
|   +-- verifier.jar
|   +-- createVModel.sh

TAUC distribution includes a sanitized example models: RUCM uses case and domain model.

The executable jars can be classified into two categories:

Test Generation

TAUC test generator - taucGen.jar, which takes Timeliness Test Model (UPPAAL Model files embedded with environment, scenario, and augmented timing requirements automata) as inputs and generates Timeliness test suite.

~$ java -jar taucGen.jar
usage: taucGen.jar
 -i <InputModels>         File/Folder contains Timeliness Model.
 -d <DomainModel>         Domain Model File.
 -o <PathForTestSuite>    Specify the path to save test suite.
 -t <PathForTrace>        Specify the path to save traces.
 -m <NumberOfIteration>   Specify number of Iteration.
 -n <SizeOfTestSuite>     Size of generated test suite.
 -r                       Random test generation strategy instead TAUC.
 -p                       Print test generation statistics.

Evaluation

Evaluation Module contains several components:

• Firstly muta.jar was used to automatically mutate Timeliness test model by a subset of mutation operators suggested in [1][2], which may impact timing requirements. This allow the generation of mutants that represent faulty implementations of system.

~$ java -jar muta.jar
usage: muta.jar
 -f <ModelFile>      Timeliness model file to mutate.
 -m <MutaOps>        List of mutation operators.
 -o <PathForMutants> Specify the path to save generated mutants.
 -s <OffsetValue>    Required for widen|shift|restrict MutaOps.
 -t <TemplateName>   Specify the template to mutate.
 -c <ConfigFile>     Load configuration from config file.

MutaOps is a comma separated list and can be any combination of the following items: WidenTimeGuardStrategy, ShiftTimeGuardStrategy, RestrictTimeGuardStrategy and SelfLoopStrategy.

Configuration can be loaded from a config file instead of command-line arguments. Once config file is specified by -c, other command-line arguments will be ignored. Here is a example of config file.

• Secondly, vmodels.jar translates generated test cases into sequential timed automata by following the approach described in [3], and embedded them into each generated mutants from the previous step. The generated models which composed by sequential timed automata (test cases) and mutated timeliness test model (faulty implementations) are called "verification model", vmodel for short.

~$ java -jar vmodel.jar
usage: java -jar vmodel.jar
 -c <ClassPathOfTestCases>   Specify the class path of test cases.
 -i <Mutants>                File/Folder contains mutants.
 -o <PathForVModel>          Specify the path to save vmodels.

By default, vmodels.jar execute and translate test cases dynamically by using Java Reflection, thus test case folder was required in command line argument. This also requires generated test cases have been compiled based on a adaptor library by the following command.

~$ javac -cp uppaal-test-adaptor.jar <PathOfTestCases>/*.java

For convenience, please use the provided batch script createVModel.sh, which will first compile the test cases and then create VModels.

~$ createVModel.sh
Usage:
./createVModel.sh <PathOfTestCases> <Mutants> <PathForVModel>

• Finally, each vmodel file is verified by verifier.jar, which verifies each test case from generated test suite against each mutant. A mutant was killed by the test suite when at least one test case failed.

~$ java -jar verifier.jar
usage: verifier.jar
 -i <VModels>     VModel file/folder to verify.
 -p <TC-Prefix>   Prefix for the name of test case templates.
 -f               Fast verification(stop when first killed).
 -s               Print verification Statistics.

The command-line arguments -p indicates the prefix for the name of test case templates. Conventionally, each test case was translated into a sequential timed automata and named as test0, test1, test2, ... etc. Thus, here the prefix is "test".

IMPORTANT NOTES:

The lib folder contains all the library dependencies, thus it should be placed under the same folder with executable jars.

The bin-OS folder contains UPPAAL binaries for different platforms, which are also required and should be placed under the same folder with executable jars.

Support or Contact

Having trouble with TAUC? Please feel free to contact support, we would like to help you sort it out.

Reference

[1] M. S. Aboutrab, M. Brockway, S. Counsell, and R. M. Hierons, “Testing real-time embedded systems using timed automata based approaches,” J. Syst. Softw., vol. 86, no. 5, pp. 1209–1223, May 2013.

[2] B. K. Aichernig, F. Lorber, and D. Nicˇkovic ́, Time for Mutants — Model- Based Mutation Testing with Timed Automata. Berlin, Heidelberg: Springer Berlin Heidelberg, 2013, pp. 20–38.

[3] A. Hessel, K. G. Larsen, B. Nielsen, P. Pettersson, and A. Skou, Time-Optimal Real-Time Test Case Generation Using Uppaal. Berlin, Heidelberg: Springer Berlin Heidelberg, 2004, pp. 114–130.