ESEC/FSE 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

  • DAES Benchmark:
  • We designed 10 digital controllers for an A/C motor plant, extracted from Discrete-Time Control Systems. All digital controllers are designed in transfer-function format using 0.01s as sample time .

    Reference: DAES Publication, 2016

  • HSCC Benchmark:
  • The first set of benchmarks uses the discrete model of a cruise control system for a car, and accounts for rolling friction, aerodynamic drag, and the gravitational disturbance force.
    The second set of benchmarks considers the discrete model of a simple spring-mass damper plant.
    A third set of benchmarks uses the discrete model for satellite attitude dynamics, which require attitude control for orientation of antennas and sensors w.r.t. Earth.
    The fourth and fifth set of benchmarks describe the discrete model of a DC servo motor velocity dynamics.
    The sixth set of benchmarks contains a well-studied discrete non-minimal phase model. Non-minimal phase models cause additional difficulties for the design of stable controllers.
    The seventh set of benchmarks describes the discrete model for the Helicopter Longitudinal Motion, which provides the longitudinal motion dynamics of a helicopter.
    The eighth set of benchmarks contains the discrete model for the known Inverted Pendulum, which describes a pendulum dynamics with its center of mass above its pivot point.
    The ninth set of benchmarks contains the Magnetic Suspension discrete model, which describes the dynamics of a mass that levitates with support only of a magnetic field.
    The last set of benchmarks contains the Computer Tape Driver discrete model, which describes a system to read and write data on a storage device.

    Reference: HSSC Publication, 2017

    Tool and Data Availability at: Virtual Machine Download .

    Download DSValidator Toolbox at: Download Page .

    Scripts to run the DSValidator toolbox over the benchmarks: Benchmarks Scripts .

    Validation Results:

  • UAV Benchmark Validation Results
  • DAES Benchmark Validation Results
  • HSCC Benchmark 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>
    DAES Benchmark:
    Benchmark Id Numerator Denominator Sample Time Implementation
    controller-1 {0.15, 0.05, 0.4} {1.0, 0.0, 0.3} 0.01 < 3, 4 >
    controller-2 {2.000000, -4.000000, 2.000000} {1.000000, 0.000000, -0.250000} 0.01 < 2, 6 >
    controller-3 {0.2, -0.4, 0.2} {1.0, 0.0, -0.25} 0.01 < 3, 4 >
    controller-4 { 1.0, -2.819, 2.637, -0.8187} {1.0, -1.97, 1.033, -0.06068} 0.01 < 2, 13 >
    controller-5 {0.0937, -0.3582, 0.5201, -0.3482, 0.1003, -0.0078} {1.0000, 9.1122, -2.2473, -8.6564, 0.6569, 0.1355} 0.01 < 2, 13 >
    controller-6 {0.00937, -0.03582, 0.05201, -0.03482, 0.01003, -0.00078} {1.0000, 9.1122, -2.2473, -8.6564, 0.6569, 0.1355} 0.01 < 2, 13 >
    controller-7 {0.1, -0.2819, 0.2637, -0.08187} {1.0, -2.574, 2.181, -0.6068} 0.01 < 2, 13 >
    controller-8 {0.10, -0.28, 0.26, -0.08} {1.0, -2.57, 2.18, -0.60} 0.01 < 2, 8 >
    controller-9 {0.1, -0.28, 0.26, -0.08} {1.0, -2.57, 2.18, -0.60} 0.01 < 4, 11 >
    controller-10 {0.2, -0.4, 0.2} {1.0, 0.0, -0.25} 0.01 < 3, 12 >
    HSCC Benchmark:
    Benchmark Id Numerator Denominator Sample Time Implementation
    controller-cruiser {0.00390625, 0.0009765625} {0.3134765625, -0.0009765625} 0.2 <3,7>
    controller-dc-motor {-0.3466796875, 0.015625} {0.5, 0.19921875, 0} 2 <3,7>
    controller-dc-servo-motor {0.5, -0.96875, -0.875, -0.5} {0.001190185546875, 0.0008544921875, 0.000152587890625, 0.000335693359375, 0, 0, 0, 0, 0} 0.01 <4,11>
    controller-doyleetal {-0.580535888671875, 0.919769287109375, 0.11871337890625, -0.951934814453125} {0.7188720703125, -0.38751220703125, -0.415924072265625, 0.437286376953125} 0.02 <4,11>
    controller-helicopter {-0.0009765625, 0, 0} {0.76171875, 0, 0, 0} 2 <3,7>
    controller-pendulum {-0.96484375, 0.9833984375} {0.8896484375, -0.875, 0} 2 <3,7>
    controller-satelliteB2 {0.8359375, 0.265625, -0.96875} {0.9453125, 0.90625, -0.15625, -0.123046875} 0.001 <3,7>
    controller-spgMsDamper {-0.0000000004656612873077392578125, 1.0000000004656612873077392578125, -1.0000000004656612873077392578125} {1, -0.0000000004656612873077392578125, 0.0000000004656612873077392578125} 0.001 <15,16>
    controller-suspension {-0.0224609375, 0, 0, 0} {0.138671875, 0, 0, 0, 0} 2 <3,7>
    controller-tapedriver {0, 0.0625} {0.517578125, -0.4990234375} 2 <3,7>