IEEE Transactions of Reliability Benchmarks

DSVerifier-Aided Verification Applied to Attitude Control Software in Unmanned Aerial Vehicles

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 10 digital controllers from an unmanned aerial vehicle (UAV), in particular, a quadrotor attitude system, taken from Design and Control of an Indoor Micro Quadrotor.

    Scripts to run the verification over the benchmarks: Benchmarks Scripts .

    Verification Results:

  • Overflow – Saturate Mode Verification Results
  • Overflow – Wrap-around Mode Verification Results
  • Limit-Cycle Verification Results
  • Digital Controllers Specifications:
    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.39154052734375z, -0.7646636962890625, 0} {0.8602752685546875, 0.52484130859375, 0} 0.02 <8,8>