Static detection of equivalent mutants in real-time model-based mutation testing

Timed games (TG) are transition systems which can remain in a certain state or location only a specific amount of time, can execute a transition only within a certain time interval, and distinguish between controllable and uncontrollable actions. TG are based on timed (game) automata (Alur and Dill 1994; Asarin et al. 1998) and form the underlying behavioral structure of featured timed game (automata) (Cordy et al. 2012b; Cordy et al. 2013).

In reactive systems, one usually distinguishes between uncontrollable and controllable actions, that are assigned to inputs and outputs, respectively, if the environment is uncontrollable and vice versa otherwise.

We denote by CC(C) the set of clock constraints over C. In TG, a clock constraint can label either a state or a transition. In case it labels a state, the constraint is a location invariant, which defines the interval of time in which the system can be in the state. In case it labels a transition, it is a transition guard specifying the interval of time during which the system can execute the transition. Note that the domain of the numeric constants in clock constraints is limited to natural numbers. Without loss of generality, we could use real numbers. However, natural numbers facilitate the implementation of clock constraints by allowing efficient data structures.

For a transition \(t = (\ell , g, \alpha , R, \ell ^{\prime })\), ℓ is the starting location, g is the transition guard, α is the action triggering the transition, R is the subset of clocks to reset, and \(\ell ^{\prime }\) is the target location. We may also write t as \(\ell \xrightarrow {g,\alpha ,R} \ell ^{\prime }\) and omit g and/or R when immaterial, and instead of {x} for a reset of clock x, we may also write x := 0.

The semantics of a TG is commonly defined as an infinite transition system (TS) whose states consist of a location and a valuation of the clocks. The transitions can be categorised into two types. Delay transitions do not change the location of the system, but only represent the passing of time. They may occur only if the invariant of the current location is still satisfied after the delay modelled by the transition. Discrete transitions instead occur when the system moves from one location to another. They may occur only if the current clock values satisfy both the guard of the executed transition and the invariant of the target location. After the execution of such transitions, clock values can be reset.

Featured timed games (FTG) extend TG with variability in the same way that featured transition systems (FTS) (Classen et al. 2013) extend (labelled) transition systems (LTS). FTS concisely model the behaviour of all products of a product line in a single superimposed LTS through the annotation of transitions with feature expressions, i.e., conditions expressing their existence in products, based on a feature model.

We assume products to be represented by sets of Boolean features and a feature model to be defined as a pair \((F,P\subseteq 2^{F})\), where F is a set of features and P is the set of valid products. The semantics of a feature model φ, denoted by [ [φ] ]_FM, is then its set of valid products. It can be represented by either a propositional formula or by the usual feature diagram. Let \(\mathbb {B} = \{\top ,\bot \}\) denote the Boolean constants true (⊤) and false (⊥), and let \(\mathbb {B}(F)\) denote the set of Boolean expressions over F (i.e., using features as propositional variables). The elements of \(\mathbb {B}(F)\) are also called feature expressions. Formally, a feature expression χ is a total function \(\{\top ,\bot \}^{|F|} \rightarrow \{\top ,\bot \}\) that associates every combination of features with a truth value. A feature expression can be interpreted as a set of products \([\![\chi ]\!]\subseteq 2^{F}\) defined as all products p for which the induced truth assignment (⊤ for f ∈ p, ⊥ for f∉p, for features f ∈ F) validates χ. Feature expressions and clock constraints allow modelling the behaviour of real-time variable-intensive systems.

As for FTS, the function γ associates a feature expression χ to some transition \(t = (\ell , g, \alpha , R, \ell ^{\prime })\) such that γ(t) = χ encodes the set of products able to execute t. We may also write t as \(\ell \xrightarrow {[\chi ]g,\alpha ,R} \ell ^{\prime }\) and omit g and/or R when immaterial. The function γ moreover associates a feature expression χ to a location invariant Inv(ℓ) = g, for some ℓ ∈Loc, such that γ(g) = χ, which we may also write as [χ]g, encodes the set of products with the invariant g in location ℓ. Note that [⊤] stands for a feature expression that is always satisfied (by any product).

