From 3267568b88ef7832c56287bec62fc8b559b9434a Mon Sep 17 00:00:00 2001 From: theyoucheng Date: Fri, 30 Sep 2016 15:24:14 +0100 Subject: [PATCH 1/4] Clarified the inputs for the pid case study. --- doc/html-manual/cover.shtml | 146 +++++++++++++++++++----------------- doc/html-manual/pid.c | 31 ++++---- 2 files changed, 92 insertions(+), 85 deletions(-) diff --git a/doc/html-manual/cover.shtml b/doc/html-manual/cover.shtml index dd007d06f02..7135f95ec0c 100644 --- a/doc/html-manual/cover.shtml +++ b/doc/html-manual/cover.shtml @@ -54,12 +54,12 @@ is plotted in the Figure below. 
01:  // CONSTANTS:
-02: #define MAX_CLIMB_SUM_ERR 100
+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,67 +70,69 @@ 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 funciton OUTPUTS */
+26: float desired_gaz;
+27: float desired_pitch;
+28:
+29: /** Accumulated error in the control */
+30: float climb_sum_err;
+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:     climb_pid_run(); 
+67:
+68:   }
+69:
+70:   return 0;
+72: }

In order to test the PID controller, we construct a main control loop, -which repeatedly invokes the function climb_pid_run (line 65). -In the beginning of the main function, the values of the desired speed desired_climb -and the estimated speed estimated_z_dot are initialised non-deterministically. -Subsequently, the __CPROVER_assume statement in lines 60 and 61 guarantees that -their values are bounded within a range. +which repeatedly invokes the function climb_pid_run (line 66). +In the beginning of each loop iteration, the values of the desired speed desired_climb +and the estimated speed estimated_z_dot are assigned non-deterministically. +Subsequently, the __CPROVER_assume statement in lines 63 and 64 guarantees that +their values are bounded within a valid range.

@@ -138,20 +140,20 @@ To demonstrate the automatic test suite generation in CBMC, we call the following command

-
cbmc pid.c --cover mcdc --unwind 25 --trace --xml-ui
+
cbmc pid.c --cover mcdc --unwind 6 --trace --xml-ui
 

 
 

 The option --cover mcdc 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 true and false.
-Consider the condition "pprz>=0 && pprz<=MAX_PPRZ" at line 39. CBMC
+Consider the condition "pprz>=0 && pprz<=MAX_PPRZ" in line 41. CBMC
 instruments three coverage goals to control the respective evaluated results of "pprz>=0" and 
 "pprz<=MAX_PPRZ". 
 We list them in below and they satisfy the MC/DC rules.
-Note that MAX_PPRZ is defined as 16 * 600 at line 06 of the program.
+Note that MAX_PPRZ is defined as 16 * 600 in line 06 of the program.
 

 
 
@@ -171,20 +173,26 @@ goals at the same time.  Each trace corresponds to a test case.
 
 

 For the example above, the following test suites are generated.
+A test suite consists of a sequence of input parameters that are
+passed to the PID function climb_pid_run at each loop iteration. 
 
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)
+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); (desired_climb=1.000000f, estimator_z_dot=1.000000f)
+    goal id: climb_pid_run.coverage.2
+T3: (desired_climb=0.000000f, estimator_z_dot=1.000000f)
+    goal id: climb_pid_run.coverage.3
 

 

 
 

-The option --unwind 25 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 --unwind 6 unwinds the loop inside the main
+function body six times. In order to achieve the complete coverage on the instrumented goals,
+the loop must be unwound sufficient enough times.
+For example, the PID function climb_pid_run needs to be called at
+least six times for evaluating the condition 
+climb_sum_err>MAX_CLIMB_SUM_ERR in line 48 to true.
+An introduction to the use of loop unwinding can be found
 in Understanding Loop Unwinding.
 

 
diff --git a/doc/html-manual/pid.c b/doc/html-manual/pid.c
index fe6b4e0e070..acb34a845e7 100644
--- a/doc/html-manual/pid.c
+++ b/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 */
 float desired_gaz;
 float desired_pitch;
