ISSTA Benchmarks


Verifying Digital Systems with MATLAB.

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 9 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

  • CAV Benchmark:
  • A set of state-space models for different classes of systems was extracted from the literature and employed for validating our methodology.
    A DC Motor Rate plants describes the angular velocity of a DC Motor, respectively.
    The Automotive Cruise System plant represents the speed of a motor vehicle.
    The Helicopter Longitudinal Motion plant provides the longitudinal motion model of a helicopter.
    The Inverted Pendulum plant describes a pendulum model with its center of mass above its pivot point.
    The Magnetized Pointer plant describes a physical model employed in analogue gauges and indicators that is rotated through interaction with magnetic fields.
    The 1/4 Car Suspension plant presents a physical model that connects a car to its wheels and allows relative motion between both parts.
    The Computer Tape Driver plant describes a system to read and write data on a storage device in the computer.

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

    Counterexamples Graphs:

    Check our MATLAB diagrams for some counterexamples found by DSVerifier.

    Verification Results:

  • Transfer-Function Verification Results
  • State-Space Verification Results
  • Closed-Loop Verification Results
  • UAVs Benchmarks:
    Benchmark Id Numerator Denominator Sample Time Implementation
    controller-1 { 1.5, -0.5 } { 1.0, 0.0 } 0.02 <2,14>
    controller-2 { 60.0, -50.0 } { 1.0, 0.0 } 0.02 <6,10>
    controller-3 { 110.0, -100.0 } { 1.0, 0.0 } 0.02 <7,9>
    controller-4 { 135.0, -260.0, 125.0 } { 1.0, -1.0, 0.0 } 0.02 <8,8>
    controller-5 { 2002.0, -4000.0, 1998.0 } { 1.0, 0.0, -1.0 } 0.001 <10,6>
    controller-6 { 0.93, -0.87 } { 1.0, 1.0 } 0.02 <4,12>
    controller-7 { 0.1, -0.09998 } { 1.0, -1.0 } 0.02 <4,12>
    controller-8 { 0.0096, -0.009 } { 0.02, 0.0 } 0.02 <3,13>
    controller-9 { 0.1, -0.1 } { 1.0, -1.0 } 0.02 <4,12>
    DAES Benchmarks:
    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 >
    State-Space Benchmarks (CAV):
    Benchmark Id A B C D
    tapedriver_ss_disc1 [4.6764e-166,0,0;5.1253e-144,0,0;0,2.5627e-144,0] [0.125;0;0] [0.16,-2.7274e-23,0] [0]
    tapedriver_ss_disc2 [2.2259e-248,0,0;1.0251e-143,0,0;0,5.1253e-144,0] [0.125;0;0] [0.16,1.1554e-106,0] [0]
    tapedriver_ss_disc3 [-4.8229e-83,-2.8204e-83,5.7998e-98;3.2944e-83,0,0;0,3.2944e-83,0] [0.25;0;0] [0.08,0.090775,2.3179e-16] [0]
    tapedriver_ss_disc4 [1.0758e-33,-1.2605e-33,-5.2243e-48;7.7037e-34,0,0;0,7.7037e-34,0] [0.125;0;0] [0.16,0.010291,6.2509e-16] [0]
    tapedriver_ss_disc5 [5.5197e-17,-3.5503e-17,9.5141e-33;2.7756e-17,0,0;0,2.7756e-17,0] [0.25;0;0] [0.08,-0.04887,1.5463e-16] [0]
    tapedriver_ss_disc6 [-1.0862e-08,-4.2133e-09,1.0827e-22;7.4506e-09,0,0;0,7.4506e-09,0] [0.25;0;0] [0.08,0.047793,-1.2469e-15] [0]
    tapedriver_ss_disc7 [-0.044641,-0.01595,0.0007445;0.03125,0,0;0,0.00097656,0] [0.25;0;0] [0.081851,0.056338,-0.0026246] [0]
    tapedriver_ss_disc8 [-0.044641,-0.01595,0.0007445;0.03125,0,0;0,0.00097656,0] [0.25;0;0] [0.081851,0.056338,-0.0026246] [0]
    suspension_ss_disc1 [-5.915e-06,-2.7472e-06,3.3912e-52,-1.264e-208;3.8147e-06,0,0,0;0,3.8147e-06,0,0;0,0,3.8147e-06,0] [131072;0;0;0] [1.9074e-06,1,131072.5481,-59566.752] [0]
    suspension_ss_disc2 [-6.8455e-09,-2.2767e-09,7.8063e-79,0;1.4901e-08,0,0,0;0,2.9802e-08,0,0;0,0,5.9605e-08,0] [33554432;0;0;0] [7.4506e-09,1,16777216.0766,-642489.3324] [0]
    suspension_ss_disc3 [0.00074795,-0.0016575,1.8415e-26,-1.1243e-104;0.0019531,0,0,0;0,0.0019531,0,0;0,0,0.0019531,0] [256;0;0;0] [0.00097712,0.99991,255.4721,-172.6768] [0]
    suspension_ss_disc4 [-0.15905,-0.1019,8.849e-11,-6.0477e-42;0.0625,0,0,0;0,0.0625,0,0;0,0,0.0625,0] [16;0;0;0] [0.019589,0.60479,4.3085,-5.6516] [0]
    suspension_ss_disc5 [0.02366,-0.31922,0.0012041,-4.0292e-17;0.25,0,0,0;0,0.0019531,0,0;0,0,0.0019531,0] [256;0;0;0] [0.001404,0.0097416,1.3492,-390.7199] [0]
    suspension_ss_disc6 [0.76995,-0.56916,0.049073,-1.2695e-08;0.5,0,0,0;0,0.03125,0,0;0,0,0.03125,0] [16;0;0;0] [0.016561,0.049179,-0.032149,-17.4724] [0]
    suspension_ss_disc7 [2.0727,-1.3602,0.5395,-0.091745;1,0,0,0;0,0.5,0,0;0,0,0.125,0] [1;0;0;0] [0.047193,0.053056,-0.070934,-0.66128] [0]
    satellite_ss_disc1 [2,-1;1,0] [1;0] [0.5,0.5] [0]
    satellite_ss_disc2 [2,-1;1,0] [0.5;0] [0.25,0.25] [0]
    satellite_ss_disc3 [2,-1;1,0] [2;0] [1,1] [0]
    pendulum_ss_disc1 [-1.9999,-1;1,0] [4;0] [-1.7569,-1.7495] [9.8]
    pendulum_ss_disc2 [-0.028501,-1;1,0] [2;0] [-0.99605,-2.5603] [9.8]
    pendulum_ss_disc3 [0.0095007,-1;1,0] [2;0] [-2.5271,-0.96267] [9.8]
    pendulum_ss_disc4 [1.6203,-1;1,0] [1;0] [-1.5829,0.2514] [9.8]
    pendulum_ss_disc5 [1.9027,-1;1,0] [1;0] [-0.65262,0.31144] [9.8]
    pendulum_ss_disc6 [1.9755,-1;1,0] [0.5;0] [-0.57382,0.40218] [9.8]
    pendulum_ss_disc7 [1.999,-1;1,0] [0.25;0] [-0.20285,0.18909] [9.8]
    pendulum_ss_disc8 [1.9998,-1;1,0] [0.25;0] [-0.099716,0.096276] [9.8]
    magsuspension_ss_disc1 [54149865291660.31,-403447.9357;524288,0] [8388608;0] [8068958.7134,15.5109] [0]
    magsuspension_ss_disc2 [2.001,-1;1,0] [0.0625;0] [0.020002,0.020002] [0]
    dcmotor_ss_disc1 [0.90122,1.3429e-08;7.4506e-09,0] [128;0] [0.0014826,189.0217] [0]
    dcmotor_ss_disc2 [1.3678,-0.73569;0.5,0] [0.015625;0] [0.0047087,0.0067641] [0]
    dcmotor_ss_disc3 [0.94933,0;1,0] [0.25;0] [0.38902,0.00075955] [0]
    dcmotor_ss_disc4 [0.97941,0;1,0] [0.25;0] [0.15756,0.00078362] [0]
    dcmotor_ss_disc5 [0.98965,1.4747e-08;7.4506e-09,0] [128;0] [0.00015389,207.5687] [0]
    dcmotor_ss_disc6 [0.99481,-1.4824e-08;7.4506e-09,0] [128;0] [7.6368e-05,208.6509] [0]
    dcmotor_ss_disc7 [0.99901,-0.0058054;0.0078125,0] [0.125;0] [0.014393,0.20451] [0]
    dcmotor_ss_disc8 [1.0062,-0.10775;0.0625,0] [0.0625;0] [0.012819,0.04911] [0]
    cruiseHSCC_ss_disc1 [0.998] [0.125] [0.2112] [0]
    cruise_ss_disc1 [0.95123] [0.03125] [0.031213] [0]
    cruise_ss_disc2 [0.92774] [0.03125] [0.046244] [0]
    cruise_ss_disc3 [0.97531] [0.03125] [0.015802] [0]
    cruise_ss_disc4 [0.99005] [0.015625] [0.012736] [0]
    cruise_ss_disc5 [0.99501] [0.0078125] [0.012768] [0]
    cruise_ss_disc6 [0.9975] [0.0078125] [0.006392] [0]
    cruise_ss_disc7 [0.9995] [0.0039062] [0.0025594] [0]
    Closed-Loop Benchmarks (HSCC):
    Benchmark Id Plant Controller Sample Time Implementation
    controller-cruiser tf([9.7541E-04],[1.0, -0.9512]) tf([0.00390625, 0.0009765625],[0.3134765625, -0.0009765625]) 0.2 <3,7>
    controller-dc-motor tf([0.1898, 1.8027E-4],[1.0, -0.9012, -1.0006E-16]) tf([-0.3466796875, 0.015625],[0.5, 0.19921875, 0]) 2 <3,7>
    controller-dc-servo-motor tf([0.0001929, 6.814e-09],[1.0, -0.6921, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0]) tf([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 tf([-0.01285, 0.02582, -0.01293],[1.0, -2.99, 2.983, -0.9929]) tf([-0.580535888671875, 0.919769287109375, 0.11871337890625, -0.951934814453125],[0.7188720703125, -0.38751220703125, -0.415924072265625, 0.437286376953125]) 0.02 <4,11>
    controller-helicopter tf([15.1315, 17.8600, 17.4549],[1.0, -2.6207, 2.3586, -0.6570]) tf([-0.0009765625, 0, 0],[ 0.76171875, 0, 0, 0 ]) 2 <3,7>
    controller-pendulum tf([0.2039, 0.2039],[1.0, 1.19999, 1.0 ]) tf([-0.96484375, 0.9833984375],[0.8896484375, -0.875, 0 ]) 2 <3,7>
    controller-satelliteB2 tf([1.250000e-1, 1.250000e-1],[1.000000, -2.000000, 1.000000]) tf([0.8359375, 0.265625, -0.96875],[0.9453125, 0.90625, -0.15625, -0.123046875]) 0.001 <3,7>
    controller-spgMsDamper tf([5.000000e-5, 5.000000e-5],[1.000000, -2.000000, 1.000000]) tf([-0.0000000004656612873077392578125, 1.0000000004656612873077392578125, -1.0000000004656612873077392578125 ],[1, -0.0000000004656612873077392578125, 0.0000000004656612873077392578125]) 0.001 <15,16>
    controller-suspension tf([0.25, 0.5, 0.25, -4.3341E-7],[1.0, 5.9150E-6, 1.0480E-11, -4.9349E-63, 7.0168E-225]) tf([-0.0224609375, 0, 0, 0 ],[0.138671875, 0, 0, 0, 0]) 2 <3,7>
    controller-tapedriver tf([0.0200, -3.8303E-176],[1.0, -4.6764E-166]) tf([ 0, 0.0625 ],[0.517578125, -0.4990234375]) 2 <3,7>