October 12, 2016

HSCC Benchmarks

DSValidator: An Automated Counterexample Reproducibility Tool for Digital Systems: Benchmarks Results.

 

Experimental Setup:
The experiments were executed in a computer with the following hardware configurations: Intel Core i7-2600 3.40 GHz processor, 24 GB of RAM, and Ubuntu 64-bits OS. The experiments used the Linux times command to measure CPU time used for each benchmark. The runtime was limited to one hour (i.e., 3600s).

Benchmarks Description:

  • UAV Benchmark:

We extracted 11 digital controllers from an unmanned aerial vehicle (UAV), in particular, a quadrotor attitude system, taken from Design and Control of an Indoor Micro Quadrotor.

Reference: UAV Benchmarks, 2016

Download DSValidator Toolbox at: Download Page .

Counterexamples to be used on the DSValidator toolbox: Benchmarks Counterexamples .

Validation Results:

UAV Benchmark:
Test Case Id Numerator Denominator Sample Time Implementation
ds1-impl1 { 1.5, -0.5 } { 1.0, 0.0 } 0.02 <2,14>
ds1-impl2 { 1.5, -0.5 } { 1.0, 0.0 } 0.02 <4,12>
ds1-impl3 { 1.5, -0.5 } { 1.0, 0.0 } 0.02 <6,10>
ds2-impl1 { 60.0, -50.0 } { 1.0, 0.0 } 0.02 <6,10>
ds2-impl2 { 60.0, -50.0 } { 1.0, 0.0 } 0.02 <8,8>
ds2-impl3 { 60.0, -50.0 } { 1.0, 0.0 } 0.02 <10,6>
ds3-impl1 { 110.0, -100.0 } { 1.0, 0.0 } 0.02 <7,9>
ds3-impl2 { 110.0, -100.0 } { 1.0, 0.0 } 0.02 <9,7>
ds3-impl3 { 110.0, -100.0 } { 1.0, 0.0 } 0.02 <11,5>
ds4-impl1 { 135.0, -260.0, 125.0 } { 1.0, -1.0, 0.0 } 0.02 <8,8>
ds4-impl2 { 135.0, -260.0, 125.0 } { 1.0, -1.0, 0.0 } 0.02 <10,6>
ds4-impl3 { 135.0, -260.0, 125.0 } { 1.0, -1.0, 0.0 } 0.02 <11,5>
ds5-impl1 { 2002.0, -4000.0, 1998.0 } { 1.0, 0.0, -1.0 } 0.001 <10,6>
ds5-impl2 { 2002.0, -4000.0, 1998.0 } { 1.0, 0.0, -1.0 } 0.001 <12,4>
ds5-impl3 { 2002.0, -4000.0, 1998.0 } { 1.0, 0.0, -1.0 } 0.001 <13,3>
ds6-impl1 { 0.93, -0.87 } { 1.0, 1.0 } 0.02 <4,12>
ds6-impl2 { 0.93, -0.87 } { 1.0, 1.0 } 0.02 <8,8>
ds6-impl3 { 0.93, -0.87 } { 1.0, 1.0 } 0.02 <10,6>
ds7-impl1 { 0.1, -0.09998 } { 1.0, -1.0 } 0.02 <4,12>
ds7-impl2 { 0.1, -0.09998 } { 1.0, -1.0 } 0.02 <8,8>
ds7-impl3 { 0.1, -0.09998 } { 1.0, -1.0 } 0.02 <10,6>
ds8-impl1 { 0.0096, -0.009 } { 0.02, 0.0 } 0.02 <3,13>
ds8-impl2 { 0.0096, -0.009 } { 0.02, 0.0 } 0.02 <4,12>
ds8-impl3 { 0.0096, -0.009 } { 0.02, 0.0 } 0.02 <5,11>
ds9-impl1 { 0.1, -0.1 } { 1.0, -1.0 } 0.02 <4,12>
ds9-impl2 { 0.1, -0.1 } { 1.0, -1.0 } 0.02 <8,8>
ds9-impl3 { 0.1, -0.1 } { 1.0, -1.0 } 0.02 <10,6>
ds10-impl1 { 0.009, -0.0084 } { 1.0 } 0.02 <4,12>
ds10-impl2 { 0.009, -0.0084 } { 1.0 } 0.02 <8,8>
ds10-impl3 { 0.009, -0.0084 } { 1.0 } 0.02 <10,6>
ds11-impl1 { 0.1, -0.09996 } { 1.0, -1.0 } 0.02 <4,12>
ds11-impl2 { 0.1, -0.09996 } { 1.0, -1.0 } 0.02 <8,8>
ds11-impl3 { 0.1, -0.09996 } { 1.0, -1.0 } 0.02 <10,6>