FTG model real-time behaviour of a product line. Moreover, from an FTG we can derive TG modelling behaviour of specific products. This is achieved by projection of an FTG onto a product p obtained in much the same way as an LTS is obtained from an FTS (Classen et al. 2013): all transitions and invariants unavailable in product p are removed.

The semantics of an FTG model of a product line is defined as a function that associates every valid product with the semantics of its projection.

The idea underlying model-based mutation testing is to guide the test-case generation by mutants, which are typically obtained through random mutations of the original model. Organising the mutants as a product line of mutations, a family of variations of the system under test (SUT), coined the featured mutant model (FMM) in Devroey et al. (2016), enables the efficient generation, configuration, and execution of mutants. Each feature in the FMM corresponds to a single application of one mutant operator on the original model.

Like Devroey et al. (2016), we use a selection of the operators proposed by Fabbri et al. (1999), based on Chow (1978) and Weyuker et al. (1994), to generate mutants from a TS:

Additionally, we introduce the following operators specific to timed models, which change the constant in clock constraints, which we recall to be either a transition guard or a location invariant:

The CCN operator is inspired by the μ_ng operator from Aichernig et al. (2013), where only clock constraints appearing as transition guards are negated.

Each operator can be used to generate mutants using either the enumerative approach or the FMM approach. In the enumerative approach, each mutation transforms an FTG model ftg, representing the SUT behaviour, into a mutant ftg_m.

In the FMM approach, each mutation operator is added as a feature to the existing feature model. When considering first-order mutation (only one mutation can be applied to the original system), the features/mutations are mutually exclusive. For higher order mutations, disjunction is used instead.

Hence, mutation operators are added to the FMM under construction.

To begin with, we formalise the notion of refinement between TG, adapted from David et al. (2010a) and Larsen et al. (2017). In Larsen et al. (2017), real-time systems are modelled as timed I/O automata, in which input actions are defined controllable and output actions are defined uncontrollable. The main idea is to perform a refinement check between the mutant and the system model, using Ecdar (David et al. 2010b), which is a tool built on top of Uppaal TIGA (Behrmann et al. 2007) that implements the timed interface theory from David et al. (2010a). Basically, a refinement model (i.e., a live mutant) must be able to mimic all controllable transitions of the original system model, while the original model must be able to mimic all uncontrollable transitions of the refinement. In our case, controllable transitions correspond to inputs (since a live mutant must accept all inputs that the original system accepts), whereas uncontrollable transitions correspond to outputs and delays (since a live mutant should not exhibit any behaviour that does not belong to the system). Note that this is the opposite of the standard notion of modal refinement, where the inputs are seen as sent by an uncontrolled environment (Larsen et al. 2007). In other words, here the viewpoint is switched to the environment (David et al. 2010a; Larsen et al. 2017).

We now provide a definition of subsumed mutant, where Op_fmm is the set of mutations. Basically, after applying an additional mutation the resulting mutant is a refinement of the former one on which the additional mutation was not applied.

We only consider deterministic TG, as usual (Larsen et al. 2017; Aichernig et al. 2015; Aichernig et al. 2013). The following proposition identifies conditions under which a mutant is subsumed.

In the remainder of this section, we present several results for identifying mutations that generate subsumed mutants by construction. Proof (sketches) can be found in Basile et al. (2020a). We start with those operations that were proposed by Fabbri et al. (1999), followed by the novel ones introduced in this paper.

We continue with the mutation operators that were firstly introduced in Basile et al. (2020a).