-// Accumulated error in the system
-float climb_sum_err;
 
+/** Accumulated error in the control */
+float climb_sum_err;
 
 /** Computes desired_gaz and desired_pitch */
 void climb_pid_run() 
@@ -47,25 +48,23 @@ 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);
+
     climb_pid_run(); 
+
   }
 
   return 0;

From cf085a83f9142210249236f078a38dc7f8262cdd Mon Sep 17 00:00:00 2001
From: theyoucheng 
Date: Fri, 30 Sep 2016 22:43:02 +0100
Subject: [PATCH 2/4] Added the test suite for unwinding the loop 6 times in
 PID case study.

---
 doc/html-manual/cover.shtml | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/doc/html-manual/cover.shtml b/doc/html-manual/cover.shtml
index 7135f95ec0c..ed376737a16 100644
--- a/doc/html-manual/cover.shtml
+++ b/doc/html-manual/cover.shtml
@@ -192,6 +192,14 @@ the loop must be unwound sufficient enough times.
 For example, the PID function climb_pid_run needs to be called at
 least six times for evaluating the condition 
 climb_sum_err>MAX_CLIMB_SUM_ERR in line 48 to true.
+This corresponds to the test suite below.
+
(desired_climb=-1.000000f, estimator_z_dot=1.000000f);
+(desired_climb=-1.000000f, estimator_z_dot=0.000000f);
+(desired_climb=-1.000000f, estimator_z_dot=1.000000f);
+(desired_climb=-1.000000f, estimator_z_dot=1.000000f);
+(desired_climb=-1.000000f, estimator_z_dot=1.000000f);
+(desired_climb=-1.000000f, estimator_z_dot=1.000000f).
+

 An introduction to the use of loop unwinding can be found
 in Understanding Loop Unwinding.
 


From 6266a20e028e7821f6eaad1045b730764eae38e2 Mon Sep 17 00:00:00 2001
From: theyoucheng 
Date: Fri, 30 Sep 2016 22:53:38 +0100
Subject: [PATCH 3/4] Added the test suite for unwinding the loop 6 times in
 PID case study.

---
 doc/html-manual/cover.shtml | 11 +++++------
 1 file changed, 5 insertions(+), 6 deletions(-)

diff --git a/doc/html-manual/cover.shtml b/doc/html-manual/cover.shtml
index ed376737a16..d7e6f4b62d5 100644
--- a/doc/html-manual/cover.shtml
+++ b/doc/html-manual/cover.shtml
@@ -53,7 +53,7 @@ is plotted in the Figure below.
 
 
 
-
01:  // CONSTANTS:
+
01: // CONSTANTS:
 02: #define MAX_CLIMB_SUM_ERR 10
 03: #define MAX_CLIMB 1
 04:
@@ -187,11 +187,10 @@ T3: (desired_climb=0.000000f, estimator_z_dot=1.000000f)
 
 

 The option --unwind 6 unwinds the loop inside the main
-function body six times. In order to achieve the complete coverage on the instrumented goals,
-the loop must be unwound sufficient enough times.
-For example, the PID function climb_pid_run needs to be called at
-least six times for evaluating the condition 
-climb_sum_err>MAX_CLIMB_SUM_ERR in line 48 to true.
+function body six times. In order to achieve the complete coverage on all the instrumented goals 
+in the PID function climb_pid_run, the loop must be unwound sufficient enough times.
+For example, climb_pid_run needs to be called at least six times for evaluating the 
+condition climb_sum_err>MAX_CLIMB_SUM_ERR in line 48 to true.
 This corresponds to the test suite below.
 
(desired_climb=-1.000000f, estimator_z_dot=1.000000f);
 (desired_climb=-1.000000f, estimator_z_dot=0.000000f);

From 455c36bb312ffc4bd59012c669227e7d7ace3a9a Mon Sep 17 00:00:00 2001
From: theyoucheng 
Date: Fri, 7 Oct 2016 11:55:34 +0100
Subject: [PATCH 4/4] Refined the form of test suites generated for the PID
 controller.

