Merge pull request #244 from theyoucheng/case-study

Clarified the inputs for the PID case study.

Author: Daniel Kroening

doc/html-manual/cover.shtml

@@ -53,13 +53,13 @@ is plotted in the Figure below.
 
 </center>
 
-<pre><code class="c numbered">01:  // CONSTANTS:
-02: #define MAX_CLIMB_SUM_ERR 100
+<pre><code class="c numbered">01: // CONSTANTS:
+02: #define MAX_CLIMB_SUM_ERR 10
 03: #define MAX_CLIMB 1
 04:
 05: #define CLOCK 16
 06: #define MAX_PPRZ (CLOCK*600)
-07: 
+07:
 08: #define CLIMB_LEVEL_GAZ 0.31
 09: #define CLIMB_GAZ_OF_CLIMB 0.75
 10: #define CLIMB_PITCH_OF_VZ_PGAIN 0.05
@@ -70,88 +70,99 @@ is plotted in the Figure below.
 15: const float climb_pgain=CLIMB_PGAIN;
 16: const float climb_igain=CLIMB_IGAIN;
 17: const float nav_pitch=0;
-18: 
-19: // 1) the target speed in vertical direction
-20: float desired_climb;
-21: // 2) vertical speed of the UAV, estimated by a control function
-22: float estimator_z_dot;
-23: 
-24: /** PID funciton OUTPUTS */
-25: float desired_gaz;
-26: float desired_pitch;
-27: // Accumulated error in the system
-28: float climb_sum_err;
-29: 
-30: /** Computes desired_gaz and desired_pitch */
-31: void climb_pid_run() 
-32: {
-33:  
-34:   float err=estimator_z_dot-desired_climb;
-35:  
-36:   float fgaz=climb_pgain*(err+climb_igain*climb_sum_err)+CLIMB_LEVEL_GAZ+CLIMB_GAZ_OF_CLIMB*desired_climb;
-37:  
-38:   float pprz=fgaz*MAX_PPRZ;
-39:   desired_gaz=((pprz>=0 && pprz<=MAX_PPRZ) ? pprz : (pprz>MAX_PPRZ ? MAX_PPRZ : 0));
-40:           
-41:   /** pitch offset for climb */
-42:   float pitch_of_vz=(desired_climb>0) ? desired_climb*pitch_of_vz_pgain : 0;
-43:   desired_pitch=nav_pitch+pitch_of_vz;
-44:   
-45:   climb_sum_err=err+climb_sum_err;
-46:   if (climb_sum_err>MAX_CLIMB_SUM_ERR) climb_sum_err=MAX_CLIMB_SUM_ERR;
-47:   if (climb_sum_err<-MAX_CLIMB_SUM_ERR) climb_sum_err=-MAX_CLIMB_SUM_ERR;
-48:  
-49:   /** Estimates the vertical speed */
-50:   estimator_z_dot=climb_pgain * err + desired_climb;
+18:
+19: /** PID function INPUTS */
+20: // The user input: target speed in vertical direction
+21: float desired_climb;
+22: // Vertical speed of the UAV detected by GPS sensor
+23: float estimator_z_dot;
+24:
+25: /** PID function OUTPUTS */
+26: float desired_gaz;
+27: float desired_pitch;
+28:
+29: /** The state variable: accumulated error in the control */
+30: float climb_sum_err=0;
+31:
+32: /** Computes desired_gaz and desired_pitch */
+33: void climb_pid_run() 
+34: {
+35:
+36:   float err=estimator_z_dot-desired_climb;
+37:
+38:   float fgaz=climb_pgain*(err+climb_igain*climb_sum_err)+CLIMB_LEVEL_GAZ+CLIMB_GAZ_OF_CLIMB*desired_climb;
+39:
+40:   float pprz=fgaz*MAX_PPRZ;
+41:   desired_gaz=((pprz>=0 && pprz<=MAX_PPRZ) ? pprz : (pprz>MAX_PPRZ ? MAX_PPRZ : 0));
+42:
+43:   /** pitch offset for climb */
+44:   float pitch_of_vz=(desired_climb>0) ? desired_climb*pitch_of_vz_pgain : 0;
+45:   desired_pitch=nav_pitch+pitch_of_vz;
+46:
+47:   climb_sum_err=err+climb_sum_err;
+48:   if (climb_sum_err>MAX_CLIMB_SUM_ERR) climb_sum_err=MAX_CLIMB_SUM_ERR;
+49:   if (climb_sum_err<-MAX_CLIMB_SUM_ERR) climb_sum_err=-MAX_CLIMB_SUM_ERR;
+50:
 51: }
 52:
 53: int main()
 54: {
-55:   /** Non-deterministic initialisation */ 
-56:   desired_climb=nondet_float();
-57:   estimator_z_dot=nondet_float();
-58:  
-59:   /** Range of initial values of variables */ 
-60:   __CPROVER_assume(desired_climb>=-MAX_CLIMB && desired_climb<=MAX_CLIMB);
-61:   __CPROVER_assume(estimator_z_dot>=-MAX_CLIMB && estimator_z_dot<=MAX_CLIMB);
-62:  
-63:   while(1)
-64:   {
-65:     climb_pid_run(); 
-66:   } 
-67:  
-68:   return 0;
-69: }
+55:
+56:   while(1)
+57:   {
+58:     /** Non-deterministic input values */ 
+59:     desired_climb=nondet_float();
+60:     estimator_z_dot=nondet_float();
+61:
+62:     /** Range of input values */ 
+63:     __CPROVER_assume(desired_climb>=-MAX_CLIMB && desired_climb<=MAX_CLIMB);
+64:     __CPROVER_assume(estimator_z_dot>=-MAX_CLIMB && estimator_z_dot<=MAX_CLIMB);
+65:
+66:     __CPROVER_input("desired_climb", desired_climb);
+67:     __CPROVER_input("estimator_z_dot", estimator_z_dot);
+68:
+69:     climb_pid_run();
+70:
+71:     __CPROVER_output("desired_gaz", desired_gaz);
+72:     __CPROVER_output("desired_pitch", desired_pitch);
+73:
+74:   }
+75:
+76:   return 0;
+77: }
 </code></pre>
 
 <p class="justified">
 In order to test the PID controller, we construct a main control loop,