Although our focus is on detecting subsumed mutants, the developed theory is also helpful in spotting when a specific mutation yields by construction a non-subsumed mutant. The following auxiliary results target non-subsumed mutants and complement the results stated so far (from Basile et al. 2020a). At this point, it is important to note that the experiments in Section 5 will only exploit results on subsumed mutants to discard ineffective mutations. However, the auxiliary results presented in this section could be exploited to perform a different evaluation: instead of discarding subsumed mutants, only generate (statically known) non-subsumed ones. This evaluation is harder, because only in specific cases it is possible to statically detect when a mutation is non-redundant. This is left for future work. A TG is said to be non-redundant if every location ℓ is reachable in at least one trace, it is not time-locked (i.e., delay is possible), and every transition is executable in at least one trace. For the non-subsumed lemmata, we will only consider non-redundant TG. Indeed, mutating a redundant element may produce a subsumed mutant. Note that redundant specifications are ill-defined and should be amended prior to any application, be it testing, model checking or any other.

We introduce the auxiliary definition of non-redundancy preserving mutation. This will be useful for the forthcoming results about non-redundant higher order mutations, whose hypothesis is that the mutated mutant is non-redundant.

Proof (sketches) of the results already reported earlier can be found in Basile et al. (2020a).

Below follow two generic results on non-redundancy preserving on location or transition for any mutation. Note that the results below are operating at the syntactic level (i.e., statically). This means that the information on the specific values of clocks is missing. This information is only known at the semantics level (i.e., during the execution), where states are pairs of locations and clock evaluations. However, under specific hypothesis, it is possible to infer (statically) the values of clocks. Intuitively, if all clocks are reset when entering a location, the clocks evaluation when entering the location is statically known to be zero, and it is possible to predict whether guards and invariants will be satisfied. This allows to provide a result on non-redundancy preserving of a generic mutation involving a location that can be checked statically.

We also provide a result on non-redundancy preserving of a generic mutation involving a transition that can be checked statically.

The following lemma shows that the application of a mutation TMI on a transition t (tmi_t in the following) of a mutant \(m^{\prime }\), i.e., removing such a transition from \(m^{\prime }\), produces by construction a mutant m that is non-subsumed by \(m^{\prime }\), in case t is controllable.

We note that a non-redundant transition to add could simply have a guard trivially true and an empty set of reset clocks (this will not be the case for the experiments in Section 5). Under the (assumed) hypothesis that the added transition is executable in at least one trace, such a mutation produces a non-subsumed mutant if an uncontrollable transition is added and a subsumed mutant if a controllable transition is added.

The next lemma shows that the application of a mutation TAD on a transition t (tad_t in the following) of a mutant \(m^{\prime }\), i.e., adding such a transition to \(m^{\prime }\), produces by construction a mutant m that is non-subsumed by \(m^{\prime }\), in case t is uncontrollable. Note that the added transition is non-redundant in the mutant.

Let c be a clock and let k be some constant. Then such a mutation does not generate a subsumed mutant when applied to a guard of the form x ≤ k of an uncontrollable transition or to a guard of the form x ≥ k of a controllable transition, under conditions discussed in the next lemma.

The next lemma provides the conditions under which the application of the mutation operator CXL on an invariant of a location ℓ (written as cxl_ℓ), yields a non-subsumed mutant.

Again, let c be a clock and let k be some constant. Then such a mutation produces a non-subsumed mutant when applied to a guard of the form x ≤ k of a controllable transition or to a guard of the form x ≥ k of an uncontrollable transition, as the next lemma shows.

The next lemma provides the conditions under which the application of the mutation operator CXS on an invariant of a location ℓ (written as cxs_ℓ) produces a non-subsumed mutant.

The following main theorem sums up all the results presented in this section. The specific additional conditions that need to hold for each mutation operator can be found in the corresponding lemmata.

Based on our results for detecting subsumed mutants (i.e., Lemmata 1–7), we provide guidelines for generating effective FMM and their corresponding FTG. The FTG in Fig. 3 (right) is an example of a “bad” model. This is because two out of three mutants of the model are subsumed, and a subsumed mutant cannot be used to generate effective test cases (Larsen et al. 2017). Hence, while building the FMM and the corresponding FTG (cf. Section 3.3), ideally one wants to minimise the number of subsumed mutants, thus maximising the effectiveness of the test-case generation phase. To do so, we select from Table 1 those results for detecting subsumed mutants that are applicable by only checking the syntax of the original model, rather than those based on the semantics.

