1 Introduction
- An approach to compute adaptive test strategies for reactive systems from temporal specifications that provide implementation freedom. The tests are guaranteed to reveal certain bugs for every realization of the specification.
- The underlying theory is considered in detail, i.e., we show that the approach is sound and complete for many interesting cases and provide additional solutions for other cases that may arise in practice.
- A post-processing procedure to generalize a test strategy by eliminating input constraints not necessary to guarantee a coverage goal.
- A case study with a safety-critical software component of a real-world satellite system developed in the German Aerospace Center (DLR). We specify the system in LTL, synthesize test strategies, and evaluate the generated adaptive test strategies using code coverage and mutation coverage metrics. Our synthesized test strategies increase both the mutation coverage as well as the code coverage of random test cases by activating behaviors that require complex input sequences that are unlikely to be produced by random testing.
2 Motivating example
3 Background and related work
4 Preliminaries and notation
- \(\sigma _0 \sigma _1 \sigma _2 \ldots \models p\) iff \(p \in \sigma _0\),
- \({\overline{\sigma }}\models \lnot \varphi \) iff \({\overline{\sigma }}\not \models \varphi \),
- \({\overline{\sigma }}\models \varphi _1 \vee \varphi _2\) iff \({\overline{\sigma }}\models \varphi _1\) or \({\overline{\sigma }}\models \varphi _2\),
- \(\sigma _0 \sigma _1 \sigma _2 \ldots \models {{\,\mathrm{\mathsf {X}}\,}}\varphi \) iff \(\sigma _1 \sigma _2 \ldots \models \varphi \), and
- \(\sigma _0 \sigma _1 \ldots \models \varphi _1 \mathbin {\mathsf {U}}\varphi _2\) iff \(\exists j \ge 0 {{\,\mathrm{\mathbin {.}}\,}}\sigma _j \sigma _{j+1} \ldots \models \varphi _2 \wedge \forall 0 \le k < j {{\,\mathrm{\mathbin {.}}\,}}\sigma _k \sigma _{k+1} \ldots \models \varphi _1\).
5 Synthesis of adaptive test strategies
5.1 Coverage objective for test strategy computation
5.2 Test strategy computation
- Fault frequency \({{\,\mathrm{\mathsf {G}}\,}}\) means that the fault is permanent.
- Frequency \({{\,\mathrm{\mathsf {F}}\,}}\! {{\,\mathrm{\mathsf {G}}\,}}\) means that the fault occurs from some time step i on permanently. Yet, we do not make any assumptions about the precise value of i.
- Frequency \({{\,\mathrm{\mathsf {G}}\,}}\! {{\,\mathrm{\mathsf {F}}\,}}\) states that the fault strikes infinitely often, but not when exactly.
- Frequency \({{\,\mathrm{\mathsf {F}}\,}}\) means that the fault occurs at least once.
5.3 Extensions and variants
6 Case study
6.1 Eu:CROPIS FDIR specification
Boolean variable | Description |
---|---|
\(\mathtt{mode}_{\mathtt{1}}\,\) | \(\mathsf {true}\) iff \(S_1\) is activated |
\(\mathtt{mode}_{\mathtt{2}}\,\) | \(\mathsf {true}\) iff \(S_2\) is activated |
\(\mathtt{err}_{\mathtt{nc}}\,\) | \(\mathsf {true}\) iff a non-critical error is signaled by \(S_1\) or \(S_2\) |
\(\mathtt{err}_{\mathtt{s}}\,\) | \(\mathsf {true}\) iff a severe error is signaled by \(S_1\) or \(S_2\) |
reset | \(\mathsf {true}\) iff the FDIR component is reset |
\(\mathtt{on}_{\mathtt{1}}\,\) | \(\mathsf {true}\) iff \(S_1\) shall be switched on |
\(\mathtt{off}_{\mathtt{1}}\,\) | \(\mathsf {true}\) iff \(S_1\) shall be switched off |
\(\mathtt{on}_{\mathtt{2}}\,\) | \(\mathsf {true}\) iff \(S_2\) shall be switched on |
\(\mathtt{off}_{\mathtt{2}}\,\) | \(\mathsf {true}\) iff \(S_2\) shall be switched off |
safemode | \(\mathsf {true}\) iff the FDIR component initiates the safemode of the satellite |
lastup | \(\mathsf {true}\) if the last active system was \(S_1\) and \(\mathsf {false}\) if the last active system was \(S_2\) |
allowswitch | \(\mathsf {true}\) iff a switch of \(S_1\) to \(S_2\) or \(S_2\) to \(S_1\) is allowed |
Assumptions\(A_{1}\)–\(A_{6}\) | |
\(A_1\) | \({{\,\mathrm{\mathsf {G}}\,}}((\lnot \mathtt{mode}_{\mathtt{2}}\,\wedge \lnot \mathtt{mode}_{\mathtt{1}}\,) \rightarrow \lnot \mathtt{err}_{\mathtt{nc}}\,\wedge \lnot \mathtt{err}_{\mathtt{s}}\,)\) |
\(A_2\) | \({{\,\mathrm{\mathsf {G}}\,}}(\lnot \mathtt{err}_{\mathtt{nc}}\,\vee \lnot \mathtt{err}_{\mathtt{s}}\,) \wedge {{\,\mathrm{\mathsf {G}}\,}}(\mathtt{reset}\,\rightarrow \lnot \mathtt{err}_{\mathtt{nc}}\,\wedge \lnot \mathtt{err}_{\mathtt{s}}\,)\) |
\(A_3\) | \({{\,\mathrm{\mathsf {G}}\,}}(\mathtt{reset}\,\rightarrow {{\,\mathrm{\mathsf {X}}\,}}(\mathtt{mode}_{\mathtt{2}}\,\oplus \mathtt{mode}_{\mathtt{1}}\,))\) |
\(A_4\) | \(\begin{aligned} {{\,\mathrm{\mathsf {G}}\,}}(&\lnot \mathtt{mode}_{\mathtt{1}}\,\wedge \mathtt{on}_{\mathtt{1}}\,\wedge \lnot \mathtt{off}_{\mathtt{1}}\,\wedge \lnot \mathtt{on}_{\mathtt{2}}\,\wedge \lnot \mathtt{off}_{\mathtt{2}}\,\wedge \lnot \mathtt{reset}\,\wedge \lnot \mathtt{safemode}\,) \rightarrow \\ \quad&{{\,\mathrm{\mathsf {X}}\,}}\mathtt{mode}_{\mathtt{1}}\,\wedge (\mathtt{mode}_{\mathtt{2}}\,\leftrightarrow {{\,\mathrm{\mathsf {X}}\,}}\mathtt{mode}_{\mathtt{2}}\,)) \end{aligned}\) |
\(\begin{aligned} {{\,\mathrm{\mathsf {G}}\,}}(&\lnot \mathtt{mode}_{\mathtt{2}}\,\wedge \lnot \mathtt{on}_{\mathtt{1}}\,\wedge \lnot \mathtt{off}_{\mathtt{1}}\,\wedge \mathtt{on}_{\mathtt{2}}\,\wedge \lnot \mathtt{off}_{\mathtt{2}}\,\wedge \lnot \mathtt{reset}\,\wedge \lnot \mathtt{safemode}\,\rightarrow \\&{{\,\mathrm{\mathsf {X}}\,}}\mathtt{mode}_{\mathtt{2}}\,\wedge (\mathtt{mode}_{\mathtt{1}}\,\leftrightarrow {{\,\mathrm{\mathsf {X}}\,}}\mathtt{mode}_{\mathtt{1}}\,)) \end{aligned}\) | |
\(A_5\) | \(\begin{aligned} {{\,\mathrm{\mathsf {G}}\,}}(&\mathtt{mode}_{\mathtt{1}}\,\wedge \lnot \mathtt{on}_{\mathtt{1}}\,\wedge \mathtt{off}_{\mathtt{1}}\,\wedge \lnot \mathtt{on}_{\mathtt{2}}\,\wedge \lnot \mathtt{off}_{\mathtt{2}}\,\wedge \lnot \mathtt{reset}\,\wedge \lnot \mathtt{safemode}\,\rightarrow \\&{{\,\mathrm{\mathsf {X}}\,}}\lnot \mathtt{mode}_{\mathtt{1}}\,\wedge (\mathtt{mode}_{\mathtt{2}}\,\leftrightarrow {{\,\mathrm{\mathsf {X}}\,}}\mathtt{mode}_{\mathtt{2}}\,) ) \end{aligned}\) |
\(\begin{aligned} {{\,\mathrm{\mathsf {G}}\,}}(&\mathtt{mode}_{\mathtt{2}}\,\wedge \lnot \mathtt{on}_{\mathtt{1}}\,\wedge \lnot \mathtt{off}_{\mathtt{1}}\,\wedge \lnot \mathtt{on}_{\mathtt{2}}\,\wedge \mathtt{off}_{\mathtt{2}}\,\wedge \lnot \mathtt{reset}\,\wedge \lnot \mathtt{safemode}\,\rightarrow \\&{{\,\mathrm{\mathsf {X}}\,}}\lnot \mathtt{mode}_{\mathtt{2}}\,\wedge (\mathtt{mode}_{\mathtt{1}}\,\leftrightarrow {{\,\mathrm{\mathsf {X}}\,}}\mathtt{mode}_{\mathtt{1}}\,) ) \end{aligned}\) | |
\(A_6\) | \(\begin{aligned} {{\,\mathrm{\mathsf {G}}\,}}(&(\lnot (\lnot \mathtt{on}_{\mathtt{2}}\,\wedge \lnot \mathtt{off}_{\mathtt{1}}\,\wedge \lnot \mathtt{on}_{\mathtt{1}}\,\wedge \lnot \mathtt{off}_{\mathtt{2}}\,) \wedge {{\,\mathrm{\mathsf {X}}\,}}(\lnot \mathtt{on}_{\mathtt{2}}\,\wedge \lnot \mathtt{off}_{\mathtt{1}}\,\wedge \lnot \mathtt{on}_{\mathtt{1}}\,\wedge \lnot \mathtt{off}_{\mathtt{2}}\,) \wedge \\&(\lnot \mathtt{reset}\,\wedge {{\,\mathrm{\mathsf {X}}\,}}\lnot \mathtt{reset}\,\wedge \lnot \mathtt{safemode}\,\wedge {{\,\mathrm{\mathsf {X}}\,}}\lnot \mathtt{safemode}\,) \rightarrow \\&{{\,\mathrm{\mathsf {X}}\,}}((\mathtt{mode}_{\mathtt{2}}\,\leftrightarrow {{\,\mathrm{\mathsf {X}}\,}}\mathtt{mode}_{\mathtt{2}}\,) \wedge (\mathtt{mode}_{\mathtt{1}}\,\leftrightarrow {{\,\mathrm{\mathsf {X}}\,}}\mathtt{mode}_{\mathtt{1}}\,) ) \end{aligned}\) |
Guarantees\(G_{1}\)–\(G_{13}\) | |
\(G_1\) | \({{\,\mathrm{\mathsf {G}}\,}}((\mathtt{on}_{\mathtt{1}}\,\wedge \lnot \mathtt{on}_{\mathtt{2}}\,) \rightarrow ({{\,\mathrm{\mathsf {X}}\,}}\mathtt{lastup}\,))\) |
\({{\,\mathrm{\mathsf {G}}\,}}((\lnot \mathtt{on}_{\mathtt{1}}\,\wedge \mathtt{on}_{\mathtt{2}}\,) \rightarrow ({{\,\mathrm{\mathsf {X}}\,}}\lnot \mathtt{lastup}\,))\) | |
\({{\,\mathrm{\mathsf {G}}\,}}( (\lnot \mathtt{on}_{\mathtt{1}}\,\wedge \lnot \mathtt{on}_{\mathtt{2}}\,) \rightarrow (\mathtt{lastup}\,\leftrightarrow {{\,\mathrm{\mathsf {X}}\,}}\mathtt{lastup}\,))\) | |
\(G_2\) | \({{\,\mathrm{\mathsf {G}}\,}}(\mathtt{on}_{\mathtt{1}}\,\rightarrow \lnot \mathtt{off}_{\mathtt{1}}\,\wedge \lnot \mathtt{on}_{\mathtt{2}}\,\wedge \lnot \mathtt{off}_{\mathtt{2}}\,)\) |
\({{\,\mathrm{\mathsf {G}}\,}}(\mathtt{off}_{\mathtt{1}}\,\rightarrow \lnot \mathtt{on}_{\mathtt{1}}\,\wedge \lnot \mathtt{on}_{\mathtt{2}}\,\wedge \lnot \mathtt{off}_{\mathtt{2}}\,)\) | |
\({{\,\mathrm{\mathsf {G}}\,}}(\mathtt{on}_{\mathtt{2}}\,\rightarrow \lnot \mathtt{on}_{\mathtt{1}}\,\wedge \lnot \mathtt{off}_{\mathtt{1}}\,\wedge \lnot \mathtt{off}_{\mathtt{2}}\,)\) | |
\({{\,\mathrm{\mathsf {G}}\,}}(\mathtt{off}_{\mathtt{2}}\,\rightarrow \lnot \mathtt{on}_{\mathtt{1}}\,\wedge \lnot \mathtt{on}_{\mathtt{2}}\,\wedge \lnot \mathtt{off}_{\mathtt{1}}\,)\) | |
\(G_3\) | \({{\,\mathrm{\mathsf {G}}\,}}(\lnot \mathtt{mode}_{\mathtt{2}}\,\wedge \lnot \mathtt{mode}_{\mathtt{1}}\,\rightarrow {{\,\mathrm{\mathsf {F}}\,}}(\mathtt{reset}\,\vee \mathtt{on}_{\mathtt{2}}\,\vee \mathtt{on}_{\mathtt{1}}\,\vee \mathtt{safemode}\,))\) |
\(G_4\) | \({{\,\mathrm{\mathsf {G}}\,}}(\mathtt{allowswitch}\,\rightarrow \lnot \mathtt{safemode}\,)\) |
\(G_5\) | \({{\,\mathrm{\mathsf {G}}\,}}((\mathtt{mode}_{\mathtt{2}}\,\vee \mathtt{mode}_{\mathtt{1}}\,) \rightarrow \lnot \mathtt{on}_{\mathtt{1}}\,\wedge \lnot \mathtt{on}_{\mathtt{2}}\,)\) |
\(G_6\) | \({{\,\mathrm{\mathsf {G}}\,}}(\lnot \mathtt{allowswitch}\,\wedge \mathtt{lastup}\,\rightarrow \lnot \mathtt{on}_{\mathtt{2}}\,)\) |
\({{\,\mathrm{\mathsf {G}}\,}}(\lnot \mathtt{allowswitch}\,\wedge \lnot \mathtt{lastup}\,\rightarrow \lnot \mathtt{on}_{\mathtt{1}}\,)\) | |
\(G_7\) | \({{\,\mathrm{\mathsf {G}}\,}}(\lnot \mathtt{reset}\,\wedge \mathtt{allowswitch}\,\wedge \mathtt{lastup}\,\wedge \mathtt{on}_{\mathtt{2}}\,\rightarrow {{\,\mathrm{\mathsf {X}}\,}}\lnot \mathtt{allowswitch}\,)\) |
\({{\,\mathrm{\mathsf {G}}\,}}(\lnot \mathtt{reset}\,\wedge \mathtt{allowswitch}\,\wedge \lnot \mathtt{lastup}\,\wedge \mathtt{on}_{\mathtt{1}}\,\rightarrow {{\,\mathrm{\mathsf {X}}\,}}\lnot \mathtt{allowswitch}\,)\) | |
\(G_8\) | \({{\,\mathrm{\mathsf {G}}\,}}((\mathtt{allowswitch}\,\wedge \lnot (((\mathtt{lastup}\,\wedge \mathtt{on}_{\mathtt{2}}\,) \vee (\lnot \mathtt{lastup}\,\wedge \mathtt{on}_{\mathtt{1}}\,)))) \rightarrow {{\,\mathrm{\mathsf {X}}\,}}\mathtt{allowswitch}\,)\) |
\(G_9\) | \({{\,\mathrm{\mathsf {G}}\,}}(\mathtt{reset}\,\rightarrow {{\,\mathrm{\mathsf {X}}\,}}\mathtt{allowswitch}\,)\) |
\(G_{10}\) | \({{\,\mathrm{\mathsf {G}}\,}}(\mathtt{safemode}\,\rightarrow (\lnot \mathtt{on}_{\mathtt{1}}\,\wedge \lnot \mathtt{on}_{\mathtt{2}}\,))\) |
\(G_{11}\) | \({{\,\mathrm{\mathsf {G}}\,}}( \lnot \mathtt{allowswitch}\,\wedge \lnot \mathtt{reset}\,\rightarrow {{\,\mathrm{\mathsf {X}}\,}}\lnot \mathtt{allowswitch}\,)\) |
\(G_{12}\) | \( \begin{aligned} {{\,\mathrm{\mathsf {G}}\,}}(&(\mathtt{err}_{\mathtt{s}}\,\wedge \mathtt{mode}_{\mathtt{1}}\,\wedge \lnot \mathtt{reset}\,) \rightarrow \\&{{\,\mathrm{\mathsf {F}}\,}}(\mathtt{reset}\,\vee \mathtt{safemode}\,\vee \mathtt{mode}_{\mathtt{2}}\,\vee (\mathtt{mode}_{\mathtt{1}}\,\mathbin {\mathsf {U}}(\mathtt{mode}_{\mathtt{1}}\,\wedge \lnot \mathtt{err}_{\mathtt{s}}\,)))) \end{aligned}\) |
\(\begin{aligned} {{\,\mathrm{\mathsf {G}}\,}}(&(\mathtt{err}_{\mathtt{s}}\,\wedge \mathtt{mode}_{\mathtt{2}}\,\wedge \lnot \mathtt{reset}\,) \rightarrow \\&{{\,\mathrm{\mathsf {F}}\,}}(\mathtt{reset}\,\vee \mathtt{safemode}\,\vee \mathtt{mode}_{\mathtt{1}}\,\vee (\mathtt{mode}_{\mathtt{2}}\,\mathbin {\mathsf {U}}(\mathtt{mode}_{\mathtt{2}}\,\wedge \lnot \mathtt{err}_{\mathtt{s}}\,)))) \end{aligned}\) | |
\(G_{13}\) | \({{\,\mathrm{\mathsf {G}}\,}}((\mathtt{err}_{\mathtt{nc}}\,\wedge \mathtt{mode}_{\mathtt{1}}\,\wedge \lnot \mathtt{reset}\,) \rightarrow {{\,\mathrm{\mathsf {F}}\,}}(\mathtt{reset}\,\vee \mathtt{safemode}\,\vee \mathtt{mode}_{\mathtt{2}}\,\vee (\mathtt{mode}_{\mathtt{1}}\,\wedge \lnot \mathtt{err}_{\mathtt{nc}}\,)))\) |
\({{\,\mathrm{\mathsf {G}}\,}}((\mathtt{err}_{\mathtt{nc}}\,\wedge \mathtt{mode}_{\mathtt{2}}\,\wedge \lnot \mathtt{reset}\,) \rightarrow {{\,\mathrm{\mathsf {F}}\,}}(\mathtt{reset}\,\vee \mathtt{safemode}\,\vee \mathtt{mode}_{\mathtt{1}}\,\vee (\mathtt{mode}_{\mathtt{2}}\,\wedge \lnot \mathtt{err}_{\mathtt{nc}}\,)))\) |
6.2 Experimental results
6.2.1 Test strategy computation
safemode
of the FDIR component considering the fault models stuck-at-0, stuck-at-1, and bit-flip with the lowest possible fault frequencies. These are general fault assumptions and cover faults where the specification is violated with this signal being high (stuck-at-1), faults where the specification is violated with this signal being low (stuck-at-0) and faults where the specification is violated with this signal having the wrong polarity (bit-flip). We do not synthesize test strategies for the outputs \(\mathtt{on}_{\mathtt{2}}\,\) and \(\mathtt{off}_{\mathtt{2}}\,\) because they behave identical to \(\mathtt{on}_{\mathtt{1}}\,\) and \(\mathtt{off}_{\mathtt{1}}\,\), respectively, if the role of \(S_1\) and \(S_2\) are mutually interchanged. For synthesizing test strategies, both, the bound for the maximal number of states of a test strategy and the bound for the maximal number of test strategies, are set to four. We chose the bound to be four, because for this bound there exist strategies for all our chosen fault models and output signals. The size for the maximum number of strategies per variable and fault model is set arbitrarily to four and could also be set to a different value.Fault | \(o_i\) | \(\mathsf {frq}\) | \(|\mathcal {T}|\) | Time | Peak memory |
---|---|---|---|---|---|
(s) | (MB) | ||||
S-a-0 | \(\mathtt{on}_{\mathtt{1}}\,\) | \({{\,\mathrm{\mathsf {F}}\,}}\! {{\,\mathrm{\mathsf {G}}\,}}\) | 4 | 1.2k | 400 |
\(\mathtt{off}_{\mathtt{1}}\,\) | \({{\,\mathrm{\mathsf {F}}\,}}\! {{\,\mathrm{\mathsf {G}}\,}}\) | 3 | 517 | 396 | |
safemode | \({{\,\mathrm{\mathsf {F}}\,}}\! {{\,\mathrm{\mathsf {G}}\,}}\) | 4 | 934 | 324 | |
S-a-1 | \(\mathtt{on}_{\mathtt{1}}\,\) | \({{\,\mathrm{\mathsf {G}}\,}}\!{{\,\mathrm{\mathsf {F}}\,}}\) | 4 | 438 | 222 |
\(\mathtt{off}_{\mathtt{1}}\,\) | \({{\,\mathrm{\mathsf {F}}\,}}\! {{\,\mathrm{\mathsf {G}}\,}}\) | 4 | 753 | 378 | |
safemode | \({{\,\mathrm{\mathsf {G}}\,}}\!{{\,\mathrm{\mathsf {F}}\,}}\) | 3 | 169 | 192 | |
Bit-Flip | \(\mathtt{on}_{\mathtt{1}}\,\) | \({{\,\mathrm{\mathsf {G}}\,}}\!{{\,\mathrm{\mathsf {F}}\,}}\) | 4 | 26k | 3.6k |
\(\mathtt{off}_{\mathtt{1}}\,\) | \({{\,\mathrm{\mathsf {F}}\,}}\! {{\,\mathrm{\mathsf {G}}\,}}\) | 4 | 98.9k | 4.3k | |
safemode | \({{\,\mathrm{\mathsf {G}}\,}}\!{{\,\mathrm{\mathsf {F}}\,}}\) | 3 | 13.1k | 4.3k |
safemode
we are able to derive strategies for stuck-at-1 faults and bit-flips also at a lower frequency, i.e., we can detect those faults also if they occur at least infinitely often.safemode
being stuck at 0 computed consists of four states. Figure 11 illustrates the strategy. In the first state (state 0) we have the first system running (\(\mathtt{mode}_{\mathtt{1}}\,\)) and set the \(\mathtt{err}_{\mathtt{nc}}\,\) flag, i.e., we raise a non-critical error that requires the component to restart until the error is gone or to switch to the other system. We loop in this state until the FDIR component, if it behaves according to the specification, switches off the running system. In the next state (state 1), we do not set any input and wait for the FDIR component to eventually switch on one of the systems. If the component switches on the same system, then we go back to the previous state (state 0), if it switches on the other system we go into the next state (state 3). In this state we have the second system running (\(\mathtt{mode}_{\mathtt{2}}\,\)) and set again the \(\mathtt{err}_{\mathtt{nc}}\,\) flag, i.e., we again raise a non-critical error. We loop in this state until the FDIR component reacts and, if it conforms to the specification, switches off the running system. Continuing according to the strategy we always raise a non-critical error whatever system the FDIR component activates. Eventually the FDIR component has to activate safemode
or violate the specification. State 2 is only entered when the FDIR violates G5. In this state, it is irrelevant how the test strategy behaves because the specification has already been violated (which is easy to detect during test execution).
6.2.2 Test strategy evaluation
gcov
to measure the line and branch coverage of the source code.true
with false
or false
with true
,==
with !=
or !=
with ==
, and&&
with ||
or ||
with &&
gcc
to remove all mutant programs, which do not compile and do not conform to the C++ programming language. We analyzed the remaining 105 mutants manually and identified 5 equivalent mutant programs, i.e., they do not violate the specification. We further correct this number by removing another 17 mutant programs related to un-specified implementation-specific behavior. Next, we executed all test strategies on the mutant programs for 80 time steps each and log the corresponding execution traces.Output | Fault model | |||
---|---|---|---|---|
S-a-0 | S-a-1 | Bit-flip | All | |
(%) | (%) | (%) | (%) | |
\(\mathtt{on}_{\mathtt{1}}\,\) | 67.47 | 53.01 | 8.43 | 75.90 |
\(\mathtt{off}_{\mathtt{1}}\,\) | 13.25 | 3.61 | 16.87 | 16.87 |
safemode | 61.45 | 13.25 | 13.25 | 16.87 |
All | 71.08 | 55.42 | 16.87 | 78.31 |
safemode
and the three fault models stuck-at-0 (S-a-0), stuck-at-1 (S-a-1), and bit-flip (Bit-flip). The last column and last row show the mutation scores when considering all three fault models and all three signal, respectively.reset
is with \(10\%\) probability 1, and all other signals are with 50% probability 1.gcov
. The table is built as follows: the different testing approaches are shown in the columns. The columns R(0.1k), R(1k), R(10k), R(100k) refer to random testing with increasing numbers of input stimuli, and the columns S(80) and S(80) + R(10k) refer to the synthesized test strategies and the test strategies in combination with R(10k).Metric | Random stimuli | Adapt. strategies | ||||
---|---|---|---|---|---|---|
R(0.1k) | R(1k) | R(10k) | R(100k) | S(80) | S(80) + R(10k) | |
(%) | (%) | (%) | (%) | (%) | (%) | |
Line | 91.5 | 95.7 | 96.8 | 100.0 | 83.0 | 97.9 |
Branch | 85.4 | 89.6 | 89.6 | 93.8 | 70.8 | 91.7 |
Mutation | 88.0 | 92.8 | 94.0 | 98.0 | 78.3 | 97.6 |