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

Latest News

FORSYTE’s 2018 paper awards

FORSYTE has had a quite successful year: Adrian Rebola Pardo and his co-authors received the IJCAR best paper award for their paper Extended Resolution Simulates DRAT, Mitra Tabaei Befrouei and her co-authors received an OOPSLA 2018 Distinguished Paper award for their paper Randomized Testing of Distributed Systems with Probabilistic Guarantees, and Thomas Pani received the […]

Continue reading

OOPSLA Distinguished Paper Award

Mitra Tabaei Befrouei and her co-authors from MPI-SWS Burcu Kulahcioglu Ozkan, Rupak Majumdar, and Filip Niksic, received an OOPSLA’18 Distinguished Paper Award for their contribution “Randomized Testing of Distributed Systems with Probabilistic Guarantees” (Open Access article). Congratulations!

Continue reading

Zvonimir Rakamiric visiting FORSYTE

Prof. Zvonimir Rakamiric from the School of Computing at the University of Utah is spending his sabbatical with the FORSYTE group at TU Wien. He is generously sponsored by the Wolfgang Pauli Institute and a Pauli Fellow.

Continue reading

Helmut Veith Stipend Award Ceremony

The Vice Rector for Academic Affairs of TU Wien, Kurt Matyas, will award the scholarship recipient of the Helmut Veith Stipend at the award ceremony on Friday, April 06, 2018 in the Kontaktraum, starting at 17:05.

Continue reading

Full news archive