Note that in Basile et al. (2020a), we reported two more commandments. The seventh commandment in Basile et al. (2020a) was distilled from the current Lemma 11, and it is a condition ensuring that the generated mutant is non-subsumed. As stated in Section 4.2, Lemma 11 also requires the original model to be non-redundant. This was the first commandment in (Basile et al. 2020a), in fact a pre-requisite on the used models. Since our focus is on subsumption detection and to improve the separation of concerns, all results about non-subsumed detection have now been rendered as auxiliary and are thus no longer part of the guidelines (and neither is the non-redundant requirement).

Finally, we note that such guidelines could be implemented directly as constraints in the feature model of the FMM (cf. Figure 5), such that subsumed mutants are prevented from being generated. In the next section, we provide an empirical evaluation of the results presented in this section, i.e., certain subsets of mutations are guaranteed to produce mutants that are a refinement of the SUT and thus there is no need to use them.

The objective of our empirical evaluation is to identify the mutation operators and the conditions under which a non-effective (i.e., subsumed) mutant is generated. We already addressed this by formally proving that mutants resulting from specific operators are subsumed under specific conditions, as reported in Theorem 1 and Table 1. To raise confidence in our results, we confront our theory with a practical implementation. Thus, we ask:

Our next question concerns the benefits of avoiding the generation of mutants that are subsumed by construction. In practice, the saved computation time is dependent on the concrete test-case generation and execution platform. Instead, we measure these benefits in a relative way, as the percentage of subsumed mutants that our guidelines can detect. Thus, we ask:

To answer these questions, we apply the mutation operators to a given original model to produce first-order mutants. To produce second-order mutants we apply second mutations on first-order mutants. Then, we check whether those mutants violate guidelines and whether they are subsumed by the original system model, using the refinement check implemented in the Uppaal or Ecdar tools (David et al. 2010b).

A proof-of-concept software has been implemented to perform the evaluation. The development of this software has been made necessary due to the high number of mutants to check for each case study. Indeed, in Basile et al. (2020a) the experiments were only considering first-order mutations of a single case study and were only partially automatised, requiring manual intervention to collect the data, parse the logs, and to produce the output tables. As a side-product, the software can be used as a tool to automatically check the guidelines on given mutants of Uppaal/Ecdar models, as well as for mutant generation with the mutation operators discussed in Section 3.3.

It is important to state at this point that the organisation of TG into the framework of FTG and FMM has been used to obtain a clean formalisation of the theoretical results discussed in Section 4. However, the guidelines for detecting subsumed mutants are independent from the way in which mutants are generated, i.e., they are not constrained to use FMM or FTG.

The experiments protocol is modular and has been divided into two main activities, depicted in Fig. 11, which led to the (parallel) production of two applications called AppMutant (developed by the third, fourth, and first authors) and AppEcdar (developed by the first author).

The experiment protocol is organised into a control part and an experimental part. The control part uses the run-time refinement checking offered by Uppaal (originally introduced in Ecdar) to check, for each mutant, whether or not it is a refinement. The experimental part statically analyses the mutants to check if they are violating the guidelines presented in this paper.

We note that whilst the theory presented in Section 4 only distinguishes between subsumed and non-subsumed mutants, the refinement checking performed by Uppaal may also return inconsistent as output. An inconsistent model is such that it cannot be refined to one satisfying two additional requirements, called output urgency and independent progress (cf. David et al. 2015, Def. 4). Output urgency states that an automaton cannot delay an enabled output. Independent progress is not satisfied by an automaton if it cannot internally (i.e., by only delaying or firing uncontrollable (output) actions) prevent an invariant from being violated in a location, against all possible inputs that may or may not arrive from the environment.

