-
Notifications
You must be signed in to change notification settings - Fork 5
Home
Welcome to the EvoMBT wiki!
EvoMBT implements the Model-Based Testing generation cycle that comprises four steps
- abstract the system under test (SUT) in an appropriate model. EvoMBT uses Extended Finite State Machines (EFSMs) [1] as the modelling formalism to capture the behaviour of the SUT;
- derive abstract test cases from the model;
- concretise the abstract test cases generated on the EFMS in a format that the SUT can understand;
- execute the concrete test case on the SUT.
The core of EvoMBT is the generation of the abstract test cases from a given EFSM. This part is completely independent from the specific SUT considered. Given an EFSM, EvoMBT applies different search heuristics to find test cases that satisfy the desired coverage criteria, e.g., state or transition coverage. EvoMBT relies on the well known EvoSuite tool as a library for the various search algorithms. The other steps of the MBT cycle, i.e., abstraction of the model, concretisation, and execution on the SUT, are specific to the particular SUT. EvoMBT has built-in support for the 3D game Lab Recruits [2] and for the BeamNG.tech driving simulator [3].
- First run
- Traffic light example
- EvoMBT output
- EvoMBT parameters
- Supported systems
- Using EvoMBT as a Java library
- References
EvoMBT build is managed by Maven, and it should suffice to run the following command from the project root:
mvn clean package -DskipTests
which should perform a basic build and produce an executable jar EvoMBT-x.x.x-jar-with-dependencies.jar
in the target
folder. This build does not run the regression test suite of EvoMBT. It is however recommended to run the build with the regression suite at least once (i.e., run the build command omitting the -DskipTests
flag).
To have a flavour of EvoMBT run the following command
java -jar target/EvoMBT-x.x.x-jar-with-dependencies.jar -sbt
This launches EvoMBT on a simple example model distributed with the package. If all works correctly, the tool prints the message
Final coverage: 100.0%
and creates the folder mbt-files, with two subfolders: tests and statistics.
Let us consider a more complex example, an EFSM describing a traffic light at a pedestrian crosswalk (see pag. 60 of [4]). Here, a graphical representation of the EFSM model
The model includes four states, red, green, yellow, and pending, and an internal variable count. The time is explicit, i.e., each transition consumes a unit of time (seconds for instance). The system starts in red and waits 60s seconds checking the variable count and then moves to green. Then, the system waits for pedestrians. When a pedestrian arrives, if the count is less than 60s, the system goes to pending, letting the pedestrian wait for the count to reach 60. Instead, if the traffic light was green for at least 60s, the light becomes yellow for 5 seconds before going to red. The EFSM has also outputs that correspond to light colours.
To run test generation for the traffic light EFSM above, run
java -jar target/EvoMBT-x.x.x-jar-with-dependencies.jar -sbt -Dsut_efsm=examples.traffic_light
This command performs test generation on transition coverage criteria for traffic light EFSM model using MOSA algorithm with 60s of time budget. Subfolder mbt-files\tests\examples.traffic_light\MOSA contains abstract tests generated. An example of a test case generated is reported here. The test performs 60 times the self-loop in state red, making the variable count reach the value of 60. Then, the system goes from red to green and starts waiting for a pedestrian. After 24 cycles, the system receives the input from the pedestrian and goes to state pending. To have a value of count=60, which allows the system to move to the state yellow, the system stays in the state pending for 35 cycles. Finally, the system cycles 5 times in state yellow and then returns to state red.
Likely, the test generation reaches 100% of coverage, i.e., all the transitions are covered. However, the search has a stochastic component and it could be that different values are obtained. To make the experiments almosta repeatable, we could specify the seed of the random generator used by EvoMBT
java -jar target/EvoMBT-x.x.x-jar-with-dependencies.jar -sbt -Dsut_efsm=examples.traffic_light -Drandom_seed=1234
With random seed 1234, EvoMBT generates nine test cases that can be found in the folder mbt-files.
By default, EvoMBT uses MOSA test generation strategy, but it is also possible to use random search:
java -jar target/EvoMBT-x.x.x-jar-with-dependencies.jar -random -Dsut_efsm=examples.traffic_light -Drandom_seed=094309
With the default time budget (60s), random search reaches a coverage of 11%, i.e., 1/9 transitions are covered. In particular, only the self-loop transition in state red is covered, as, to go from red to green, the random search has to select the red state self-loop at least 60 times consecutively, quite an unlikely event.
Using the traffic light example, we will explore the main EvoMBT input parameters in the next section.
By default, EvoMBT creates a folder named mbt-files in the same location EvoMBT is run. Folder mbt-files contains folders statistics and tests.
Folder statistics contains the file statistics.csv, that collects data about the test case generation process. Each time EvoMBT runs, execution statistics are appended to this file. The statistics snapshots are taken every 10 seconds, however this could be modified by setting the corresponding parameter when launching EvoMBT. The statistics file has 15 columns:
- id: a unique id to retrieve the generated tests in folder tests. There could be multiple lines with the same id, representing snapshots of the same generation process;
- covered_goals: number of covered goals;
- sut: SUT under test;
- coverage: fraction of covered goals;
- tests: number of generated test cases;
- budget: total budget (in seconds) for the test generation project (default 60s);
- consumed_budget: budget consumed until the current snapshot. Given an id, the consumed represent the time at which EvoMBT taks a snapshot of the generation process. By default, EvoMBT takes a snapshot each 10s;
- fitness_evaluations: number of times the fitness function is evaluated;
- feasible_paths: total number of feasible paths found on the current EFSM;
- feasible_rate: estimate of the fraction of feasible paths of the current EFSM;
- algorithm: search strategy used;
- criteria: coverage criteria used;
- random_seed: seed of the random number generator;
- lr_seed: Lab Recruits specific random seed.
File statistics.csv gives an overview of the test generation process and allows to evaluate test generation performances. Many parameters, as budget or algorithm can be customised (see EvoMBT parameters).
Folder tests has a subfolder for each considered SUT. Within each SUT subfolder, there is a folder for each used algorithm. Within each algorithm subfolder, there is a folder for each experiment with a random generated name that correspond to the column id in statistics.csv file. In this way, it is possible to associate each generated test suite the proper examples. Let's consider an example of tests folder.
- tests
- cps.beamng_custom_model
- MONOTONIC_GA
- 1665064599362
- MOSA
- 1665064575554
- 1665064873863
- MONOTONIC_GA
- examples.traffic_light
- MOSA
- 1664972192380
- 1664972196360
- RANDOM
- 1664973161266
- 1664973266802
- 1664973351541
- MOSA
- labrecruits.random_simple
- MU_LAMBDA_EA
- 1665064741562
- MU_LAMBDA_EA
- cps.beamng_custom_model
This tests folder represents a situation where three SUT are tested. For cps.beamng_custom_model there is a run with monotonic genetic algorithm and two with MOSA. For examples.traffic_light, there are two runs with MOSA and three runs with RANDOM. Finally, there is a run for labrecruits.random_simple SUT using mu,lambda evolutionary algorithm.
EvoMBT has a number of parameters that can be exposed by using the -help
option:
java -jar target/EvoMBT-x.x.x-jar-with-dependencies.jar -help The main parameters are the following:
-
-sbt
: EvoMBT uses test case based search algorithms for test generation. By default the MOSA algorithm is used, but a different algorithm can be provided as-Dalgorithm=<AlgorithmName>
-
-wholesuite
: EvoMBT uses whole test suite based search algorithm for test generation. -
-random
: EvoMBT uses random test generation strategy -
-exec_on_sut
: execute tests on the actual system under test, by default supported for Lab Recruits. Additional parameters need to be supplied (e.g., path to SUT executable), detailed below. -
-sut_exec_dir,--sut_exec_dir <arg>
: (currently only for Lab Recruits) path to the gym folder containing the Lab Recruits executables. Binaries distributed for Windows, Linux, and Mac. -
-sut_executable,--sut_executable <arg>
: (currently only for Lab Recruits) path to the csv file describing the level of the game under test. -
-tests_dir,--tests_dir <arg>
: (currently only for Lab Recruits) path to the folder containing tests to be executed on the SUT -
-agent_name,--agent_name <arg>
: (currently only for Lab Recruits) name of the agent in the level, defaults to 'Agent1' -
-max_cycles,--max_cycles <arg>
: (currently only for Lab Recruits) maximum number of update cycles the agent is allowed for executing a given goal -
-mutation_analysis
: (currently only for Lab Recruits) run mutation analysis on the actual system under test. Use-Dmax_number_mutations=X
to run on at most X mutations. (Default 10) -
-silent_mode
: save only execution statistics. Model and tests are not saved on disc. This could be particularly useful when running a large number of experiments hence the generated data could occupy a large amount of space on disk.
In addition to the above high-level parameters, EvoMBT has a number of other parameters that can be set using the syntax
-D<parameter_name>=<parameter_value>
. Any number of parameters could be passed at a time by repeating the parameter-value pair as: -Dparam1=val1 -Dparam2=val2 -DparamN=valN
. For a full list of the parameters that can be set in this way, please refer to the MBTProperties class.
[1] Cheng, K. T., & Krishnakumar, A. S. (1993, June). Automatic functional test generation using the extended finite state machine model. In 30th ACM/IEEE Design Automation Conference (pp. 86-91). IEEE.
[2] R. Ferdous, F. M. Kifetew, D. Prandi, I. S. W. B. Prasetya, S. Shirzadehhajimahmood, A. Susi. Search-based automated play testing of computer games: A model-based approach. 13th International Symposium, SSBSE 2021. doi:10.1007/978-3-030-88106-1_5.
[3] R. Ferdous, C. Hung, F. M. Kifetew, D. Prandi, A. Susi. EvoMBT. 15th IEEE/ACM International Workshop on Search-Based Software Testing (tool competition), SBST@ICSE 2022. doi:10.1145/3526072.3527534.
[4] Lee, E. A., & Seshia, S. A. (2011). Introduction to embedded systems. A cyber-physical systems approach, 499. ISBN 978-0-557-70857-4.
a. due to rounding, there could be exceptions.