-which repeatedly invokes the function <code>climb_pid_run</code> (line 65). 
-In the beginning of the main function, the values of the desired speed <code>desired_climb</code>
-and the estimated speed <code>estimated_z_dot</code> are initialised non-deterministically.
-Subsequently, the <code>__CPROVER_assume</code> statement in lines 60 and 61 guarantees that
-their values are bounded within a range.
+which repeatedly invokes the function <code>climb_pid_run</code> (line 69). 
+This PID function has two input variables: the desired speed <code>desired_climb</code>
+and the estimated speed <code>estimated_z_dot</code>.
+In the beginning of each loop iteration, values of the inputs are assigned non-deterministically.
+Subsequently, the <code>__CPROVER_assume</code> statement in lines 63 and 64 guarantees that
+both values are bounded within a valid range.
+The <code>__CPROVER_input</code> and <code>__CPROVER_output</code> will help clarify the inputs
+and outputs of interest for generating test suites.
 </p>
 
 <p class="justified">
 To demonstrate the automatic test suite generation in CBMC,
-we call the following command
+we call the following command and we are going to explain the command line options one by one.
 </p>
 
-<pre><code>cbmc pid.c --cover mcdc --unwind 25 --trace --xml-ui
+<pre><code>cbmc pid.c --cover mcdc --unwind 6 --trace --xml-ui
 </code></pre>
 
 <p class="justified">
 The option <code>--cover mcdc</code> specifies the code coverage criterion.
-There are four conditional statements in the PID function: in line 39, line 42, 
-line 46 and line 47. 
+There are four conditional statements in the PID function: in line 41, line 44, 
+line 48 and line 49. 
 To satisfy MC/DC, the test suite has to meet multiple requirements.
 For instance, each conditional statement needs to evaluate to <em>true</em> and <em>false</em>.
-Consider the condition <code>"pprz>=0 && pprz<=MAX_PPRZ"</code> at line 39. CBMC
+Consider the condition <code>"pprz>=0 && pprz<=MAX_PPRZ"</code> in line 41. CBMC
 instruments three coverage goals to control the respective evaluated results of <code>"pprz>=0"</code> and 
 <code>"pprz<=MAX_PPRZ"</code>. 
 We list them in below and they satisfy the MC/DC rules.
-Note that <code>MAX_PPRZ</code> is defined as 16 * 600 at line 06 of the program.
+Note that <code>MAX_PPRZ</code> is defined as 16 * 600 in line 06 of the program.
 </p>
 
 <pre>
@@ -170,21 +181,48 @@ goals at the same time.  Each trace corresponds to a test case.
 </p>
 
 <p class="justified">
-For the example above, the following test suites are generated.
+In the end, the following test suites are automatically generated for testing the PID controller.
+A test suite consists of a sequence of input parameters that are
+passed to the PID function <code>climb_pid_run</code> at each loop iteration. 
+For example, Test 1 covers the MC/DC goal with id="climb_pid_run.coverage.1".
 <pre><code>Test suite:
-T1: desired_climb=-1.000000f, estimator_z_dot=1.000000f
-    (goal id: climb_pid_run.coverage.1)
-T2: desired_climb=1.000000f, estimator_z_dot=-1.000000f
-    (goal id: climb_pid_run.coverage.2)
-T3: desired_climb=0.000000f, estimator_z_dot=0.000000f
-    (goal id: climb_pid_run.coverage.3)
+Test 1. 
+  (iteration 1) desired_climb=-1.000000f, estimator_z_dot=1.000000f
+
+Test 2.
+  (iteration 1) desired_climb=-1.000000f, estimator_z_dot=1.000000f 
+  (iteration 2) desired_climb=1.000000f, estimator_z_dot=-1.000000f 
+
+Test 3.
+  (iteration 1) desired_climb=0.000000f, estimator_z_dot=-1.000000f
+  (iteration 2) desired_climb=1.000000f, estimator_z_dot=-1.000000f
+
+Test 4.
+  (iteration 1) desired_climb=1.000000f, estimator_z_dot=-1.000000f
+  (iteration 2) desired_climb=1.000000f, estimator_z_dot=-1.000000f
+  (iteration 3) desired_climb=1.000000f, estimator_z_dot=-1.000000f
+  (iteration 4) desired_climb=1.000000f, estimator_z_dot=-1.000000f
+  (iteration 5) desired_climb=0.000000f, estimator_z_dot=-1.000000f
+  (iteration 6) desired_climb=1.000000f, estimator_z_dot=-1.000000f
+
+Test 5.
+  (iteration 1) desired_climb=-1.000000f, estimator_z_dot=1.000000f
+  (iteration 2) desired_climb=-1.000000f, estimator_z_dot=1.000000f
+  (iteration 3) desired_climb=-1.000000f, estimator_z_dot=1.000000f
+  (iteration 4) desired_climb=-1.000000f, estimator_z_dot=1.000000f
+  (iteration 5) desired_climb=-1.000000f, estimator_z_dot=1.000000f
+  (iteration 6) desired_climb=-1.000000f, estimator_z_dot=1.000000f
 </code></pre>
 </p>
 
 <p class="justified">
-The option <code>--unwind 25</code> unwinds the loop inside the main
-function body 25 times.  The number of the unwinding operation is
-adjustable, and an introduction to the use of loop unwinding can be found
+The option <code>--unwind 6</code> unwinds the loop inside the main
+function body six times. In order to achieve the complete coverage on all the instrumented goals 
+in the PID function <code>climb_pid_run</code>, the loop must be unwound sufficient enough times.
+For example, <code>climb_pid_run</code> needs to be called at least six times for evaluating the 
+condition <code>climb_sum_err>MAX_CLIMB_SUM_ERR</code> in line 48 to <em>true</em>.
+This corresponds to the Test 5.
+An introduction to the use of loop unwinding can be found
 in <a href="cbmc-loops.shtml">Understanding Loop Unwinding</a>.
 </p>
 

doc/html-manual/pid.c

@@ -1,5 +1,5 @@
 // CONSTANTS:
-#define MAX_CLIMB_SUM_ERR 100
+#define MAX_CLIMB_SUM_ERR 10
 #define MAX_CLIMB 1
 
 #define CLOCK 16
@@ -16,17 +16,18 @@ const float climb_pgain=CLIMB_PGAIN;
 const float climb_igain=CLIMB_IGAIN;
 const float nav_pitch=0;
 
-// 1) the target speed in vertical direction
+/** PID function INPUTS */
+// The user input: target speed in vertical direction
 float desired_climb;
-// 2) vertical speed of the UAV detected by GPS sensor
+// Vertical speed of the UAV detected by GPS sensor
 float estimator_z_dot;
 
-/** PID funciton OUTPUTS */
+/** PID function OUTPUTS */
 float desired_gaz;
 float desired_pitch;
-// Accumulated error in the system
-float climb_sum_err;
 
+/** The state variable: accumulated error in the control */
+float climb_sum_err=0;
 
 /** Computes desired_gaz and desired_pitch */
 void climb_pid_run() 
@@ -47,25 +48,29 @@ void climb_pid_run()
   if (climb_sum_err>MAX_CLIMB_SUM_ERR) climb_sum_err=MAX_CLIMB_SUM_ERR;
   if (climb_sum_err<-MAX_CLIMB_SUM_ERR) climb_sum_err=-MAX_CLIMB_SUM_ERR;
 
-  /** The control function for estimating the vertical speed */
-  estimator_z_dot=climb_pgain * err + desired_climb;
-
 }
 
-
 int main()
 {
-  /** Non-deterministic initialisation */ 
-  desired_climb=nondet_float();
-  estimator_z_dot=nondet_float();
-
-  /** Range of initial values of variables */ 
-  __CPROVER_assume(desired_climb>=-MAX_CLIMB && desired_climb<=MAX_CLIMB);
-  __CPROVER_assume(estimator_z_dot>=-MAX_CLIMB && estimator_z_dot<=MAX_CLIMB);
 
   while(1)
   {
+    /** Non-deterministic input values */ 
+    desired_climb=nondet_float();
+    estimator_z_dot=nondet_float();
+
+    /** Range of input values */ 
+    __CPROVER_assume(desired_climb>=-MAX_CLIMB && desired_climb<=MAX_CLIMB);
+    __CPROVER_assume(estimator_z_dot>=-MAX_CLIMB && estimator_z_dot<=MAX_CLIMB);
+
+    __CPROVER_input("desired_climb", desired_climb);
+    __CPROVER_input("estimator_z_dot", estimator_z_dot);
+
     climb_pid_run(); 
+
+    __CPROVER_output("desired_gaz", desired_gaz);
+    __CPROVER_output("desired_pitch", desired_pitch);
+
   }
 
   return 0;