When answering a refinement query Sm <= S, Uppaal firstly refines Sm to be consistent. This means that the uncontrollable behaviour of Sm violating the requirements of consistency is pruned before performing the refinement checking (after pruning, the model can still be inconsistent because the controllable (input) behaviour is not pruned). Since, as for a subsumed mutant, an inconsistent model is not usable, we consider both subsumed and inconsistent mutants as “bad” mutants. More specifically, an inconsistent model is subsumed by any other model (similarly to how from false premises any conclusion can be reached), thus an inconsistent model is also a subsumed model.

As we will see in Section 5.4, this additional pruning operation of Uppaal that introduces further redundant mutated behaviour may cause subsumed or inconsistent mutants to be undetected by the commandments (for which this behaviour is not considered redundant).

Initially, the original models have been collected with only few adjustments (cf. Section 5.3) to make them consistent and usable by Uppaal. Indeed, we assume the competent programmer hypothesis (DeMillo et al. 1978) (i.e., developers produce initial models close to being correct). Thus, we assume that developers make only small mistakes (e.g., we will only mutate the clock constants by one time unit, see below). These simple mistakes (simulated by small mutations) can be put in cascade or coupled to form other emergent faults using higher-order mutants, according to the coupling effect (DeMillo et al. 1978).

The first activity is the generation of mutants which uses these original models to generate their mutants, in particular first-order and second-order (i.e., two mutations are applied) mutants. Each mutant operator is systematically applied to each relevant element (location or transition) of each model. The second-order mutants generation can be performed exhaustively or on a sample of each mutation (≤ 10%, see below). Sampling can be useful when the number of second-order mutants is huge, due to a combinatorial explosion. We generated all mutants for all case studies, and sampling had been used earlier to quickly validate the code and models. Moreover, the first activity also performs the experimental part on the generated mutants: for each mutant it is checked whether or not it violates some guideline.

AppMutant is the software that has been developed (in Java) to perform both the generation of mutants and the guidelines checking. The class diagrams of AppMutant are displayed in Fig. 12.

Each mutation is represented as a class instantiating the interface Mutation, offering facilities to compute the number of possible applications of the mutation to a specific model, as well as applying the mutation to a model (given as a parameter). Which of the identified possible mutants is to be generated (and stored) is a second parameter to the method apply. The guideline checking is also performed in the method apply: a Boolean flag is returned by this method with value true in case the generated mutant is violating a guideline, and value false otherwise.

For example, the abstract class ConstraintSmallerMutation implements Mutation and represents the mutation operator CXS. Two implementations of this abstract class are available, depending on whether the mutation is applied to a transition or to a location. In both cases, a method reduceBound is available to reduce the constant of the clock constraint. In the performed experiments, the bound is always reduced (resp., incremented) by one unit in CXS (resp., CXL). Note that CCN is only applied to transitions. The results presented in Section 4 are applicable to constraints with no conjunctions nor disjunctions. Accordingly, only these constraints can be mutated by the mutation operators. The TAD mutation operator is implemented by the abstract class TransitionAddedMutation. This abstract class is implemented by TransitionAddedControllable and TransitionAddedUncontrollable. The implementation of this mutation operator simply clones a transition (the first one encountered in the model), then changes the cloned transition source and target states and its action, and adds it to the model. In particular, a unique dummy action is used to avoid non-determinism.

The Mutator class is used to apply a Mutation to a Model. The class Model offers facilities to manage a Uppaal model (stored in .xml format). AppMutant is the executable class. It features methods for running first-order and second-order experiments.

Sampling is implemented in the runTwoMutationsSampling utility method. More in detail, this method takes as parameters the two mutation operators to apply, and the original model is retrieved with the method original. The method getPossibleMutations of the retrieved model returns the number of possible mutations that can be applied to that model for a given mutation operator (as parameter). By calling this method for the two mutation operators and multiplying the returned values (say, n1 and n2) the total number of possible mutations to apply is computed. The sampled number of mutants to generate is computed as \(\textit {max}(\frac {n1\times n2}{10},1000)\). For each mutant, the selected mutations to apply are chosen uniformly in the interval [0,n1] for the first mutation and [0,n2] for the second mutation.

