01: // CONSTANTS:
-02: #define MAX_CLIMB_SUM_ERR 100
+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: }
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 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
+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 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.
@@ -170,21 +181,48 @@ 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
- (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
-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 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 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 fe6b4e0e070..4d33545647a 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 */
+/** 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;