Symbolic Test Generation Using a Temporal Logic with Constrained Events - Formal Methods and Hybrid Real-Time Systems - page 470

Table 1. Test Results

TorX TorX

No. FD(%) S No. FD(%) S

FD(%) S FD(%) S

1 64.79 11.39 99.50 9.42 8 6.03 12.55 - -

2 64.79 11.39 97.00 10.10 9 10.82 14.19 39.50 18.63

3 13.42 8.41 - - 10 1.23 7.44 19.50 16.95

4 22.19 5.08 - - 11 20.00 29.30 - -

5 0.14 2.00 - - 12 0.68 19.10 30.00 21.53

6 37.53 11.96 40.50 19.98 13 38.36 4.00 - -

7 0.27 4.50 14.00 19.54 14 0.96 14.92 29.50 19.97

4 Case Study

We revise the symbolic test generation algorithm in [WL05] to adapt the syn-
tax and semantics of TLCE. The TorX tool environment [TB02] is used as the
execution engine for test campaigns.
A cache coherence protocol [GG04] is considered for a case study. The pro-
tocol aims to maintain the cache coherence among multi-processors with shared
memory. We construct a system model with 3 processes, based on the formal
description of the protocol presented in [PLL06], and design 6 test purposes in
TLCE, concerning the features defined in the protocol specification.
In total 730 test cases are derived by our tool, of which the state and transi-
tion coverage are both 100%. 14 erroneous mutants of the protocol are tested to
evaluate the effectiveness of these test cases. Table 1 illustrates the test results,
where FD stands for fault detection ratio [WST+05], column S shows the av-
erage number of steps that TorX has run to detect a mutant, and column TorX
shows the test results with 300 random test cases generated by TorX.
In our experiment, TorX is configured to run randomly no more than 35 steps.
It can be seen that the symbolic test cases result in a better mutation score
(100%) than random testing by TorX itself (57.14%). Moreover, most mutants
can be detected by the symbolic test cases within a fairly small number of steps.
In addition, for those mutants that can be detected by both methods, the
FDs of the symbolic test cases are less than those of the random test cases. This
actually conforms to the observation on accurate test cases stated in [JJRZ05].
A random test case, which is not correspondent to any test purpose, would
drive the system under test to exhibit non-conformance more possibly; while a
symbolic test case, which can reflect accurately the guiding test purpose, would
show less capability of detecting errors that are not related to that test purpose.

5Con lu on

We have proposed a temporal logic with constrained events to express test pur-
poses involving data dependencies between event parameters, and correspond-
ingly developed a symbolic test generation algorithm. Case studies have shown