The executable AppMutant has options for generating either first-order or second-order mutants, with or without sampling. The outputs of the execution are the created mutants (stored as Uppaal models) and a comma separated values file containing for each mutation operator the number of violations. Moreover, for each mutation a file listing the mutants that are violating guidelines is provided. Each generated model comes equipped with two or three automata: the original model (Spec), the first-order mutant (Spec_mutant), and the second-order mutant (Spec_mutant_mutant).

After computing both mutants and the violations log, the second activity is carried out using the AppEcdar application. AppEcdar has two concerns: execute for each mutant model the refinement checking and parse the logs.

During the refinement checking the queries evaluated by Uppaal are as follows (for first- and second-order mutants, respectively):

The evaluations of these queries for each mutant model produce logs that are grouped by their mutation operators and stored.

Concerning log parsing, the logs of violations and refinement checking are processed to provide as output the LATE X tables showed in this paper. Moreover, for validation purposes, a text file (called false negatives) is used to store all mutants violating a guideline whose refinement checking output is non-subsumed. The class diagrams of AppEcdar are displayed in Fig. 13.

The two main concerns of this activity are separated into two classes extending the Consumer functional interface of Java. The RefinementChecker class overrides the method apply(Integer) of Consumer<Integer> to execute the refinement checking, where the parameter indicates whether first-order or second-order mutants are processed. This class basically launches the verifytga Uppaal process, and can be executed on either Windows, Linux or Mac OS X. Similarly, LogParser extends the same interface and is used to perform the parsing: the mutants and violations logs parsing are decomposed into two separate methods. The class AppEcdar is the executable class. It offers options to select which case study to analyse, whether to perform refinement checking (indicating whether for first or second order), and whether to perform logs parsing (indicating whether for first or second order).

To enable the replication of our experiments, the source code, models, binaries and a video tutorial are publicly available.¹ Note that, for refinement checking, a distribution of Ecdar or Uppaal TIGA is required.² The experiments have been executed on a Windows machine with Java version 9.0.4 and a Linux Machine with OpenJDK 1.8, both using Uppaal TIGA 4.1.4 (rev. 5535), March 2014 academic version.

The third issue is that Uppaal TIGA requires that each model is consistent (cf. Section 5). In some of the case studies the automata had originally been designed to be consistent when composed with the other automata of the same case study (with specific parameter assignments), but not for any possible environment, as instead is required by the consistency checking of Uppaal TIGA. We solved this third issue by fixing the automata not satisfying these properties for the specific set-up of parameters. Indeed, performing refinement checking of inconsistent models would be useless.

We specify below the changes we applied to the models in order to deal with these three issues. We evaluated the guidelines on six case studies retrieved from the literature that are detailed next.

Here we interpret the results of our experiments for RQ1 and RQ2 for all the case studies. We applied all mutation operators discussed in the paper, namely TMI, TAD, SMI, CXL, CXS, and CCN. Mutations are applied singularly for first-order mutants or in pairs for second-order mutants. For each case study, we provide a table for first-order mutations and a table for second-order mutations (for reasons of readability, the latter are reported in Appendix A). Each table reports the total number of mutants, that of non-subsumed mutants, of subsumed mutants, of inconsistent mutants, and of mutants violating the guidelines, as well as—in the last column—the ratio of mutants that are statically detected to be subsumed by our guidelines, computed as follows:

The experiments confirm that all mutants violating the guidelines were subsumed or inconsistent, as expected, thus providing further confidence in our results and an answer to RQ1. This has been theoretically proved in Section 4, and the correctness of the proofs was confirmed during the experiments. Indeed, AppEcdar performed a false negative checking, to check for the presence of non-subsumed mutants violating the guidelines. No such mutants have been identified in any of the case studies. The correctness of the theoretical results can also be observed by the fact that, for each case study, the number of mutants violating the guidelines is never greater than the number of mutants that are either subsumed or inconsistent. We remark that all subsumed and inconsistent mutants that are violating the guidelines are those that would not be generated if one were to apply the guidelines presented in Section 4.4.