---
 doc/html-manual/cover.shtml | 81 ++++++++++++++++++++++++-------------
 doc/html-manual/pid.c       | 12 ++++--
 2 files changed, 61 insertions(+), 32 deletions(-)

diff --git a/doc/html-manual/cover.shtml b/doc/html-manual/cover.shtml
index d7e6f4b62d5..45a3fb82143 100644
--- a/doc/html-manual/cover.shtml
+++ b/doc/html-manual/cover.shtml
@@ -77,12 +77,12 @@ is plotted in the Figure below.
 22: // Vertical speed of the UAV detected by GPS sensor
 23: float estimator_z_dot;
 24:
-25: /** PID funciton OUTPUTS */
+25: /** PID function OUTPUTS */
 26: float desired_gaz;
 27: float desired_pitch;
 28:
-29: /** Accumulated error in the control */
-30: float climb_sum_err;
+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() 
@@ -118,26 +118,35 @@ is plotted in the Figure below.
 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:     climb_pid_run(); 
-67:
-68:   }
-69:
-70:   return 0;
-72: }
+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: }
 

 
 

 In order to test the PID controller, we construct a main control loop,
-which repeatedly invokes the function climb_pid_run (line 66). 
-In the beginning of each loop iteration, the values of the desired speed desired_climb
-and the estimated speed estimated_z_dot are assigned non-deterministically.
+which repeatedly invokes the function climb_pid_run (line 69). 
+This PID function has two input variables: the desired speed desired_climb
+and the estimated speed estimated_z_dot.
+In the beginning of each loop iteration, values of the inputs are assigned non-deterministically.
 Subsequently, the __CPROVER_assume statement in lines 63 and 64 guarantees that
-their values are bounded within a valid range.
+both values are bounded within a valid range.
+The __CPROVER_input and __CPROVER_output will help clarify the inputs
+and outputs of interest for generating test suites.
 

 
 

 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.
 

 
 
cbmc pid.c --cover mcdc --unwind 6 --trace --xml-ui
@@ -172,16 +181,37 @@ goals at the same time.  Each trace corresponds to a test case.
 

 
 

-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 climb_pid_run at each loop iteration. 
+For example, Test 1 covers the MC/DC goal with id="climb_pid_run.coverage.1".
 
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); (desired_climb=1.000000f, estimator_z_dot=1.000000f)
-    goal id: climb_pid_run.coverage.2
-T3: (desired_climb=0.000000f, estimator_z_dot=1.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
 

 

 
@@ -191,14 +221,7 @@ function body six times. In order to achieve the complete coverage on all the in
 in the PID function climb_pid_run, the loop must be unwound sufficient enough times.
 For example, climb_pid_run needs to be called at least six times for evaluating the 
 condition climb_sum_err>MAX_CLIMB_SUM_ERR in line 48 to true.
-This corresponds to the test suite below.
-
(desired_climb=-1.000000f, estimator_z_dot=1.000000f);
-(desired_climb=-1.000000f, estimator_z_dot=0.000000f);
-(desired_climb=-1.000000f, estimator_z_dot=1.000000f);
-(desired_climb=-1.000000f, estimator_z_dot=1.000000f);
-(desired_climb=-1.000000f, estimator_z_dot=1.000000f);
-(desired_climb=-1.000000f, estimator_z_dot=1.000000f).
-

+This corresponds to the Test 5.
 An introduction to the use of loop unwinding can be found
 in Understanding Loop Unwinding.
 

diff --git a/doc/html-manual/pid.c b/doc/html-manual/pid.c
index acb34a845e7..4d33545647a 100644
--- a/doc/html-manual/pid.c
+++ b/doc/html-manual/pid.c
@@ -22,12 +22,12 @@ float desired_climb;
 // 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 control */
-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() 
@@ -63,8 +63,14 @@ int main()
     __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;