Experiments
Source Code used for Queries Q1-Q24 in ASE’10 Publication
list2.c:
int partition(int a[], int left, int right) { int v = a[right], i = left - 1, j = right, t; for (;;) { while (a[++i] < v) ; while (j > left && a[--j] > v) ; if (i >= j) break; t = a[i]; a[i] = a[j]; a[j] = t; } t = a[i]; a[i] = a[right]; a[right] = t; return i; } int main(int argc, char * argv[]) { int A[3]; partition(A, 0, 2); }
sort1.c:
#include <stdio.h>
int compare(int a, int b) {
if (a <= b) return 1;
return 0;
}
int unfinished();
void sort(int * a, int len) {
int i, t;
for (i=1; i<len; ++i) {
if (compare(a[i-1], a[i])) continue;
unfinished();
t=a[i]; a[i]=a[i-1]; a[i-1]=t;
}
return;
}
void eval(int * a, int len) {
int i;
for (i=0; i < 3; ++i)
printf("a[%d]=%d\n", i, a[i]);
return;
}
int main(int argc, char * argv[]) {
int i; int A[3];
int verify;
for (i=0; i < 3; ++i)
sort(A, 3);
if (verify) {
assert(compare(A[0],A[1]));
assert(compare(A[1],A[2]));
}
eval(A, 3);
return 0;
}
sort2.c:
#include <stdio.h>
int rand_init;
void insert(int * a, int pos) {
int rand;
a[pos] = rand%rand_init;
return;
}
void eval(int * a, int first, int last) {
if (first > last) return;
printf("a[%d]=%d\n", first, a[first]);
eval(a+1, first+1, last);
return;
}
int precond() {
return (rand_init == 7);
}
int postcond() {
return (rand_init == 7);
}
int main(int argc, char * argv[]) {
int i;
int A[3];
int max;
if(max > 0)
init: rand_init = 7;
for (i=0; i<max; ++i)
insert(A, i);
eval(A, 0, max);
return 0;
}
Experiments Performed for our VMCAI’09 Publication
Source code used in the following experiments:
Source | LLOC* | Description |
---|---|---|
kbfiltr.i | 4879 | Preprocessed device drivers used in [1] for generating test cases with BLAST. |
floppy.i | 6435 | |
cdaudio.i | 8022 | |
parport.i | 20698 | |
parclass.i | 45283 | |
matlab.c | 2033 | An engine controller provided by an industrial collaborator from the automotive industries. It is generated from a MATLAB/Simulink model. |
statemate.c | 637 | Taken from the Mälardalen WCET Benchmark [2]: statemate.c was automatically generated by STARC (STAtechart Realtime Code generator), nsichneu.c simulates a Petri net, and adpcm.c implements functionality for adaptive pulse code modulation. In the benchmark, values of external variables are fixed. We replaced constant values by nondeterministic input. |
nsichneu.c | 1471 | |
adpcm.c | 365 | |
autopilot.i | 3141 | Preprocessed sources generated from source code in Papa-Bench [3]. We performed unit tests on periodic tasks of autopilot.i and fly_by_wire.i. In autopilot.i we replaced the implemented sinus function by a stub that returns a nondeterministic value because the implementation of sinus contains an unbounded loop. |
fly_by_wire.i | 488 |
*: Logical lines of code, i.e., the number of occurrences of ‘;’.
[1] Dirk Beyer, Adam J. Chlipala, Thomas A. Henzinger, Ranjit Jhala, and Rupak Majumdar. Generating Tests from Counterexamples. In Proceedings of the 26th IEEE International Conference on Software Engineering (ICSE 2004, Edinburgh, May 26-28), pages 326-335, 2004. IEEE Computer Society Press, Los Alamitos (CA).
[2] http://www.mrtc.mdh.se/projects/wcet/benchmarks.html
[3] http://www.irit.fr/recherches/ARCHI/MARCH/rubrique.php3?id_rubrique=97
Experimental results for basic block (BB) and condition coverage (CC):
Source file | BLAST (BB) | BB | CC | ||||
---|---|---|---|---|---|---|---|
#cases | Time[s] | #cases | Time[s] | Min* | #cases | Time[s] | |
kbfiltr.i | 39 | 300 | 26 | 18 | 6 | 98 | 24 |
floppy.i | 111 | 1500 | 63 | 1041 | 10 | 175 | 1259 |
cdaudio.i | 85 | 1500 | 71 | 1240 | 7 | 161 | 1243 |
parport.i | 213 | 5460 | 134 | 1859 | 21 | 351 | 2915 |
parclass.i | 219 | 2520 | 156 | 1324 | 16 | 392 | 2070 |
matlab.c | – | – | 5 | 30 | 1 | 16 | 31 |
statemate.c | – | – | 17 | 12 | 0 | 63 | 16 |
nsichneu.c | – | – | 14 | 3402 | 19 | 274 | 6929 |
adpcm.c | – | – | 1 | 34 | 0 | 9 | 36 |
autopilot.i | – | – | 206 | 894 | 14 | 450 | 1358 |
fly_by_wire.i | – | – | 4 | 89 | 1 | 7 | 113 |
*: Number of test cases removed by our test suite minimization algorithm.
-: No results from BLAST available.
To demonstrate the power of our approach,we considered queries on autopilot.i that
enforce a certain function call stack and focus coverage criteria to single functions:
> in periodic_task/ cover passing @entry -> / & @entry -> / & @entry -> @exit
queries for a test suite satisfying coverage criteria , where all test cases
start in periodic task passing its entry, thereafter the entry of , the entry
of and finally an exitpoint of periodic task. The following table shows the results.
The last two coverage criteria combine basic block and condition coverage at different
locations in the source code.
=/@blocks | ||||
#cases | Time[s] | Min | ||
course_run | course_pid_run | 171 | 1067 | 14 |
climb_control_task | climb_pid_run | 169 | 968 | 7 |
altitude_control_task | altitude_pid_run | 170 | 936 | 11 |
=/@conditions | ||||
#cases | Time[s] | Min | ||
course_run | course_pid_run | 369 | 2283 | – |
climb_control_task | climb_pid_run | 361 | 2422 | – |
altitude_control_task | altitude_pid_run | 365 | 2155 | – |
=/@blocks,/@conditions | ||||
#cases | Time[s] | Min | ||
course_run | course_pid_run | 377 | 1563 | 0 |
climb_control_task | climb_pid_run | 359 | 1625 | 0 |
altitude_control_task | altitude_pid_run | 372 | 1428 | 0 |
=/@conditions,/@blocks | ||||
#cases | Time[s] | Min | ||
course_run | course_pid_run | 170 | 1436 | 14 |
climb_control_task | climb_pid_run | 174 | 1138 | 12 |
altitude_control_task | altitude_pid_run | 174 | 921 | 14 |