To answer RQ2, we report a histogram summarising the outcome of the experiments in Fig. 22. The results confirm the gain of our approach: more than half of all subsumed first-order mutants are detected by our guidelines for each case study, detecting 91%, 86%, and 77% subsumed mutants for, respectively, the COFFEE, ACCEL, and CAS case studies. As discussed in Section 5.4.2, this holds also for second-order mutants. Indeed, the guidelines were capable of detecting more than half of the second-order subsumed or inconsistent mutants for the case studies COFFEE, ACCEL, and CAS, and fewer for the remaining three case studies.

We also report a histogram in Fig. 23 showing what is the likelihood of generating a subsumed mutant when applying random mutations, with or without using the guidelines, for both first-order and second-order experiments. We assume that all mutations have the same probability of being applied. For each case study, the probability of generating a subsumed mutant is computed as

(the parameter of mutants violating guidelines is equal to zero when generating mutants without using the guidelines). Notably, the guidelines can drastically diminish the probability of generating subsumed mutants in some case study. The histogram shows how this probability gets lower when applying two mutations (independently of the usage of the guidelines). Indeed, by augmenting the number of mutations, it is less likely that they will have no effect on the mutated model. We note that HOTEL has the highest probability of generating subsumed mutants. This also explains the worst performances of the guidelines for this particular case study.

Several directions of improvement of the static analysis performed by the guidelines are possible. Different implementations of the mutation operators can be investigated. For example, our implementation of the TAD mutation operator adds uncontrollable transition that may be guarded. This is likely to introduce subsumed mutants not detected by our guidelines when such guards are never satisfied. By changing the implementation of TAD such that no guarded transition is added, the generated mutants are less likely to be subsumed. We note that TAD mutation is responsible for many undetected subsumed mutants in all the analysed case studies.

Parametric timed games (Luthmann et al. 2019; Luthmann et al. 2017) can be investigated to perform exhaustive experiments for the mutations CXL and CXS for all possible constant value updates. In the presented experiments, CXL and CXS updated the constants of clock constraints by increasing or decreasing by one unit.

More research is needed for the static detection of redundant elements (e.g., dangling locations). Our experiments have exploited the refinement checking provided by Uppaal, which however performs a pre-processing step to prune uncontrollable behaviour not consistent. For experiments performed with Uppaal, syntactically detecting locations not satisfying independent progress is possible. For example, if a location has a clock invariant of the form x ≤ k and no outgoing uncontrollable transition, then this location is not satisfying independent progress. This is the case for location qH1 of the HOTEL case study, which is indeed generating the worst performances for our guidelines. We argue that by statically pre-processing models similar to the HOTEL model to remove such “bad” locations, the performances can be improved.

In Fig. 21, an example of two mutations producing subsumed mutants whose composition is producing a non-subsumed mutant is displayed. However, these two mutations are not violating the guidelines. Indeed, the set of mutants violating the guidelines is a strict subset of the subsumed mutants. Further research is needed to prove or disprove whether the composition of two mutations violating guidelines always yields a subsumed mutant.

Finally, we note that the variation of percentages of detected mutants in each case study also depends on the number of controllable and uncontrollable transitions, as well as the presence of different types of constraints, which are specific to each case study.

Our empirical results essentially rely on the refinement relation as implemented in Uppaal/Ecdar. Should this implementation deviate (even slightly) from the definition we employ (itself based on the paper introducing Ecdar (David et al. 2010b)), we might witness the occurrence of false positives (mutants erroneously labelled as subsumed). To mitigate this risk, we conducted a non-exhaustive manual analysis of the sampled mutants.

Nevertheless, we did not remove these few false positives, which would actually improve our results since it would increase the percentage of subsumed mutants detected by our guidelines.