CharonTester

Online Manual

1. Launch CharonTester

After installing the CharonTester, go to your installation directory. On linux. type "./run_testgen.sh", or on Windows, type "run_testgen.bat" to start Charon. CharonTester is embedded in the "test" section on the menu bar.

2. Load a Charon Model

You may refer to the Charon online resource for the information how to model a hybrid system in Charon and use the Charon IDE.

The CharonTester distribution includes an example CoffeeMachine. To load CoffeeMachine, choose "File/Open Project" and load coffeeMachine.prj.

3. Change the setting for test generation.

To change the setting, go to "Test/Configure Generator".

  1. Maximal Length of a Test: define the upbound a test case. Test generator will search tests within the given length.
  2. Integration Step Size: define the step size in a test case. A test discretizes a continuous trace of a Charon model. The step size decides the time interval between each sample points.
  3. Coverage Criteria: you can choose either "Mode Coverage" or "Transition Coverage". The CharonTester generates a set of tests, if necessary, to achieve the desired the coverage. For more information, refer to understand results.
  4. Strategy: the CharonTester implements two advanced test generation strategies in addition to the basic simulation-based strategy. Note. as of May 8, these functions haven't enabled on the UI.
  5. Debug Information: decide if you want additional debug informations on the command line.

4. Create on-the-fly test generator

CharonTester will create a customized test generator for a Charon model. After loading your model and choosing the test setting, choose "Test/Create Generator" to create the customized test generator. You will see the message on the command window like,

Charon home is in .
No syntax error.
Global Simulator will be generated.
%GlobalGen.class: agent init block should be in an atomic agent

Global simulator is generated.
To compile: javac CHARON\simulator\CoffeeMachinerTest.java
To run: java CHARON.simulator.CoffeeMachinerTest [int: the maximum number of simulation rounds]

compiling the simulator...
Note: .\CHARON\simulator\CoffeeMachinerTest.java uses unchecked or unsafe operations.
Note: Recompile with -Xlint:unchecked for details.
done

If the CharonTester hangs on "Compile the simulator ...", make sure that your JDK binary directory has been added to the PATH and the CLASSPATH points to your JDK installation directory.

4. Run test generator

After creating the customized test generator, choose "Test/Run Generator/Start" to start test generation.

Progress panel shows the structural information of the model and the progress of test generation.

  • The top-left corner of the panel shows the static structural information of the model including the number of agents, models, and transitions. The right-left side shows the progress of the test generation in terms of how many modes and transitions were covered and how many test traces have been generated.
  • At any time, you can click "stop" to terminate the test generation process, and you are still able to acess the test traces generated

4. Understand results

The tests generated are put into the "testsuite" subdirectory under your Charon project directory. Tests are marked sequentially by a set of subdirectories "trace1"..."traceN". In each trace directory,

CoffeeMachinegTest.rep

graphCoffeeMachinegTest.rep

trLogCoffeeMachinegTest.rep

coveredmode.txt

coveredtrans.txt

uncoveredmode.txt

uncoveredtrans.txt

The file $ModelName$gTest.rep is a space-seperated multi-column data file which can be accepted by most of plotting software. It shows the step-by-step changes of values of control and data variables. One way to display the trace is to use "Simulate/Display Simulation Trace" and open $ModelName$gTest.rep. The file trLog$ModelName$gTest.rep shows transitions performaned during a test.

coveredmode.txt and coveredtrans.txt show the modes and transitions covered by the test trace. uncoveredmode.txt and uncoveredtrans.txt show the modes and the transitions which have been covered yet and hence require additional tests.